I am working through the Dependent Types chapter from Advanced Topics in Types and Programming Languages (ATTAPL) by Benjamin Pierce et al. I am confused with the calculus presented Fig 2-7 (Calculus of Constructions) that extends $\lambda LF$ to support
Prop type. I have multiple questions.
Propterm be $\beta$-reduced at all? The rule
(BETA-ALL)on the next page suggests that only the body of a
Propcan be reduced. That is, in the term
forall x:T.t, only
There are no atomic propositions like True, False. So how can one build a term of type
Prf p). Any simple example suffices.
I am not sure I understand the type equivalence rule
QT-ALLin Fig 2-7.
The encoding of
zerolater on) is confusing. For the sake of readability I am writing it down here.
nat = all a:Prop.all z:Prf a.all s:Prf a ->Prf a. a
What is the meaning? Specifically, what is
a- any Prop? Why are proofs of
I think these are lot of questions. I would appreciate answers to any of these questions.
EDIT: I was suggested to move this to cs.stackexchange.com. However, the question is about the meta-theory of Coq and I thought cstheory is an appropriate forum. But if multiple users suggest moving this, I can do that.