データ型

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

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