3.5 Subsets and propositional resizing

As another example of the usefulness of mere propositions, we discuss subsets (and more generally subtypes). Suppose $P:A\to 𝒰$ is a type family, with each type $P(x)$ regarded as a proposition. Then $P$ itself is a predicate on $A$, or a property of elements of $A$.

In set theory, whenever we have a predicate on $P$ on a set $A$, we may form the subset $\{x\in A|P(x)\}$. In type theory, the obvious analogue is the $\mathrm{\Sigma }$-type ${\sum }_{(x:A)}P(x)$. An inhabitant of ${\sum }_{(x:A)}P(x)$ is, of course, a pair $(x,p)$ where $x:A$ and $p$ is a proof of $P(x)$. However, for general $P$, an element $a:A$ might give rise to more than one distinct element of ${\sum }_{(x:A)}P(x)$, if the proposition $P(a)$ has more than one distinct proof. This is counter to the usual intuition of a subset. But if $P$ is a mere proposition, then this cannot happen.

Lemma 3.5.1.

Suppose $P\mathrm{:}A\mathrm{\to }\mathrm{U}$ is a type family such that $P\mathit{}\mathrm{(}x\mathrm{)}$ is a mere proposition for all $x\mathrm{:}A$. If $u\mathrm{,}v\mathrm{:}{\mathrm{\sum }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}P\mathit{}\mathrm{(}x\mathrm{)}$ are such that ${\mathrm{pr}}_{\mathrm{1}}\mathit{}\mathrm{(}u\mathrm{)}\mathrm{=}{\mathrm{pr}}_{\mathrm{1}}\mathit{}\mathrm{(}v\mathrm{)}$, then $u\mathrm{=}v$.

Proof.

Suppose $p:{\mathrm{𝗉𝗋}}_1(u)={\mathrm{𝗉𝗋}}_1(v)$. By Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1), to show $u=v$ it suffices to show $p_{*}\left({\mathrm{𝗉𝗋}}_2(u)\right)={\mathrm{𝗉𝗋}}_2(v)$. But $p_{*}\left({\mathrm{𝗉𝗋}}_2(u)\right)$ and ${\mathrm{𝗉𝗋}}_2(v)$ are both elements of $P({\mathrm{𝗉𝗋}}_1(v))$, which is a mere proposition; hence they are equal. ∎

For instance, recall that in §2.4 (http://planetmath.org/24homotopiesandequivalences) we defined

$$(A\simeq B):\equiv \sum _{f:A\to B}\mathrm{𝗂𝗌𝖾𝗊𝗎𝗂𝗏}(f),$$

where each type $\mathrm{𝗂𝗌𝖾𝗊𝗎𝗂𝗏}(f)$ was supposed to be a mere proposition. It follows that if two equivalences have equal underlying functions, then they are equal as equivalences.

Henceforth, if $P:A\to 𝒰$ is a family of mere propositions (i.e. each $P(x)$ is a mere proposition), we may write

$$\{x:A|P(x)\}$$ (3.5.2)

as an alternative notation for ${\sum }_{(x:A)}P(x)$. (There is no technical reason not to use this notation for arbitrary $P$ as well, but such usage could be confusing due to unintended connotations.) If $A$ is a set, we call (3.5.2) a subset of $A$; for general $A$ we might call it a subtype. We may also refer to $P$ itself as a subset or subtype of $A$; this is actually more correct, since the type (3.5.2) in isolation doesn’t remember its relationship to $A$.

Given such a $P$ and $a:A$, we may write $a\in P$ or $a\in \{x:A|P(x)\}$ to refer to the mere proposition $P(a)$. If it holds, we may say that $a$ is a member of $P$. Similarly, if $\{x:A|Q(x)\}$ is another subset of $A$, then we say that $P$ is contained in $Q$, and write $P\subseteq Q$, if we have ${\prod }_{(x:A)}(P(x)\to Q(x))$.

As further examples of subtypes, we may define the “subuniverses” of sets and of mere propositions in a universe $𝒰$:

${\mathrm{𝖲𝖾𝗍}}_{𝒰}$ $:\equiv \{A:𝒰|\mathrm{𝗂𝗌𝖲𝖾𝗍}(A)\},$

${\mathrm{𝖯𝗋𝗈𝗉}}_{𝒰}$ $:\equiv \{A:𝒰|\mathrm{𝗂𝗌𝖯𝗋𝗈𝗉}(A)\}.$

An element of ${\mathrm{𝖲𝖾𝗍}}_{𝒰}$ is a type $A:𝒰$ together with evidence $s:\mathrm{𝗂𝗌𝖲𝖾𝗍}(A)$, and similarly for ${\mathrm{𝖯𝗋𝗈𝗉}}_{𝒰}$. Lemma 3.5.1 (http://planetmath.org/35subsetsandpropositionalresizing#Thmprelem1) implies that $(A,s){=}_{{\mathrm{𝖲𝖾𝗍}}_{𝒰}}(B,t)$ is equivalent to $A{=}_{𝒰}B$ (and hence to $A\simeq B$). Thus, we will frequently abuse notation and write simply $A:{\mathrm{𝖲𝖾𝗍}}_{𝒰}$ instead of $(A,s):{\mathrm{𝖲𝖾𝗍}}_{𝒰}$. We may also drop the subscript $𝒰$ if there is no need to specify the universe in question.

Recall that for any two universes ${𝒰}_i$ and ${𝒰}_{i+1}$, if $A:{𝒰}_i$ then also $A:{𝒰}_{i+1}$. Thus, for any $(A,s):{\mathrm{𝖲𝖾𝗍}}_{{𝒰}_i}$ we also have $(A,s):{\mathrm{𝖲𝖾𝗍}}_{{𝒰}_{i+1}}$, and similarly for ${\mathrm{𝖯𝗋𝗈𝗉}}_{{𝒰}_i}$, giving natural maps

${\mathrm{𝖲𝖾𝗍}}_{{𝒰}_i}$ $\to {\mathrm{𝖲𝖾𝗍}}_{{𝒰}_{i+1}},$ (3.5.3)

${\mathrm{𝖯𝗋𝗈𝗉}}_{{𝒰}_i}$ $\to {\mathrm{𝖯𝗋𝗈𝗉}}_{{𝒰}_{i+1}}.$ (3.5.3)

The map (3.5.3) cannot be an equivalence, since then we could reproduce the paradoxes of self-reference that are familiar from Cantorian set theory. However, although (3.5.3) is not automatically an equivalence in the type theory we have presented so far, it is consistent to suppose that it is. That is, we may consider adding to type theory the following axiom.

Axiom 3.5.3 (Propositional resizing).

The map ${\mathrm{Prop}}_{{\mathrm{U}}_i}\mathrm{\to }{\mathrm{Prop}}_{{\mathrm{U}}_{i\mathrm{+}\mathrm{1}}}$ is an equivalence.

We refer to this axiom as propositional resizing, since it means that any mere proposition in the universe ${𝒰}_{i+1}$ can be “resized” to an equivalent one in the smaller universe ${𝒰}_i$. It follows automatically if ${𝒰}_{i+1}$ satisfies $\mathrm{𝖫𝖤𝖬}$ (see http://planetmath.org/node/87770Exercise 3.13). We will not assume this axiom in general, although in some places we will use it as an explicit hypothesis. It is a form of impredicativity for mere propositions, and by avoiding its use, the type theory is said to remain predicative.

In practice, what we want most frequently is a slightly different statement: that a universe $𝒰$ under consideration contains a type which “classifies all mere propositions”. In other words, we want a type $\mathrm{\Omega }:𝒰$ together with an $\mathrm{\Omega }$-indexed family of mere propositions, which contains every mere proposition up to equivalence. This statement follows from propositional resizing as stated above if $𝒰$ is not the smallest universe ${𝒰}_0$, since then we can define $\mathrm{\Omega }:\equiv {\mathrm{𝖯𝗋𝗈𝗉}}_{{𝒰}_0}$.

One use for impredicativity is to define power sets. It is natural to define the power set of a set $A$ to be $A\to {\mathrm{𝖯𝗋𝗈𝗉}}_{𝒰}$; but in the absence of impredicativity, this definition depends (even up to equivalence) on the choice of the universe $𝒰$. But with propositional resizing, we can define the power set to be

$$𝒫(A):\equiv (A\to \mathrm{\Omega }),$$

which is then independent of $𝒰$. See also §10.1.4 (http://planetmath.org/1014setisapimathsfwpretopos).

Title	3.5 Subsets and propositional resizing