В традиционной теории типов Мартина-Лёфа нет различия между типами и суждениями. Это идет под лозунгом «предложения как типы». Но иногда есть причины отличать их. CoC делает именно это.
Prop:Type
Type:PropPropPropType1Type2Type3PropType1Type2:Type1:Type2:Type3⋮
∏∏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)
Самое интересное - это разница между вторым и четвертым случаем. Четвертые правила говорит , что если находится в -му Вселенной и находится в -й вселенной, то произведение находится в -му Вселенной. Но второе правило говорит нам , что это не просто «еще одна вселенная на дне», потому что земли в , как только не делает, не важно , насколько велика есть. Это непредикативное , потому что позволяет определить элементыAiB(x)jmax(i,j)Prop∏x:AB(x)PropB(x)APropпутем количественного определения самого .Prop
Конкретным примером будет
против
Первый продукт находится в , но второй находится в (а не в , хотя мы количественно определяем элемент ). В частности, это означает , что один из возможных значений является сам.
∏A:Type1A→A
∏A:PropA→A
Type2PropType1Type1A∏A:PropA→A