Post History

Interpreting $\text{Prop}$ in Set

Consider a type theory with a universe $\text{Prop}$ of logical propositions (for now, it is not necessarily impredicative). Write $\text{T}$ for the decoding function for this universe.

If we stipulate proof irrelevance (i.e., say that for any $P:\text{Prop}$ and any two terms $a,b:\text{T}(P)$, we have $a=b$), then we can consider set models in which $\text{Prop}$ is interpreted as a two-element set, say $\{t,f\}$, and for every $P:\text{Prop}$, $\text{T}(P)$ is interpreted as the set $\{\emptyset, \{*\}\}$. In such set models, a proposition $P:\text{Prop}$ would be interpreted as $t$ if $\text{T}(P)$ is interpreted as $\{*\}$ and as $f$ if $\text{T}(P)$ is interpreted as $\emptyset$.

Is it possible to do the same (in some sense) if proof irrelevance is not stipulated? I believe we can still interpret $\text{Prop}$ as $\{t,f\}$, but if there is no proof irrelevance, there may be as many terms of type $\text{T}(P)$ (where $P:\text{Prop}$) as we wish, and thus it is not clear which set we should interpret $\text{T}(P)$ as. (The only thing that is clear is that the interpretation of $\text{T}(P)$ should contain the empty set.) And then if we know how to interpret $\text{T}(P)$, how should we interpret propositions? Would it be enough to just say that $P$ is interpreted as $f$ if the interpretation of $\text{T}(P)$ is $\emptyset$ and as $t$ otherwise?

And a related question: Does the answer to the question(s) in the previous paragraph depend on whether $\text{Prop}$ is predicative or impredicative? In [this stack of slides](https://math.colorado.edu/~chme3268/assets/documents/type-theory.pdf) it is said that impredicativity is only possible if $\text{Prop}$ "is" $\{\emptyset,\{*\}\}$, but it's not clarified what "is" means here.