Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
On this page about pure type systems, the section about the calculus of constructions says that $*$ is often called Prop, the type of propositions, and $\square$ is often called Type, the type of types.
In my intuition, it makes more sense to call $*$ Type, the sort of types, and $\square$ Kind, the sort of kinds, because:
1) Otherwise, if we want to use the same terminology for all calculi in the $\lambda$-cube, then the simply typed $\lambda$-calculus would only have a single type $* : \square$, and the things usually called types are now called propositions.
2) Proof irrelevance is not something that is being exploited by the syntax, as the name ’proposition’ suggests. I’m not too familiar with the CoC and its extensions, but I guess you also get a conflict in terminology when you move to the pCoC.
However, I’ve seen both uses of terminology on different locations. What is the reason for using the Prop:Type terminology?
I’ve actually never seen the word “kind” used for anything in CoC; everything I’ve read has used “prop” and “type”. In particular, that’s what Coq uses.
1 to 2 of 2