Constructions
We have now seen all the primitive notions in Lean's type theory. To reiterate, they are universes, function types, and inductive types,[…]We view formation of function and inductive types as primitive notions. This does not include concrete function types or inductive types. together with introduction and elimination of expressions of the latter two types. In addition, we have considered the concrete inductive types Eq and Nat, as well as the product and sum types Prod and Sum.
We begin with an encoding of first-order logic using inductive types. This involves product and sum types similar to Prod and Sum, a dependent sum type, a unit type, and an empty type.[…]These types are called And, Or, Exists, True, and False. The remainder of the chapter then takes a deeper look at Eq and Nat.