0
$\begingroup$

I'm studying the calculus of constructions from ATAPL, Chapter 2. I'm trying to understand the Type Equivalence rule, which describes the meaning of the new type family Prf a. The rule states:

Γ ⊢ T :: *         Γ, x:T ⊢ t: Prop
---------------------------------------[QT-ALL]
Γ ⊢ Prf (all x:T.t) ≡ Πx:T. Prf t :: *

This rule seems to state that types of the form of Prf(all ...) is equivalent to Π types. Combining this with the information that:

  1. Prf: Πx:Prop.* [Prof needs Prop as input]
  2. The only constructor of Prop is of the form all ...

implies that the only well-typed occurrence of Prf we can have is of the form Prf (all ...), which is equivalent to the Pi-type encoding (as given by QT-ALL). Thus, I see no benefit gained by adding the Prf/Prop mechanism. I believe we gain something to do with impredicativity, as we can use all x:T.t : Prop to quantify over Prop itself. I don't know enough theory to judge whether this is possible or impossible just using Pi types.

Clearly, I am missing something. Could I please have an explanation of what we gain by introducing Prf/Prop that we did not already have with Pi types?

I've added a picture of the full definition here:

enter image description here

$\endgroup$
2
  • 1
    $\begingroup$ Isn't Prf just the decoding of the element of Prop to types? That is, the elements of Prop are not actual types, but their "codes" which need to be "decoded" to actualy types. QT-All says that all is decoded as Π. This is a bit like Tarski-style universes, if you're familiar with those. $\endgroup$ May 12 at 8:14
  • $\begingroup$ Martin Hoffman's thesis: and Syntax and Semantics of Dependent Types tcs.ifi.lmu.de/mitarbeiter/martin-hofmann/pdfs/… might provide some more context and examples $\endgroup$
    – user833970
    Oct 8 at 17:32
2
$\begingroup$

It is false that the only well-typed occurrence of Prf has to be of the form Prf(all ...). For example, in the context with a variable p : Prop we can form the type Prf(p) which is not of the stated form. Another possibility is that we have a Prf(t) for some closed term t : Prop which is not of the form all ... but it normalizes to it.

The purpose of Prf is to decode, or coerce, the elements of Prop to types. That is, the elements of Prop are not actual types, so if we want to use them as if they were types, they first have to be coerced to types, which is what Prf does. The rule QT-All states that all decodes to Π.

To put it differently, Prop is a Tarski universe and Prf is the type family that decodes its elements as types.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.