3.5 Subsets and propositional resizing
As another example of the usefulness of mere propositions, we discuss subsets (and more generally subtypes). Suppose is a type family, with each type regarded as a proposition. Then itself is a predicate on , or a property of elements of .
In set theory, whenever we have a predicate on on a set , we may form the subset . In type theory, the obvious analogue is the -type . An inhabitant of is, of course, a pair where and is a proof of . However, for general , an element might give rise to more than one distinct element of , if the proposition has more than one distinct proof. This is counter to the usual intuition of a subset. But if is a mere proposition, then this cannot happen.
Suppose is a type family such that is a mere proposition for all . If are such that , then .
Suppose . By Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1), to show it suffices to show . But and are both elements of , 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 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 is a family of mere propositions (i.e. each is a mere proposition), we may write
as an alternative notation for . (There is no technical reason not to use this notation for arbitrary as well, but such usage could be confusing due to unintended connotations.) If is a set, we call (3.5.2) a subset of ; for general we might call it a subtype. We may also refer to itself as a subset or subtype of ; this is actually more correct, since the type (3.5.2) in isolation doesn’t remember its relationship to .
Given such a and , we may write or to refer to the mere proposition . If it holds, we may say that is a member of . Similarly, if is another subset of , then we say that is contained in , and write , if we have .
As further examples of subtypes, we may define the “subuniverses” of sets and of mere propositions in a universe :
An element of is a type together with evidence , and similarly for . Lemma 3.5.1 (http://planetmath.org/35subsetsandpropositionalresizing#Thmprelem1) implies that is equivalent to (and hence to ). Thus, we will frequently abuse notation and write simply instead of . We may also drop the subscript if there is no need to specify the universe in question.
Recall that for any two universes and , if then also . Thus, for any we also have , and similarly for , giving natural maps
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 is an equivalence.
We refer to this axiom as propositional resizing, since it means that any mere proposition in the universe can be “resized” to an equivalent one in the smaller universe . It follows automatically if 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 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 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 , since then we can define .
One use for impredicativity is to define power sets. It is natural to define the power set of a set to be ; 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|