Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthoranuyts
   • CommentTimeFeb 5th 2016
   • (edited Feb 5th 2016)
   • PermaLink
   Author: anuyts
   Format: MarkdownItexOn [this page](https://ncatlab.org/nlab/show/pure+type+system#CalculusOfConstructions) 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?

   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?

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 5th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI'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.

   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.