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
Replying to
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
This Tweet was deleted by the Tweet author. Learn more
Yeah, I must admit I had no idea "*" was special in the context of PTSs before now! I thought it just meant 'type of types'. Thankfully learning about it now. 😆
Yeah I found the rules for Coq's Prop and SProp documented here: coq.inria.fr/distrib/curren
1
1
Show replies