The following diagram is a simplified hierarchy of the objects in Lean (click to enlarge).
There are two top-level objects called universes, Type and Prop.
- Within the Type universe, there are sets, such as the familiar $\mathbb{N}$, $\mathbb{Z}$ and $\mathbb{R}$. Each of these sets has elements, such as 13.
- Within the Prop universe, there are propositions, such as Odd 13. Some of these propositions may have proofs.
Under the top level universes, the second level objects are called types. The third level objects are called terms.
Unsurprising Example
When we write 13 : ℕ, we mean “13, the element of the set of natural numbers ℕ”.
Using the terminology of Lean, 13 is a term of type ℕ.
Surprising Example
When we write h : Odd 13, we mean “h, the proof of the proposition Odd 13”.
The proposition Odd 13 is a type, and proofs like h or by use 6; norm_num could be terms of this type. Rest assured, many people find this odd to begin with.
It may also seem surprising that h is a proof, because we've mostly talked about h as a hypothesis. When we use a hypothesis in a Lean proof, we are actually using the proof of a proposition.
