W tradycyjnej teorii typów Martina-Löfa nie ma rozróżnienia na typy i zdania. Jest to pod hasłem „propozycje jako typy”. Ale czasem istnieją powody, aby je rozróżniać. CoC właśnie to robi.
Istnieje wiele wariantów CoC, ale większość miałaby
ale nie . Kolejna różnica pojawia się, gdy mamy nieskończenie wiele wszechświatów typów i sprawiają, że impredykatywny (tak właśnie robi Coq). Konkretnie, rozważ wariant CoC, w którym mamy i nieskończenie wiele typów wszechświatów , , z
Reguła formacji dla
Prop:Type
Type:PropPropPropType1Type2Type3PropType1Type2:Type1:Type2:Type3⋮
∏musi wyjaśnić, jak utworzyć gdy jest twierdzeniem lub typem, a jest albo twierdzeniem, albo typem. Istnieją cztery kombinacje:
∏x:AB(x)AB(x)
A:Propx:A⊢B(x):Prop∏x:AB(x):Prop
A:Typeix:A⊢B(x):Prop∏x:AB(x):Prop
A:Propx:A⊢B(x):Typei∏x:AB(x):Typei
A:Typeix:A⊢B(x):Typej∏x:AB(x):Typemax(i,j)
Najciekawsza jest różnica między drugim a czwartym przypadkiem. Czwarta zasada mówi, że jeśli jest w wszechświecie, a jest w wszechświecie, to iloczyn jest w -tym wszechświecie. Ale druga zasada mówi nam, że to nie tylko „jeszcze jeden wszechświat na dole”, ponieważ ląduje w gdy tylko , niezależnie od tego, jak duże jestJest to impredykatywne, ponieważ pozwala nam zdefiniować elementyAiB(x)jmax(i,j)Prop∏x:AB(x)PropB(x)APropprzez kwantyfikację samego .Prop
Konkretnym przykładem może być
versus
Pierwszy produkt mieszka w , ale drugi jest w (a nie w , mimo że kwantyfikujemy element ). W szczególności oznacza to, że jedną z możliwych wartości dla jest samego
∏A:Type1A→A
∏A:PropA→A
Type2PropType1Type1A∏A:PropA→A