En la teoría de tipos tradicional de Martin-Löf no hay distinción entre tipos y proposiciones. Esto va bajo el lema "proposiciones como tipos". Pero a veces hay razones para distinguirlos. CoC hace precisamente eso.
Hay muchas variantes de CoC, pero la mayoría tendría
pero no . Otra diferencia aparece cuando tenemos infinitos universos tipo y hacemos que impredecible (esto es lo que hace Coq). Concretamente, considere una variante de CoC donde tenemos e infinitos universos tipo , , con
La regla de formación para
Prop:Type
Type:PropPropPropType1Type2Type3PropType1Type2:Type1:Type2:Type3⋮
∏tiene que explicar cómo formar cuando es una proposición o un tipo, y es una proposición o un tipo. Hay cuatro combinaciones:
∏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)
Lo más interesante es la diferencia entre el segundo y el cuarto caso. La cuarta regla dice que si está en el universo -ésimo y está en el universo , entonces el producto está en el universo . Pero la segunda regla nos dice que no es solo "un universo más en la parte inferior", porque aterriza en tan pronto como no, no importa lo grande es. Esto no es predictivo porque nos permite definir elementos deAiB(x)jmax(i,j)Prop∏x:AB(x)PropB(x)APropcuantificando sobre sí.Prop
Un ejemplo concreto sería
versus
El primer producto vive en , pero el segundo está en (y no en , a pesar de que estamos cuantificando sobre un elemento de ). En particular, esto significa que uno de los valores posibles para es mismo.
∏A:Type1A→A
∏A:PropA→A
Type2PropType1Type1A∏A:PropA→A