# 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\mathcal{U}$ 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 $\Sigma$-type $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x)$. An inhabitant of $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\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 $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\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:A\to\mathcal{U}$ is a type family such that $P(x)$ is a mere proposition for all $x:A$. If $u,v:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A% )}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(% x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum% _{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x)$ are such that $\mathsf{pr}_{1}(u)=\mathsf{pr}_{1}(v)$, then $u=v$.

###### Proof.

Suppose $p:\mathsf{pr}_{1}(u)=\mathsf{pr}_{1}(v)$. By Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1), to show $u=v$ it suffices to show ${p}_{*}\mathopen{}\left({\mathsf{pr}_{2}(u)}\right)\mathclose{}=\mathsf{pr}_{2% }(v)$. But ${p}_{*}\mathopen{}\left({\mathsf{pr}_{2}(u)}\right)\mathclose{}$ and $\mathsf{pr}_{2}(v)$ are both elements of $P(\mathsf{pr}_{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\;\mathchoice{\sum_{f:A\to B}\,}{\mathchoice{{% \textstyle\sum_{(f:A\to B)}}}{\sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}{\sum_{(f:A% \to B)}}}{\mathchoice{{\textstyle\sum_{(f:A\to B)}}}{\sum_{(f:A\to B)}}{\sum_{% (f:A\to B)}}{\sum_{(f:A\to B)}}}{\mathchoice{{\textstyle\sum_{(f:A\to B)}}}{% \sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}}\mathsf{isequiv}(f),$

where each type $\mathsf{isequiv}(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\mathcal{U}$ 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 $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\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 $\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}(P(x)\rightarrow Q(x))$.

As further examples of subtypes, we may define the “subuniverses” of sets and of mere propositions in a universe  $\mathcal{U}$:

 $\displaystyle\mathsf{Set}_{\mathcal{U}}$ $\displaystyle:\!\!\equiv\{A:\mathcal{U}|\mathsf{isSet}(A)\},$ $\displaystyle\mathsf{Prop}_{\mathcal{U}}$ $\displaystyle:\!\!\equiv\{A:\mathcal{U}|\mathsf{isProp}(A)\}.$

An element of $\mathsf{Set}_{\mathcal{U}}$ is a type $A:\mathcal{U}$ together with evidence $s:\mathsf{isSet}(A)$, and similarly for $\mathsf{Prop}_{\mathcal{U}}$. Lemma 3.5.1 (http://planetmath.org/35subsetsandpropositionalresizing#Thmprelem1) implies that $(A,s)=_{\mathsf{Set}_{\mathcal{U}}}(B,t)$ is equivalent     to $A=_{\mathcal{U}}B$ (and hence to $A\simeq B$). Thus, we will frequently abuse notation and write simply $A:\mathsf{Set}_{\mathcal{U}}$ instead of $(A,s):\mathsf{Set}_{\mathcal{U}}$. We may also drop the subscript $\mathcal{U}$ if there is no need to specify the universe in question.

Recall that for any two universes $\mathcal{U}_{i}$ and $\mathcal{U}_{i+1}$, if $A:\mathcal{U}_{i}$ then also $A:\mathcal{U}_{i+1}$. Thus, for any $(A,s):\mathsf{Set}_{\mathcal{U}_{i}}$ we also have $(A,s):\mathsf{Set}_{\mathcal{U}_{i+1}}$, and similarly for $\mathsf{Prop}_{\mathcal{U}_{i}}$, giving natural maps

 $\displaystyle\mathsf{Set}_{\mathcal{U}_{i}}$ $\displaystyle\to\mathsf{Set}_{\mathcal{U}_{i+1}},$ (3.5.3) $\displaystyle\mathsf{Prop}_{\mathcal{U}_{i}}$ $\displaystyle\to\mathsf{Prop}_{\mathcal{U}_{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 $\mathsf{Prop}_{\mathcal{U}_{i}}\to\mathsf{Prop}_{\mathcal{U}_{i+1}}$ is an equivalence.

We refer to this axiom as propositional resizing, since it means that any mere proposition in the universe $\mathcal{U}_{i+1}$ can be “resized” to an equivalent one in the smaller universe $\mathcal{U}_{i}$. It follows automatically if $\mathcal{U}_{i+1}$ satisfies $\mathsf{LEM}$ (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 $\mathcal{U}$ under consideration contains a type which “classifies all mere propositions”. In other words, we want a type $\Omega:\mathcal{U}$ together with an $\Omega$-indexed family of mere propositions, which contains every mere proposition up to equivalence. This statement follows from propositional resizing as stated above if $\mathcal{U}$ is not the smallest universe $\mathcal{U}_{0}$, since then we can define $\Omega:\!\!\equiv\mathsf{Prop}_{\mathcal{U}_{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\mathsf{Prop}_{\mathcal{U}}$; but in the absence of impredicativity, this definition depends (even up to equivalence) on the choice of the universe $\mathcal{U}$. But with propositional resizing, we can define the power set to be

 $\mathcal{P}(A):\!\!\equiv(A\to\Omega),$

which is then independent of $\mathcal{U}$. See also §10.1.4 (http://planetmath.org/1014setisapimathsfwpretopos).

 Title 3.5 Subsets and propositional resizing \metatable