Inductive types and structures

Let’s see how Lean defines the type bool corresponding to the set {tt,ff} (whose elements are interpreted as “true” and “false”):

try it!

inductive bool
| tt : bool
| ff : bool

The inductive type bool is defined to have two constructors, namely tt and false. This is the type theory way to think about a set with two elements. The two terms of type bool are tt : bool and ff : bool. It looks a bit more clumsy than the corresponding set-theory argument.

However let us look now at the definition of the natural numbers. The full definition is this:

try it!

inductive nat
| zero : nat
| succ : nat → nat

That’s it. The natural numbers also have two constructors – zero, of type nat, and succ, which is a function taking terms of type nat to terms of type nat.

products of types and how ordered pairs work in dependent type theory. If A and B are types then we want the product type A × B to be a type with the property that to give a term of this type is the same as giving a term of type A and a term of type B. This is done in Lean using a structure.

try it!

structure prod (A : Type) (B : Type) :=
(fst : A) (snd : B)

notation A × B := prod A B

The result of this code is that a new type has been defined, or In words, this simply says that if A and B are types, then we define a new type prod A B by saying that the way to construct a term of this type is to give as input a term fst of type A and a term snd of type B. We then also define the usual notation for a product. That’s it. The usual definition of ordered pairs in set theory is slightly more painful than this – however this is not an argument for type theory over set theory; any mathematician who has dwelt on this knows that it does not matter that ordered pairs are messy to do in set theory, all that matters is the fact that if \((a_1,b_1)=(a_2,b_2)\) with \(a_1,a_2\in A\) and \(b_1,b_2\in B\) (or rather a₁ a₂ : A and b₁ b₂ : B as a type theorist would say) then \(a_1=a_2\) and \(b_1=b_2\). This lemma is called prod.mk.inj in Lean; the naming of basic lemmas like this follows a standard convention, which it is not hard to learn, and after a while one finds that one can guess the names of basic lemmas of this sort. One also needs access to the projection functions \(A\times B\to A\) and \(A\times B\to B\), and both set theory and type theory offer these; in type theory, if c : A × B then c.fst : A and c:snd : B are the two projections.

try it!

structure prod (A : Type) (B : Type) :=
(fst : A) (snd : B)

notation A × B := prod A B

definition c : \N \times \N := \<4,5\>
#eval c.fst -- 4

Quotient types

I talk about these in the chapter on equivalence relations.