/- # データ型
型(type)は、直観的にはデータを分類するものです。集合が要素を持つように、型は項を持つことができます。

Lean では命題 `P : Prop` も型ですが、それらを除いた型は `Type u` の項になります。本書では `Type u` の項をデータ型と呼んでいます。
-/