3.3 Mere propositions

We have seen that the propositions-as-types logic has both good and bad properties. Both have a common cause: when types are viewed as propositions, they can contain more information than mere truth or falsity, and all “logical” constructions on them must respect this additional information. This suggests that we could obtain a more conventional logic by restricting attention to types that do not contain any more information than a truth value, and only regarding these as logical propositions.

Such a type $A$ will be “true” if it is inhabited, and “false” if its inhabitation yields a contradiction (i.e. if $\mathrm{\neg }A\equiv (A\to \mathrm{𝟎})$ is inhabited). What we want to avoid, in order to obtain a more traditional sort of logic, is treating as logical propositions those types for which giving an element of them gives more information than simply knowing that the type is inhabited. For instance, if we are given an element of $\mathrm{𝟐}$, then we receive more information than the mere fact that $\mathrm{𝟐}$ contains some element. Indeed, we receive exactly one bit more information: we know which element of $\mathrm{𝟐}$ we were given. By contrast, if we are given an element of $\mathrm{𝟏}$, then we receive no more information than the mere fact that $\mathrm{𝟏}$ contains an element, since any two elements of $\mathrm{𝟏}$ are equal to each other. This suggests the following definition.

Definition 3.3.1.

A type $P$ is a mere proposition if for all $x\mathrm{,}y\mathrm{:}P$ we have $x\mathrm{=}y$.

Note that since we are still doing mathematics in type theory, this is a definition in type theory, which means it is a type — or, rather, a type family. Specifically, for any $P:𝒰$, the type $\mathrm{𝗂𝗌𝖯𝗋𝗈𝗉}(P)$ is defined to be

$$\mathrm{𝗂𝗌𝖯𝗋𝗈𝗉}(P):\equiv \prod _{x,y:P}(x=y).$$

Thus, to assert that “$P$ is a mere proposition” means to exhibit an inhabitant of $\mathrm{𝗂𝗌𝖯𝗋𝗈𝗉}(P)$, which is a dependent function connecting any two elements of $P$ by a path. The continuity/naturality of this function implies that not only are any two elements of $P$ equal, but $P$ contains no higher homotopy either.

Lemma 3.3.2.

If $P$ is a mere proposition and $x_{\mathrm{0}}\mathrm{:}P$, then $P\mathrm{\simeq }\mathrm{1}$.

Proof.

Define $f:P\to \mathrm{𝟏}$ by $f(x):\equiv \star$, and $g:\mathrm{𝟏}\to P$ by $g(u):\equiv x_0$. The claim follows from the next lemma, and the observation that $\mathrm{𝟏}$ is a mere proposition by Theorem 2.8.1 (http://planetmath.org/28theunittype#S8.Thmthm1). ∎

Lemma 3.3.3.

If $P$ and $Q$ are mere propositions such that $P\mathrm{\to }Q$ and $Q\mathrm{\to }P$, then $P\mathrm{\simeq }Q$.

Proof.

Suppose given $f:P\to Q$ and $g:Q\to P$. Then for any $x:P$, we have $g(f(x))=x$ since $P$ is a mere proposition. Similarly, for any $y:Q$ we have $f(g(y))=y$ since $Q$ is a mere proposition; thus $f$ and $g$ are quasi-inverses. ∎

That is, as promised in §1.11 (http://planetmath.org/111propositionsastypes), if two mere propositions are logically equivalent, then they are equivalent.

In homotopy theory, a space that is homotopy equivalent to $\mathrm{𝟏}$ is said to be contractible. Thus, any mere proposition which is inhabited is contractible (see also §3.11 (http://planetmath.org/311contractibility)). On the other hand, the uninhabited type $\mathrm{𝟎}$ is also (vacuously) a mere proposition. In classical mathematics, at least, these are the only two possibilities.

Mere propositions are also called subterminal objects (if thinking categorically), subsingletons (if thinking set-theoretically), or h-propositions. The discussion in §3.1 (http://planetmath.org/31setsandntypes) suggests we should also call them $\mathrm{(}\mathrm{-}\mathrm{1}\mathrm{)}$-types; we will return to this in http://planetmath.org/node/87580Chapter 7. The adjective “mere” emphasizes that although any type may be regarded as a proposition (which we prove by giving an inhabitant of it), a type that is a mere proposition cannot usefully be regarded as any more than a proposition: there is no additional information contained in a witness of its truth.

Note that a type $A$ is a set if and only if for all $x,y:A$, the identity type $x{=}_{A}y$ is a mere proposition. On the other hand, by copying and simplifying the proof of Lemma 3.1.8 (http://planetmath.org/31setsandntypes#Thmprelem1), we have:

Lemma 3.3.4.

Every mere proposition is a set.

Proof.

Suppose $f:\mathrm{𝗂𝗌𝖯𝗋𝗈𝗉}(A)$; thus for all $x,y:A$ we have $f(x,y):x=y$. Fix $x:A$ and define $g(y):\equiv f(x,y)$. Then for any $y,z:A$ and $p:y=z$ we have ${\mathrm{𝖺𝗉𝖽}}_g\left(p\right):p_{*}\left(g(y)\right)=g(z)$. Hence by Lemma 1 (http://planetmath.org/211identitytype#Thmlem1), we have $g(y)p=g(z)$, which is to say that $p=g{(y)}^{-1}g(z)$. Thus, for any $p,q:x=y$, we have $p=g{(x)}^{-1}g(y)=q$. ∎

In particular, this implies:

Lemma 3.3.5.

For any type $A$, the types $\mathrm{isProp}\mathit{}\mathrm{(}A\mathrm{)}$ and $\mathrm{isSet}\mathit{}\mathrm{(}A\mathrm{)}$ are mere propositions.

Proof.

Suppose $f,g:\mathrm{𝗂𝗌𝖯𝗋𝗈𝗉}(A)$. By function extensionality, to show $f=g$ it suffices to show $f(x,y)=g(x,y)$ for any $x,y:A$. But $f(x,y)$ and $g(x,y)$ are both paths in $A$, and hence are equal because, by either $f$ or $g$, we have that $A$ is a mere proposition, and hence by Lemma 3.3.4 (http://planetmath.org/33merepropositions#Thmprelem3) is a set. Similarly, suppose $f,g:\mathrm{𝗂𝗌𝖲𝖾𝗍}(A)$, which is to say that for all $a,b:A$ and $p,q:a=b$, we have $f(a,b,p,q):p=q$ and $g(a,b,p,q):p=q$. But by then since $A$ is a set (by either $f$ or $g$), and hence a 1-type, it follows that $f(a,b,p,q)=g(a,b,p,q)$; hence $f=g$ by function extensionality. ∎

We have seen one other example so far: condition (3.) (http://planetmath.org/24homotopiesandequivalences#I1.i3) in §2.4 (http://planetmath.org/24homotopiesandequivalences) asserts that for any function $f$, the type $\mathrm{𝗂𝗌𝖾𝗊𝗎𝗂𝗏}(f)$ should be a mere proposition.

Title	3.3 Mere propositions