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 ℕ”.
We also say 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, just as ℕ is a type.
Proofs like h or by use 6; norm_num could be terms of the type Odd 13, just as 13 is a term of type ℕ.
Rest assured, most people find this odd to begin with.
