7.1 Definition of n-types


As mentioned in §3.1 (http://planetmath.org/31setsandntypes),§3.11 (http://planetmath.org/311contractibility), it turns out to be convenient to define n-types starting two levels below zero, with the (-1)-types being the mere propositions and the (-2)-types the contractible ones.

Definition 7.1.1.

Define the predicateMathworldPlanetmathPlanetmath is-n-type:UU for n-2 by recursion as follows:

𝗂𝗌-n-𝗍𝗒𝗉𝖾(X):{𝗂𝗌𝖢𝗈𝗇𝗍𝗋(X) if n=-2,(x,y:X)𝗂𝗌-n-𝗍𝗒𝗉𝖾(x=Xy) if n=n+1.

We say that X is an n-type, or sometimes that it is n-truncated, if is-n-type(X) is inhabited.

Remark 7.1.2.

The number n in Definition 7.1.1 (http://planetmath.org/71definitionofntypes#Thmpredefn1) ranges over all integers greater than or equal to -2. We could make sense of this formally by defining a type Z-2 of such integers (a type whose inductionMathworldPlanetmath principle is identical to that of N), or instead defining a predicate is-(k-2)-type for k:N. Either way, we can prove theoremsMathworldPlanetmath about n-types by induction on n, with n=-2 as the base case.

Example 7.1.3.

We saw in Lemma 3.11.10 (http://planetmath.org/311contractibility#Thmprelem7) that X is a (-1)-type if and only if it is a mere proposition. Therefore, X is a 0-type if and only if it is a set.

We have also seen that there are types which are not sets (Example 3.1.9 (http://planetmath.org/31setsandntypes#Thmpreeg6)). So far, however, we have not shown for any n>0 that there exist types which are not n-types. In http://planetmath.org/node/87582Chapter 8, however, we will show that the (n+1)-sphere 𝕊n+1 is not an n-type. (Kraus has also shown that the nth nested univalent universePlanetmathPlanetmath is also not an n-type, without using any higher inductive types.) Moreover, in §8.8 (http://planetmath.org/88whiteheadstheoremandwhiteheadsprinciple) will give an example of a type that is not an n-type for any (finite) number n.

We begin the general theory of n-types by showing they are closed under certain operations and constructors.

Theorem 7.1.4.

Let p:XY be a retractionMathworldPlanetmath and suppose that X is an n-type, for any n-2. Then Y is also an n-type.

Proof.

We proceed by induction on n. The base case n=-2 is handled by Lemma 3.11.7 (http://planetmath.org/311contractibility#Thmprelem4).

For the inductive step, assume that any retract of an n-type is an n-type, and that X is an (n+1)-type. Let y,y:Y; we must show that y=y is an n-type. Let s be a sectionPlanetmathPlanetmath of p, and let ϵ be a homotopy ϵ:ps1. Since X is an (n+1)-type, s(y)=Xs(y) is an n-type. We claim that y=y is a retract of s(y)=Xs(y). For the section, we take

𝖺𝗉s:(y=y)(s(y)=s(y)).

For the retraction, we define t:(s(y)=s(y))(y=y) by

t(q):ϵy-1\centerdotp(q)\centerdotϵy.

To show that t is a retraction of 𝖺𝗉s, we must show that

ϵy-1\centerdotp(s(r))\centerdotϵy=r

for any r:y=y. But this follows from Lemma 2.4.3 (http://planetmath.org/24homotopiesandequivalences#Thmprelem2). ∎

As an immediate corollary we obtain the stability of n-types under equivalence (which is also immediate from univalence):

Corollary 7.1.5.

If XY and X is an n-type, then so is Y.

Recall also the notion of embeddingMathworldPlanetmathPlanetmath from §4.6 (http://planetmath.org/46surjectionsandembeddings).

Theorem 7.1.6.

If f:XY is an embedding and Y is an n-type for some n-1, then so is X.

Proof.

Let x,x:X; we must show that x=Xx is an (n-1)-type. But since f is an embedding, we have (x=Xx)(f(x)=Yf(x)), and the latter is an (n-1)-type by assumptionPlanetmathPlanetmath. ∎

Note that this theorem fails when n=-2: the map 𝟎𝟏 is an embedding, but 𝟏 is a (-2)-type while 𝟎 is not.

Theorem 7.1.7.

The hierarchy of n-types is cumulative in the following sense: given a number n-2, if X is an n-type, then it is also an (n+1)-type.

Proof.

We proceed by induction on n.

For n=-2, we need to show that a contractible type, say, A, has contractible path spaces. Let a0:A be the center of contraction of A, and let x,y:A. We show that x=Ay is contractible. By contractibility of A we have a path 𝖼𝗈𝗇𝗍𝗋x\centerdot𝖼𝗈𝗇𝗍𝗋y-1:x=y, which we choose as the center of contraction for x=y. Given any p:x=y, we need to show p=𝖼𝗈𝗇𝗍𝗋x\centerdot𝖼𝗈𝗇𝗍𝗋y-1. By path induction, it suffices to show that 𝗋𝖾𝖿𝗅x=𝖼𝗈𝗇𝗍𝗋x\centerdot𝖼𝗈𝗇𝗍𝗋x-1, which is trivial.

For the inductive step, we need to show that x=Xy is an (n+1)-type, provided that X is an (n+1)-type. Applying the inductive hypothesis to x=Xy yields the desired result. ∎

We now show that n-types are preserved by most of the type forming operations.

Theorem 7.1.8.

Let n-2, and let A:U and B:AU. If A is an n-type and for all a:A, B(a) is an n-type, then so is (x:A)B(x).

Proof.

We proceed by induction on n.

For n=-2, we choose the center of contraction for (x:A)B(x) to be the pair (a0,b0), where a0:A is the center of contraction of A and b0:B(a0) is the center of contraction of B(a0). Given any other element (a,b) of (x:A)B(x), we provide a path (a,b)=(a0,b0) by contractibility of A and B(a0), respectively.

For the inductive step, suppose that A is an (n+1)-type and for any a:A, B(a) is an (n+1)-type. We show that (x:A)B(x) is an (n+1)-type: fix (a1,b1) and (a2,b2) in (x:A)B(x), we show that (a1,b1)=(a2,b2) is an n-type. By Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1) we have

((a1,b1)=(a2,b2))p:a1=a2(p*(b1)=B(a2)b2)

and by preservation of n-types under equivalences (Corollary 7.1.5 (http://planetmath.org/71definitionofntypes#Thmprecor1)) it suffices to prove that the latter is an n-type. This follows from the inductive hypothesis. ∎

As a special case, if A and B are n-types, so is A×B. Note also that Theorem 7.1.7 (http://planetmath.org/71definitionofntypes#Thmprethm3) implies that if A is an n-type, then so is x=Ay for any x,y:A. Combining this with Theorem 7.1.8 (http://planetmath.org/71definitionofntypes#Thmprethm4), we see that for any functions f:AC and g:BC between n-types, their pullback

A×CB:(x:A)(y:B)(f(x)=g(y))

(see http://planetmath.org/node/87642Exercise 2.11) is also an n-type. More generally, n-types are closed under all limits.

Theorem 7.1.9.

Let n-2, and let A:U and B:AU. If for all a:A, B(a) is an n-type, then so is (x:A)B(x).

Proof.

We proceed by induction on n. For n=-2, the result is simply Lemma 3.11.6 (http://planetmath.org/311contractibility#Thmprelem3).

For the inductive step, assume the result is true for n-types, and that each B(a) is an (n+1)-type. Let f,g:(a:A)B(a). We need to show that f=g is an n-type. By function extensionality and closureMathworldPlanetmathPlanetmath of n-types under equivalence, it suffices to show that (a:A)(f(a)=B(a)g(a)) is an n-type. This follows from the inductive hypothesis. ∎

As a special case of the above theorem, the function space AB is an n-type provided that B is an n-type. We can now generalize our observations in http://planetmath.org/node/87569Chapter 2 that 𝗂𝗌𝖲𝖾𝗍(A) and 𝗂𝗌𝖯𝗋𝗈𝗉(A) are mere propositions.

Theorem 7.1.10.

For any n-2 and any type X, the type is-n-type(X) is a mere proposition.

Proof.

We proceed by induction with respect to n.

For the base case, we need to show that for any X, the type 𝗂𝗌𝖢𝗈𝗇𝗍𝗋(X) is a mere proposition. This is Lemma 3.11.4 (http://planetmath.org/311contractibility#Thmprelem2).

For the inductive step we need to show

X:𝒰𝗂𝗌𝖯𝗋𝗈𝗉(𝗂𝗌-n-𝗍𝗒𝗉𝖾(X))X:𝒰𝗂𝗌𝖯𝗋𝗈𝗉(𝗂𝗌-(n+1)-𝗍𝗒𝗉𝖾(X))

To show the conclusion of this implicationMathworldPlanetmath, we need to show that for any type X, the type

x,x:X𝗂𝗌-n-𝗍𝗒𝗉𝖾(x=x)

is a mere proposition. By Example 3.6.2 (http://planetmath.org/36thelogicofmerepropositions#Thmpreeg2) or Theorem 7.1.9 (http://planetmath.org/71definitionofntypes#Thmprethm5), it suffices to show that for any x,x:X, the type 𝗂𝗌-n-𝗍𝗒𝗉𝖾(x=Xx) is a mere proposition. But this follows from the inductive hypothesis applied to the type (x=Xx). ∎

Finally, we show that the type of n-types is itself an (n+1)-type. We define this to be:

n-𝖳𝗒𝗉𝖾:X:𝒰𝗂𝗌-n-𝗍𝗒𝗉𝖾(X)

If necessary, we may specify the universe 𝒰 by writing n-𝖳𝗒𝗉𝖾𝒰. In particular, we have 𝖯𝗋𝗈𝗉:(-1)-𝖳𝗒𝗉𝖾 and 𝖲𝖾𝗍:0-𝖳𝗒𝗉𝖾, as defined in http://planetmath.org/node/87569Chapter 2. Note that just as for 𝖯𝗋𝗈𝗉 and 𝖲𝖾𝗍, because 𝗂𝗌-n-𝗍𝗒𝗉𝖾(X) is a mere proposition, by Lemma 3.5.1 (http://planetmath.org/35subsetsandpropositionalresizing#Thmprelem1) for any (X,p),(X,p):n-𝖳𝗒𝗉𝖾 we have

((X,p)=n-𝖳𝗒𝗉𝖾(X,p)) (X=𝒰X)
(XX).
Theorem 7.1.11.

For any n-2, the type n-Type is an (n+1)-type.

Proof.

Let (X,p),(X,p):n-𝖳𝗒𝗉𝖾; we need to show that (X,p)=(X,p) is an n-type. By the above observation, this type is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to XX. Next, we observe that the projection

(XX)(XX).

is an embedding, so that if n-1, then by Theorem 7.1.6 (http://planetmath.org/71definitionofntypes#Thmprethm2) it suffices to show that XX is an n-type. But since n-types are preserved under the arrow type, this reduces to an assumption that X is an n-type.

In the case n=-2, this argumentMathworldPlanetmath shows that XX is a (-1)-type — but it is also inhabited, since any two contractible types are equivalent to 𝟏, and hence to each other. Thus, XX is also a (-2)-type. ∎

Title 7.1 Definition of n-types
\metatable