===== Les sortes =====

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

[[preuves_4#apartes|]]