Foundations
We will consider Lean's type theory as a language for writing formal proofs. This language is highly expressive while consisting of only a few kinds of expressions.[…]We omit below expressions related to quotient types, and effectively consider a sublanguage. Every type is either a universe in the universe hierarchy, a function type, or arises from the type constructor of an inductive type. The remaining expressions can be organized along two axes:
| introduction | elimination | |
|---|---|---|
| function | \lambda-abstraction | evaluation |
| inductive type | constructor | recursor |
We begin with an introduction to types and universes. Since our primary goal is to study formal proofs using Lean, the universe of propositions at the bottom of the universe hierarchy plays a central role. The remainder of the chapter then proceeds through functions and inductive types.