<p>It is false that the only well-typed occurrence of <code>Prf</code> has to be of the form <code>Prf(all ...)</code>. For example, in the context with a variable <code>p : Prop</code> we can form the type <code>Prf(p)</code> which is not of the stated form. Another possibility is that we have a <code>Prf(t)</code> for some closed term <code>t : Prop</code> which is not of the form <code>all ...</code> but it <em>normalizes</em> to it.</p>
<p>The purpose of <code>Prf</code> is to decode, or coerce, the elements of <code>Prop</code> to types. That is, the elements of <code>Prop</code> are <em>not</em> 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 <code>Prf</code> does. The rule <code>QT-All</code> states that <code>all</code> decodes to <code>Π</code>.</p>
<p>To put it differently, <code>Prop</code> is a <a href="https://ncatlab.org/homotopytypetheory/show/universe#Tarski" rel="nofollow noreferrer">Tarski universe</a> and <code>Prf</code> is the type family that decodes its elements as types.</p>

CC BY-SA 4.0
2021-05-12T08:40:28.653Z
2021-05-12T08:40:28.653Z
Andrej Bauer
<p>I'm studying the calculus of constructions from ATAPL, Chapter 2. I'm trying to understand the <em>Type Equivalence</em> rule, which describes the meaning of the new type family <code>Prf a</code>. The rule states:</p>
<pre><code>Γ ⊢ T :: *         Γ, x:T ⊢ t: Prop
---------------------------------------[QT-ALL]
Γ ⊢ Prf (all x:T.t) ≡ Πx:T. Prf t :: *
</code></pre>
<p>This rule seems to state that types of the form of <code>Prf(all ...)</code> is <em>equivalent</em> to <code>Π</code> types. Combining this with the information that:</p>
<ol>
<li><code>Prf: Πx:Prop.*</code> [<code>Prof</code> needs <code>Prop</code> as input]</li>
<li>The only constructor of <code>Prop</code> is of the form <code>all ...</code></li>
</ol>
<p>implies that the <em>only</em> well-typed occurrence of <code>Prf</code> we can have is of the form <code>Prf (all ...)</code>, which is equivalent to the Pi-type encoding (as given by <code>QT-ALL</code>).
Thus, I see no benefit gained by adding the <code>Prf/Prop</code> mechanism. I believe we gain something to do with impredicativity, as we can use <code>all x:T.t : Prop</code> to quantify over <code>Prop</code> itself. I don't know enough theory to judge whether this is possible or impossible just using <code>Pi</code> types.</p>
<p>Clearly, I am missing something. Could I please have an explanation of what we gain by introducing <code>Prf/Prop</code> that we did not already have with <code>Pi</code> types?</p>
<p>I've added a picture of the full definition here:</p>
<p><a href="https://i.sstatic.net/TnWMG.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/TnWMG.png" alt="enter image description here" /></a></p>

CC BY-SA 4.0
2021-05-12T08:14:52.097Z
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.
Andrej Bauer
CC BY-SA 4.0
2021-10-08T17:32:31.847Z
Martin Hoffman's thesis: 
and Syntax and Semantics of Dependent
Types https://www.tcs.ifi.lmu.de/mitarbeiter/martin-hofmann/pdfs/syntaxandsemanticsof-dependenttypes.pdf might provide some more context and examples
user833970
<dependent-type><type-systems><calculus-of-constructions>
Calculus of constructions: Why forall when pi exists?
Siddharth Bhat
# Calculus of constructions: Why forall when pi exists?

(Asked by: username_0 on 2021-05-12)

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:

Prf: Πx:Prop.* [Prof needs Prop as input]
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:

**Tags:** dependent-type, type-systems, calculus-of-constructions
> **Comments:**
> **username_1**: 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.  
> **username_2**: Martin Hoffman's thesis:  and Syntax and Semantics of Dependent Types https://www.tcs.ifi.lmu.de/mitarbeiter/martin-hofmann/pdfs/syntaxandsemanticsof-dependenttypes.pdf might provide some more context and examples  

---

## 1 answers

### Answer by username_1 on 2021-05-12. Score: 2 | Accepted answer

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](https://ncatlab.org/homotopytypetheory/show/universe#Tarski) and `Prf` is the type family that decodes its elements as types.


---

