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.
1
3
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
Replying to
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.
Replying to
I could never compute PTSs in my head. That rule looks odd, but if you’re truncating a sound PTS, the result should be type-safe (trivially) and might satisfy preservation (not so sure but I guess).
1
1
Yeah it does look a bit odd on it's own. And yeah, ℛ is always super mind-bending.
The idea is that it's kind of using the 'maximum sort' of the two input types as the sort of the pi type. It's as if we only had two universe levels: 0 and 1 (for * and □ respectively).
2
Show replies