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→𝒰 is a type family, with each type P⁒(x) regarded as a propositionPlanetmathPlanetmathPlanetmath. Then P itself is a predicateMathworldPlanetmath on A, or a property of elements of A.

In set theoryMathworldPlanetmath, whenever we have a predicate on P on a set A, we may form the subset {x∈A|P⁒(x)}. In type theoryPlanetmathPlanetmath, the obvious analogue is the Ξ£-type βˆ‘(x:A)P⁒(x). An inhabitant of βˆ‘(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 βˆ‘(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β†’U is a type family such that P⁒(x) is a mere proposition for all x:A. If u,v:βˆ‘(x:A)P⁒(x) are such that pr1⁒(u)=pr1⁒(v), then u=v.


Suppose p:𝗉𝗋1⁒(u)=𝗉𝗋1⁒(v). By Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1), to show u=v it suffices to show p*(𝗉𝗋2(u))=𝗉𝗋2(v). But p*(𝗉𝗋2(u)) and 𝗉𝗋2⁒(v) are both elements of P⁒(𝗉𝗋1⁒(v)), which is a mere proposition; hence they are equal. ∎

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


where each type π—‚π—Œπ–Ύπ—Šπ—Žπ—‚π—β’(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→𝒰 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 βˆ‘(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∈P or a∈{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βŠ†Q, if we have ∏(x:A)(P(x)β†’Q(x)).

As further examples of subtypes, we may define the β€œsubuniverses” of sets and of mere propositions in a universePlanetmathPlanetmath 𝒰:

𝖲𝖾𝗍𝒰 :≑{A:𝒰|π—‚π—Œπ–²π–Ύπ—(A)},
π–―π—‹π—ˆπ—‰π’° :≑{A:𝒰|π—‚π—Œπ–―π—‹π—ˆπ—‰(A)}.

An element of 𝖲𝖾𝗍𝒰 is a type A:𝒰 together with evidence s:π—‚π—Œπ–²π–Ύπ—β’(A), and similarly for π–―π—‹π—ˆπ—‰π’°. Lemma 3.5.1 (http://planetmath.org/35subsetsandpropositionalresizing#Thmprelem1) implies that (A,s)=𝖲𝖾𝗍𝒰(B,t) is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to A=𝒰B (and hence to A≃B). Thus, we will frequently abuse notation and write simply A:𝖲𝖾𝗍𝒰 instead of (A,s):𝖲𝖾𝗍𝒰. 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):𝖲𝖾𝗍𝒰i we also have (A,s):𝖲𝖾𝗍𝒰i+1, and similarly for π–―π—‹π—ˆπ—‰π’°i, giving natural maps

𝖲𝖾𝗍𝒰i →𝖲𝖾𝗍𝒰i+1, (3.5.3)
π–―π—‹π—ˆπ—‰π’°i β†’π–―π—‹π—ˆπ—‰π’°i+1. (3.5.3)

The mapΒ (3.5.3) cannot be an equivalence, since then we could reproduce the paradoxesMathworldPlanetmath 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 PropUi→PropUi+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 𝖫𝖀𝖬 (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 hypothesisMathworldPlanetmathPlanetmath. 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 Ξ©:𝒰 together with an Ξ©-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 Ξ©:β‰‘π–―π—‹π—ˆπ—‰π’°0.

One use for impredicativity is to define power setsMathworldPlanetmath. It is natural to define the power set of a set A to be Aβ†’π–―π—‹π—ˆπ—‰π’°; 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


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

Title 3.5 Subsets and propositional resizing