Does anyone know why CC as a PTS is often given the rules:
ℛ = { (*,*,*), (*,□,□), (□,*,*), (□,□,□) }
But systems with universe levels often use the rules:
ℛ = { (𝒰_i, 𝒰_j, 𝒰_max(i,j)) | i, j ∈ ℕ }
(□,*,*) doesn't seems to follow the max(i,j) pattern? 🤔
Conversation
For more info: ncatlab.org/nlab/show/pure
• CC: Calculus of constructions (aka. λC)
• PTS: Pure Type System
(s1,s2,s3) is often abbreviated to (s1,s2), where s2 = s3. So I'm confused about the (□,*) rule of CC.
Replying to
IIRC that’s F-style impredicativity. It doesn’t show up in the hierarchy because you can only do it once (else, IIUC, you can embed the inconsistent Systems U- or U).
Today, in Coq that’s restricted to (forall X: Prop. P): Prop (when P: Prop). CC is closer to impredicative Set.
1
2
Oh cool! Very interesting. So I'm wondering if it would be fine if I chose the rule (□,*,□) instead of (□,*,*). I don't want a full hierarchy of universes, but I don't want the impredicativity either.
1
2
Show replies