Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthoranuyts
    • CommentTimeFeb 5th 2016
    • (edited Feb 5th 2016)

    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?

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 5th 2016

    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.