From $\textsf{Prop}$ to $\textsf{Type}$

homotopy-type-theorytype-theory

Let $P,\top:\textsf{Prop}$ (where $\textsf{Prop}$ is the universe of mere propositions), $A=\{P,\neg P\}:\textsf{Type}$ and $B$ is an identity function such that $B(x)=x$. Given the above definitions, $(\star)$ trivially holds.
$$P\rightarrow(\top\rightarrow\Sigma x:A.B(x))\tag{$\star$}$$
By the distribution axiom of $\rightarrow$, we obtain the following:
$$(P\rightarrow\top)\rightarrow(P\rightarrow\Sigma x:A.B(x)).\tag{$\star\star$}$$
But this seems odd to me because $P\rightarrow\top$ is a mere proposition by definition but $P\rightarrow\Sigma x:A.B(x)$ is not a mere proposition but just a type. Thus, it shows that from a proof of a mere proposition (that is proof-irrelevant), we obtain a proof of a type (that is proof-relevant). This appears odd but it is natural in $(\star\star)$.

My question is: what amounts to a general condition for a proof-irrelevant type (of $\textsf{Prop}$) to imply a proof-relevant type such as in $(\star\star)$? Thanks!

Best Answer

$\newcommand{\inj}{\mathsf{inj}}$ $\newcommand{\refl}{\mathsf{refl}}$ $\newcommand{\isProp}{\mathsf{isProp}}$ $\newcommand{\isContr}{\mathsf{isContr}}$

I'm not sure exactly of the source of confusion, but here are some things to think about.

  1. $⊤ → A$ is equivalent to $A$, so your $(\star)$ is already equivalent to $P → Σx:A.B(x)$

  2. Your $(*)$ already has two propositions implying $Σx:A.B(x)$, so it doesn't seem unreasonable that one proposition would imply it (especially since $⊤$ is rather vacuous).

  3. Some non-propositions are easy to exhibit from any proposition. For instance, $λ x. 0$ has type $⊤ → ℕ$

  4. $P$ actually implies that $T = Σx:A.B(x)$ is contractible (and thus a proposition) by the following argument:

    • I presumed $A$ means something equivalent to $ΣX:\mathcal U. \Vert (P=X)+(¬P=X) \Vert$ and so $B$ is $π_1$
    • $T$ is inhabited by $(P, \vert ι_1 \refl \vert, p)$, where $p$ is the premise. Let $(X, t, x)$ be some other witness
    • $P = X$ is a propsition because $P$ is, using $(B → \isProp(B)) → \isProp(B)$ with $B := (P = X)$
    • This allows us to deduce that $P = X$ using the truncated witness, because $p$ and $x$ together refute $¬P = X$
    • $p$ is related to $x$ by the path from $P$ to $X$ because $P$ and $X$ are propositions
    • The two truncated witnesses are related because the truncated types are propositions
    • Thus, $(X, t, x)$ is equal to our center of contraction

  5. $¬P$ implies that $T$ is contractible by a very similar argument

  6. $T → \isContr(T)$, because $T$ gives us a value $x : X$, $\isContr(T)$ is a proposition, and by cases on $(P=X)+(¬P=X)$, we can get either a value of $P$ or a value of $¬P$ to use 4 or 5

  7. Thus $T$ is a proposition, because $(T → \isContr(T)) → \isProp(T)$. Here is a cubical Agda formalization.

However, the fact that $Σx:A.B(x)$ is actually a proposition is incidental. If the source of your question is an idea that propositions in HoTT are somehow restricted so that they may be 'erased', as in various other type theories, you should abandon that. A key feature of HoTT is that 'proof irrelevant' does not mean 'computationally irrelevant.' Mere propositions are proof irrelevant in the sense that for any two proofs $p, q$, any construction on $p$ can be systematically translated to an equivalent construction on $q$. However, this does not mean that $p$ and $q$ have no computational content.

An example of this is finite sets. One can define the type of finite sets as:

$$ΣX:\mathcal U. \Vert Σn:ℕ. \mathsf{Fin}(n) \simeq X \Vert$$

I.E. it is the collection of types that are merely equivalent to some set of a particular finite size. However, it can be shown that for a given such $X$, $n$ is unique, and may be extracted from the truncation. There is no mechanism for deducing the size $n$ from $X : \mathcal U$, so the conclusion is that the truncation was carrying it (at least, if you are expecting a computational explanation). There are just obligations for accessing it.

I don't think there is necessarily a general description of 'when a proposition can imply a non-proposition,' though. Propositions aren't arbitrarily separated/distinguished in HoTT. They are just types with a certain defined property, and there are multiple conceptual reasons a type might have that property.

Related Question