<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:

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](https://i.sstatic.net/TnWMG.png)](https://i.sstatic.net/TnWMG.png)

**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.


---

