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
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
Well, star *is* the type of types (usually of small types, lest you like dancing lambada-star ๐). It's just that impredicativity can only make *one* universe special :-). It probably doesn't need to be the first one?
1
This Tweet was deleted by the Tweet author. Learn more
Show replies