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 calcule
• Prop là où l'on raisonne

apartes