Une sorte est un type pour les types.
Les propositions A, B, etc. sont des types (ceux de leurs termes de preuves).
Ces types sont de type Prop
.
On dit que A, B, etc. sont de sorte Prop
.
D'un autre coté, les booléens bool
, les entiers nat
sont des types dont le type est Set
.
Set
et Prop
sont de type Type
.
Set
là où l'on calculeProp
là où l'on raisonne