hlevels.tex

\chapter{Homotopy \texorpdfstring{$n$}{n}-types}
\label{cha:hlevels}

\index{n-type@$n$-type|(}%
\indexsee{h-level}{$n$-type}

One of the basic notions of homotopy theory is that of a \emph{homotopy $n$-type}: a space containing no interesting homotopy above dimension $n$.
For instance, a homotopy $0$-type is essentially a set, containing no nontrivial paths, while a homotopy $1$-type may contain nontrivial paths, but no nontrivial paths between paths.
Homotopy $n$-types are also called \emph{$n$-truncated spaces}.
We have mentioned this notion already in \cref{sec:basics-sets}; our first goal in this chapter is to give it a precise definition in homotopy type theory.

A dual notion to truncatedness is connectedness: a space is \emph{$n$-connected} if it has no interesting homotopy in dimensions $n$ and \emph{below}.
For instance, a space is $0$-connected (also called just ``connected'') if it has only one connected component, and $1$-connected (also called ``simply connected'') if it also has no nontrivial loops (though it may have nontrivial higher loops between loops\index{loop!n-@$n$-}).

The duality between truncatedness and connectedness is most easily seen by extending both notions to maps.
We call a map \emph{$n$-truncated} or \emph{$n$-connected} if all its fibers are so.
Then $n$-connected and $n$-truncated maps form the two classes of maps in an \emph{orthogonal factorization system},
\index{orthogonal factorization system}
\indexsee{factorization!system, orthogonal}{orthogonal factorization system}
i.e.\ every map factors uniquely as an $n$-connected map followed by an $n$-truncated one.

In the case $n={-1}$, the $n$-truncated maps are the embeddings and the $n$-connected maps are the surjections, as defined in \cref{sec:mono-surj}.
Thus, the $n$-connected factorization system is a massive generalization of the standard image factorization of a function between sets into a surjection followed by an injection.
At the end of this chapter, we sketch briefly an even more general theory: any type-theoretic \emph{modality} gives rise to an analogous factorization system.


\section{Definition of \texorpdfstring{$n$}{n}-types}
\label{sec:n-types}

As mentioned in \cref{sec:basics-sets,sec:contractibility}, 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.

\begin{defn}\label{def:hlevel}
  Define the predicate $\istype{n} : \type \to \type$ for $n \geq -2$ by recursion as follows:
  \[ \istype{n}(X) \defeq
  \begin{cases}
    \iscontr(X) & \text{ if } n = -2, \\
    \prd{x,y : X} \istype{n'}(\id[X]{x}{y}) & \text{ if } n = n'+1.
  \end{cases}
  \]
  We say that $X$ is an \define{$n$-type}, or sometimes that it is \emph{$n$-truncated},
  \indexdef{n-type@$n$-type}%
  \indexsee{n-truncated@$n$-truncated!type}{$n$-type}%
  \indexsee{type!n-type@$n$-type}{$n$-type}%
  \indexsee{type!n-truncated@$n$-truncated}{$n$-type}%
 if $\istype{n}(X)$ is inhabited.
\end{defn}

\begin{rmk}
  The number $n$ in \cref{def:hlevel} ranges over all integers greater than or equal to $-2$.
  We could make sense of this formally by defining a type $\Z_{{\geq}-2}$ of such integers (a type whose induction principle is identical to that of $\nat$), or instead defining a predicate $\istype{(k-2)}$ for $k : \nat$.
  Either way, we can prove theorems about $n$-types by induction on $n$, with $n = -2$ as the base case.
\end{rmk}

\begin{eg}
  \index{set}
  We saw in \cref{thm:prop-minusonetype} 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.
\end{eg}

We have also seen that there are types which are not sets (\cref{thm:type-is-not-a-set}).
So far, however, we have not shown for any $n>0$ that there exist types which are not $n$-types.
In \cref{cha:homotopy}, however, we will show that the $(n+1)$-sphere $\Sn^{n+1}$ is not an $n$-type.
(Kraus has also shown that the $n^{\mathrm{th}}$ nested univalent universe is also not an $n$-type, without using any higher inductive types.)
Moreover, in \cref{sec:whitehead} will give an example of a type that is not an $n$-type for \emph{any} (finite) number $n$.

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

\begin{thm}\label{thm:h-level-retracts}
  \index{retract!of a type}%
  \index{retraction}%
 Let $p : X \to Y$ be a retraction and suppose that $X$ is an $n$-type, for any $n\geq -2$.
 Then $Y$ is also an $n$-type.
\end{thm}

\begin{proof}
 We proceed by induction on $n$.
 The base case $n=-2$ is handled by \cref{thm:retract-contr}.

 For the inductive step, assume that any retract of an $n$-type is an $n$-type, and that $X$ is an $\nplusone$-type.
 Let $y, y' : Y$; we must show that $\id{y}{y'}$ is an $n$-type.
 Let $s$ be a section of $p$, and let $\epsilon$ be a homotopy $\epsilon : p \circ s \htpy 1$.
 Since $X$ is an $\nplusone$-type, $\id[X]{s(y)}{s(y')}$ is an $n$-type.
 We claim that $\id{y}{y'}$ is a retract of $\id[X]{s(y)}{s(y')}$.
 For the section, we take
 \[ \apfunc s : (y=y') \to (s(y)=s(y')). \]
 For the retraction, we define $t:(s(y)=s(y'))\to(y=y')$ by
 \[ t(q) \defeq  \opp{\epsilon_y} \ct \ap p q \ct \epsilon_{y'}.\]
 To show that $t$ is a retraction of $\apfunc s$, we must show that
 \[ \opp{\epsilon_y} \ct \ap p {\ap sr} \ct \epsilon_{y'} = r \]
 for any $r:y=y'$.
 But this follows from \cref{lem:htpy-natural}.
\end{proof}

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

\begin{cor}\label{cor:preservation-hlevels-weq}
 If $\eqv{X}{Y}$ and $X$ is an $n$-type, then so is $Y$.
\end{cor}

Recall also the notion of embedding from \cref{sec:mono-surj}.

\begin{thm}\label{thm:isntype-mono}
  \index{function!embedding}
  If $f:X\to Y$ is an embedding and $Y$ is an $n$-type for some $n\ge -1$, then so is $X$.
\end{thm}
\begin{proof}
  Let $x,x':X$; we must show that $\id[X]{x}{x'}$ is an $\nminusone$-type.
  But since $f$ is an embedding, we have $(\id[X]{x}{x'}) \eqvsym (\id[Y]{f(x)}{f(x')})$, and the latter is an $\nminusone$-type by assumption.
\end{proof}

Note that this theorem fails when $n=-2$: the map $\emptyt \to \unit$ is an embedding, but $\unit$ is a $(-2)$-type while $\emptyt$ is not.

\begin{thm}\label{thm:hlevel-cumulative}
 The hierarchy of $n$-types is cumulative in the following sense:
   given a number $n \geq -2$, if $X$ is an $n$-type, then it is also an $\nplusone$-type.
\end{thm}

\begin{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 $a_0: A$ be the center of contraction of $A$, and let $x, y : A$. We show that $\id[A]{x}{y}$
       is contractible.
       By contractibility of $A$ we have a path $\contr_x \ct \opp{\contr_y} : x = y$, which we choose as
       the center of contraction for $\id{x}{y}$.
       Given any $p : x = y$, we need to show $p = \contr_x \ct \opp{\contr_y}$.
           By path induction, it suffices to show that
        $\refl{x} = \contr_x \ct \opp{\contr_x}$, which is trivial.

 For the inductive step, we need to show that $\id[X]{x}{y}$ is an $\nplusone$-type, provided
          that $X$ is an $\nplusone$-type. Applying the inductive hypothesis to $\id[X]{x}{y}$
         yields the desired result.
\end{proof}

% \section{Preservation under constructors}
% \label{sec:ntype-pres}

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

\begin{thm}\label{thm:ntypes-sigma}
 Let $n \geq -2$, and let $A : \type$ and $B : A \to \type$.
 If $A$ is an $n$-type and for all $a : A$, $B(a)$ is an $n$-type, then so is $\sm{x : A} B(x)$.
\end{thm}

\begin{proof}
 We proceed by induction on $n$.

 For $n = -2$, we choose the center of contraction for $\sm{x : A} B(x)$ to be the pair
       $(a_0, b_0)$, where $a_0 : A$ is the center of contraction of $A$ and $b_0 : B(a_0)$ is the center of contraction of $B(a_0)$.
       Given any other element $(a,b)$ of $\sm{x : A} B(x)$, we provide a path $\id{(a, b)}{(a_0,b_0)}$
       by contractibility of $A$ and $B(a_0)$, respectively.

 For the inductive step, suppose that $A$ is an $\nplusone$-type and
         for any $a : A$, $B(a)$ is an $\nplusone$-type. We show that $\sm{x : A} B(x)$ is an $\nplusone$-type:
      fix $(a_1, b_1)$ and $(a_2,b_2)$ in $\sm{x : A} B(x)$,
     we show that $\id{(a_1, b_1)}{(a_2,b_2)}$ is an $n$-type.
      By \cref{thm:path-sigma} we have
      \[ \eqvspaced{(\id{(a_1, b_1)}{(a_2,b_2)})}{\sm{p : \id{a_1}{a_2}} (\id[B(a_2)]{\trans{p}{b_1}}{b_2})} \]
   and by preservation of $n$-types under equivalences (\cref{cor:preservation-hlevels-weq})
   it suffices to prove that the latter is an $n$-type. This follows from the
   inductive hypothesis.
\end{proof}

As a special case, if $A$ and $B$ are $n$-types, so is $A\times B$.
Note also that \cref{thm:hlevel-cumulative} implies that if $A$ is an $n$-type, then so is $\id[A]xy$ for any $x,y:A$.
Combining this with \cref{thm:ntypes-sigma}, we see that for any functions $f:A\to C$ and $g:B\to C$ between $n$-types, their pullback\index{pullback}
\[ A\times_C B \defeq \sm{x:A}{y:B} (f(x)=g(y)) \]
(see \cref{ex:pullback}) is also an $n$-type.
More generally, $n$-types are closed under all \emph{limits}.

\begin{thm}\label{thm:hlevel-prod}
 Let $n\geq -2$, and let $A : \type$ and $B : A \to \type$.
 If for all $a : A$, $B(a)$ is an $n$-type, then so is $\prd{x : A} B(x)$.
\end{thm}

\begin{proof}
  We proceed by induction on $n$.
  For $n = -2$, the result is simply \cref{thm:contr-forall}.

  For the inductive step, assume the result is true for $n$-types, and that each $B(a)$ is an $\nplusone$-type.
  Let $f, g : \prd{a:A}B(a)$.
  We need to show that $\id{f}{g}$ is an $n$-type.
  By function extensionality and closure of $n$-types under equivalence, it suffices to show that $\prd{a : A} (\id[B(a)]{f(a)}{g(a)})$ is an $n$-type.
  This follows from the inductive hypothesis.
\end{proof}

As a special case of the above theorem, the function space $A \to B$ is an $n$-type provided that $B$ is an $n$-type.
We can now generalize our observations in \cref{cha:basics} that $\isset(A)$ and $\isprop(A)$ are mere propositions.

\begin{thm}\label{thm:isaprop-isofhlevel}
 For any $n \geq -2$ and any type $X$, the type $\istype{n}(X)$ is a mere proposition.
\end{thm}
\begin{proof}
  We proceed by induction with respect to $n$.

 For the base case, we need to show that for any $X$, the type $\iscontr(X)$ is a mere proposition.
 This is \cref{thm:isprop-iscontr}.

For the inductive step we need to show
\[\prd{X : \type} \isprop (\istype{n}(X)) \to \prd{X : \type} \isprop (\istype{\nplusone}(X)) \]
To show the conclusion of this implication, we need to show that for any type $X$, the type
\[\prd{x, x' : X}\istype{n}(x = x')\]
is a mere proposition. By \cref{thm:isprop-forall} or \cref{thm:hlevel-prod}, it suffices to show that for any $x, x' : X$, the type $\istype{n}(x =_X x')$ is a mere
proposition.
But this follows from the inductive hypothesis applied to the type $(x =_X x')$.
\end{proof}

Finally, we show that the type of $n$-types is itself an $\nplusone$-type.
We define this to be:
\symlabel{universe-of-ntypes}
\[\ntype{n} \defeq \sm{X : \type} \istype{n}(X) \]
If necessary, we may specify the universe $\UU$ by writing $\ntypeU{n}$.
In particular, we have $\prop \defeq \ntype{(-1)}$ and $\set \defeq \ntype{0}$, as defined in \cref{cha:basics}.
Note that just as for \prop and \set, because $\istype{n}(X)$ is a mere proposition, by \cref{thm:path-subset} for any $(X,p), (X',p'):\ntype{n}$ we have
\begin{align*}
  \Big(\id[\ntype{n}]{(X, p)}{(X', p')}\Big) &\eqvsym (\id[\type] X X')\\
  &\eqvsym (\eqv{X}{X'}).
\end{align*}

\begin{thm}\label{thm:hleveln-of-hlevelSn}
 For any $n \geq -2$, the type $\ntype{n}$ is an $\nplusone$-type.
\end{thm}
\begin{proof}%[Proof of \cref{thm:hleveln-of-hlevelSn}]
  Let $(X, p), (X', p') : \ntype{n}$; we need to show that $\id{(X, p)}{(X', p')}$ is an $n$-type.
  By the above observation, this type is equivalent to $\eqv{X}{X'}$.
  Next, we observe that the projection
  \[(\eqv{X}{X'}) \to (X \rightarrow X').\]
  is an embedding, so that if $n\geq -1$, then by \cref{thm:isntype-mono} it suffices to show that $X \rightarrow X'$ 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 argument shows that $\eqv{X}{X'}$ is a $(-1)$-type --- but it is also inhabited, since any two contractible types
are equivalent to \unit, and hence to each other.
  Thus, $\eqv{X}{X'}$ is also a $(-2)$-type.
\end{proof}

\section{Uniqueness of identity proofs and Hedberg's theorem}
\label{sec:hedberg}

\index{set|(}%

In \cref{sec:basics-sets} we defined a type $X$ to be a \emph{set} if for all $x, y : X$ and $p, q : x =_X y$ we have $p = q$.
In conventional type theory, this property goes by the name of \define{uniqueness of identity proofs (UIP)}.
\indexdef{uniqueness!of identity proofs}%
We have seen also that it is equivalent to being a $0$-type in the sense of the previous section.
Here is another equivalent characterization, involving Streicher's ``Axiom K'' \cite{Streicher93}:

\begin{thm}\label{thm:h-set-uip-K}
 A type $X$ is a set if and only if it satisfies \define{Axiom K}:
 \indexdef{axiom!Streicher's Axiom K}%
 for all $x : X$ and $p : (x =_A x)$ we have $p = \refl{x}$.
\end{thm}

\begin{proof}
  Clearly Axiom K is a special case of UIP.
  Conversely, if $X$ satisfies Axiom K, let $x, y : X$ and $p, q : (\id{x}{y})$; we want to show $p=q$.
  But induction on $q$ reduces this goal precisely to Axiom K.
\end{proof}

We stress that \emph{we} are not assuming UIP or the K principle as axioms!
They are simply properties which a particular type may or may not satisfy (which are equivalent to being a set).
Recall from \cref{thm:type-is-not-a-set} that \emph{not} all types are sets.

The following theorem is another useful way to show that types are sets.

\begin{thm}\label{thm:h-set-refrel-in-paths-sets}
  \index{relation!reflexive}%
  Suppose $R$ is a reflexive\index{reflexivity!of a relation} mere relation on a type $X$ implying identity.
  Then $X$ is a set, and $R(x,y)$ is equivalent to $\id[X]{x}{y}$ for all $x,y:X$.
\end{thm}

\begin{proof}
  Let $\rho : \prd{x:X} R(x,x)$ witness reflexivity of $R$, and let \narrowequation{f : \prd{x,y:X} R(x,y) \to (\id[X]{x}{y})} be a witness that $R$
implies identity.
  Note first that the two statements in the theorem are equivalent.
  For on one hand, if $X$ is a set, then $\id[X]xy$ is a mere proposition, and since it is logically equivalent to the mere proposition
$R(x,y)$ by hypothesis, it must also be equivalent to it.
  On the other hand, if $\id[X]xy$ is equivalent to $R(x,y)$, then like the latter it is a mere proposition for all $x,y:X$, and hence $X$
is a set.

  We give two proofs of this theorem.
  The first shows directly that $X$ is a set; the second shows directly that $R(x,y)\eqvsym (x=y)$.

  \emph{First proof:} we show that $X$ is a set.
  The idea is the same as that of \cref{thm:prop-set}: the function $f$ must be continuous in its arguments $x$ and $y$.
  However, it is slightly more notationally complicated because we have to deal with the additional argument of type $R(x,y)$.

  Firstly, for any $x:X$ and $p:\id[X]xx$, consider $\apdfunc{f(x)}(p)$.
  This is a dependent path from $f(x,x)$ to itself.
  Since $f(x,x)$ is still a function $R(x,x) \to (\id[X]xy)$, by \cref{thm:dpath-arrow} this yields for any $r:R(x,x)$ a path
  \[\trans{p}{f(x,x,r)} = f(x,x,\trans{p}r).
  \]
  On the left-hand side, we have transport in an identity type, which is concatenation.
  And on the right-hand side, we have $\trans{p}r = r$, since both lie in the mere proposition $R(x,x)$.
  Thus, substituting $r\defeq \rho(x)$, we obtain
  \[ f(x,x,\rho(x)) \ct p = f(x,x,\rho(x)). \]
  By cancellation, $p=\refl{x}$.
  So $X$ satisfies Axiom K, and hence is a set.

  \emph{Second proof:} we show that each $f(x,y) : R(x,y) \to \id[X]{x}{y}$ is an equivalence.
  By \cref{thm:total-fiber-equiv}, it suffices to show that $f$ induces an equivalence of total spaces:
  \begin{equation*}
    \eqv{\Parens{\sm{y:X}R(x,y)}}{\Parens{\sm{y:X}\id[X]{x}{y}}}.
  \end{equation*}
  By \cref{thm:contr-paths}, the type on the right is contractible, so it
  suffices to show that the type on the left is contractible. As the center of
  contraction we take the pair $\pairr{x,\rho(x)}$.  It remains to show, for
  every ${y:X}$ and every ${H:R(x,y)}$ that
  \begin{equation*}
    \id{\pairr{x,\rho(x)}}{\pairr{y,H}}.
  \end{equation*}
  But since $R(x,y)$ is a mere proposition, by \cref{thm:path-sigma} it suffices to show that
  $\id[X]{x}{y}$, which we get from $f(H)$.
\end{proof}

\begin{cor}\label{notnotstable-equality-to-set}
  If a type $X$ has the property that $\neg\neg(x=y)\to(x=y)$ for any $x,y:X$, then $X$ is a set.
\end{cor}

Another convenient way to show that a type is a set is the following.
Recall from \cref{sec:intuitionism} that a type $X$ is said to have \emph{decidable equality}
\index{decidable!equality|(}%
if for all $x, y : X$ we have
\[(x =_X y) + \neg (x =_X y).\]
\index{continuity of functions in type theory@``continuity'' of functions in type theory}%
\index{functoriality of functions in type theory@``functoriality'' of functions in type theory}%
This is a very strong condition: it says that a path $x=y$ can be chosen, when it exists, continuously (or computably, or functorially) in $x$ and $y$.
This turns out to imply that $X$ is a set, by way of \cref{thm:h-set-refrel-in-paths-sets} and the following lemma.

\begin{lem}\label{lem:hedberg-helper}
For any type $A$ we have $(A+\neg A)\to(\neg\neg A\to A)$.
\end{lem}

\begin{proof}
Suppose $x:A+\neg A$. We have two cases to consider.
If $x$ is $\inl(a)$ for some $a:A$, then we have the constant function $\neg\neg A
\to A$ which maps everything to $a$. If $x$ is $\inr(t)$ for some $t:\neg A$,
we have $g(t):\emptyt$ for every $g:\neg\neg A$. Hence we may use
\emph{ex falso quodlibet}, that is $\rec{\emptyt}$, to obtain an element of $A$ for any $g:\neg\neg A$.
\end{proof}

\index{anger}
\begin{thm}[Hedberg]\label{thm:hedberg}
  \index{Hedberg's theorem}%
  \index{theorem!Hedberg's}%
  If $X$ has decidable equality, then $X$ is a set.
\end{thm}

\begin{proof}
If $X$ has decidable equality, it follows that $\neg\neg(x=y)\to(x=y)$ for any
$x,y:X$. Therefore, Hedberg's theorem follows from
\cref{notnotstable-equality-to-set}.
\end{proof}

There is, of course, a strong connection between this theorem and \cref{thm:not-lem}.
The statement \LEM{\infty} that is denied by \cref{thm:not-lem} clearly implies that every type has decidable equality, and hence is a set, which we know is not the case.
\index{excluded middle}%
Note that the consistent axiom \LEM{} from \cref{sec:intuitionism} implies only that every type has \emph{merely decidable equality}, i.e.\ that for any $A$ we have
\indexdef{equality!merely decidable}%
\indexdef{merely!decidable equality}%
\[ \prd{a,b:A} (\brck{a=b} + \neg\brck{a=b}). \]

\index{decidable!equality|)}%

As an example application of \cref{thm:hedberg}, recall that in \cref{thm:nat-set} we observed that $\nat$ is a set, using our characterization of its equality types in
\cref{sec:compute-nat}.
A more traditional proof of this theorem uses only~\eqref{eq:zero-not-succ} and~\eqref{eq:suc-injective}, rather than the full
characterization of \cref{thm:path-nat}, with \cref{thm:hedberg} to fill in the blanks.

\begin{thm}\label{prop:nat-is-set}
 The type $\nat$ of natural numbers has decidable equality, and hence is a set.
\end{thm}

\begin{proof}
  Let $x, y : \nat$ be given; we proceed by induction on $x$ and case analysis on $y$ to prove $(x=y)+\neg(x=y)$.
  If $x \jdeq 0$ and $y \jdeq 0$, we take $\inl(\refl0)$.
  If $x \jdeq 0$ and $y \jdeq \suc(n)$, then by~\eqref{eq:zero-not-succ} we get $\neg (0 = \suc (n))$.

  For the inductive step, let $x \jdeq \suc (n)$.
  If $y \jdeq 0$, we use~\eqref{eq:zero-not-succ} again.
  Finally, if $y \jdeq \suc (m)$, the inductive hypothesis gives $(m = n)+\neg(m = n)$.
  In the first case, if $p:m=n$, then $\ap \suc p:\suc(m)=\suc(n)$.
  And in the second case,~\eqref{eq:suc-injective} yields $\neg(\suc(m)=\suc(n))$.
\end{proof}

\index{set|)}%

\index{axiom!Streicher's Axiom K!generalization to n-types@generalization to $n$-types}%
Although Hedberg's theorem appears rather special to sets ($0$-types), ``Axiom K'' generalizes naturally to $n$-types.
Note that the ordinary Axiom K (as a property of a type $X$) states that for all $x:X$, the loop space\index{loop space} $\Omega(X,x)$ (see \cref{def:loopspace}) is contractible.
Since $\Omega(X,x)$ is always inhabited (by $\refl{x}$), this is equivalent to its being a mere proposition (a $(-1)$-type).
Since $0 = (-1)+1$, this suggests the following generalization.

\begin{thm}\label{thm:hlevel-loops}
  For any $n\geq -1$, a type $X$ is an $\nplusone$-type if and only if for all $x : X$, the type $\Omega(X, x)$ is an $n$-type.
\end{thm}

Before proving this, we prove an auxiliary lemma:

\begin{lem}\label{lem:hlevel-if-inhab-hlevel}
  Given $n \geq -1$ and $X : \type$.
  If, given any inhabitant of $X$ it follows that $X$ is an $n$-type, then $X$ is an $n$-type.
\end{lem}
\begin{proof}
  Let $f : X \to \istype{n}(X)$ be the given map.
  We need to show that for any $x, x' : X$, the type $\id{x}{x'}$ is an $\nminusone$-type.
  But then $f(x)$ shows that $X$ is an $n$-type, hence all its path spaces are $\nminusone$-types.
\end{proof}

\begin{proof}[Proof of \cref{thm:hlevel-loops}]
  The ``only if'' direction is obvious, since $\Omega(X,x)\defeq (\id[X]xx)$.
  Conversely, in order to show that $X$ is an $\nplusone$-type, we need to show that for any $x, x' : X$, the type $\id{x}{x'}$ is an
$n$-type.
  Following \cref{lem:hlevel-if-inhab-hlevel} it suffices to give a map
  \[ (\id{x}{x'}) \to \istype{n}(\id{x}{x'}). \]
  By path induction, it suffices to do this when $x\jdeq x'$, in which case it follows from the assumption that $\Omega(X, x)$ is an
$n$-type.
\end{proof}

\index{whiskering}
By induction and some slightly clever whiskering, we can obtain a generalization of the K property to $n>0$.

\begin{thm}\label{thm:ntype-nloop}
  \index{loop space!iterated}%
  For every $n\ge -1$, a type $A$ is an $n$-type if and only if $\Omega^{n+1}(A,a)$ is contractible for all $a:A$.
\end{thm}
\begin{proof}
  Recalling that $\Omega^0(A,a) = (A,a)$, the case $n=-1$ is \cref{ex:prop-inhabcontr}.
  The case $n=0$ is \cref{thm:h-set-uip-K}.
  Now we use induction; suppose the statement holds for $n:\N$.
  By \cref{thm:hlevel-loops}, $A$ is an $(n+1)$-type iff $\Omega(A,a)$ is an $n$-type for all $a:A$.
  By the inductive hypothesis, the latter is equivalent to saying that $\Omega^{n+1}(\Omega(A,a),p)$ is contractible for all $p:\Omega(A,a)$.

  Since $\Omega^{n+2}(A,a) \defeq \Omega^{n+1}(\Omega(A,a),\refl{a})$, and $\Omega^{n+1} = \Omega^n \circ \Omega$, it will suffice to show that $\Omega(\Omega(A,a),p)$ is equal to $\Omega(\Omega(A,a),\refl{a})$, in the type $\pointed\type$ of pointed types.
  For this, it suffices to give an equivalence
  \[ g : \Omega(\Omega(A,a),p) \eqvsym \Omega(\Omega(A,a),\refl{a}) \]
  which carries the basepoint $\refl{p}$ to the basepoint $\refl{\refl{a}}$.
  For $q:p=p$, define $g(q):\refl{a} = \refl{a}$ to be the following composite:
  \[ \refl{a} = p\ct \opp p \overset{q}{=} p\ct\opp p = \refl{a}, \]
  where the path labeled ``$q$'' is actually $\apfunc{\lam{r} r\ct\opp p} (q)$.
  Then $g$ is an equivalence because it is a composite of equivalences
  \[ (p=p) \xrightarrow{\apfunc{\lam{r} r\ct\opp p}} (p\ct \opp p = p\ct \opp p) \xrightarrow{i\ct - \ct \opp i} (\refl{a} = \refl{a}). \]
  using \cref{eg:concatequiv,thm:paths-respects-equiv}, where $i:\refl{a} = p\ct \opp p$ is the canonical equality.
  And it is evident that $g(\refl{p}) = \refl{\refl{a}}$.
\end{proof}

\section{Truncations}
\label{sec:truncations}

\indexsee{n-truncation@$n$-truncation}{truncation}%
\index{truncation!n-truncation@$n$-truncation|(defstyle}%

In \cref{subsec:prop-trunc} we introduced the propositional truncation, which makes the ``best approximation'' of a type that is a mere
proposition, i.e.\ a $(-1)$-type.
In \cref{sec:hittruncations} we constructed this truncation as a higher inductive type, and gave one way to generalize it to a
0-truncation.
We now explain a better generalization of this, which truncates any type into an $n$-type for any $n\geq -2$; in classical homotopy theory this would be called its \define{$n^{\mathrm{th}}$ Postnikov section}.\index{Postnikov tower}

The idea is to make use of \cref{thm:ntype-nloop}, which states that $A$ is an $n$-type just when $\Omega^{n+1}(A,a)$
\index{loop space!iterated}%
is contractible for
all $a:A$, and \cref{lem:susp-loop-adj}, which implies that
\narrowequation{\Omega^{n+1}(A,a) \eqvsym \Map_{*}(\Sn^{n+1},(A,a)),} where $\Sn^{n+1}$ is equipp\-ed with some basepoint which we may as well call \base.
However, contractibility of $\Map_*(\Sn^{n+1},(A,a))$ is something that we can ensure directly by giving path constructors.

\index{hub and spoke}%
We will use the ``hub and spoke'' construction as in \cref{sec:hubs-spokes}.
Thus, for $n\ge -1$, we take $\trunc nA$ to be the higher inductive type generated by:
\begin{itemize}
\item a function $\tprojf n : A \to \trunc n A$,
\item for each $r:\Sn^{n+1} \to \trunc n A$, a \emph{hub} point $h(r):\trunc n A$, and
\item for each $r:\Sn^{n+1} \to \trunc n A$ and each $x:\Sn^{n+1}$, a \emph{spoke} path $s_r(x):r(x) = h(r)$.
\end{itemize}

\noindent
The existence of these constructors is now enough to show:

\begin{lem}
  $\trunc n A$ is an $n$-type.
\end{lem}
\begin{proof}
  By \cref{thm:ntype-nloop}, it suffices to show that $\Omega ^{n+1}(\trunc nA,b)$ is contractible for all $b:\trunc nA$, which by
\cref{lem:susp-loop-adj} is equivalent to \narrowequation{\Map_*(\Sn^{n+1},(\trunc nA,b)).}
  As center of contraction for the latter, we choose the function $c_b:\Sn^{n+1} \to \trunc nA$ which is constant at $b$, together with
$\refl b : c_b(\base) = b$.

  Now, an arbitrary element of $\Map_*(\Sn^{n+1},(\trunc nA,b))$ consists of a map $r:\Sn^{n+1} \to \trunc n A$ together with a path
$p:r(\base)=b$.
  By function extensionality, to show $r = c_b$ it suffices to give, for each $x:\Sn^{n+1}$, a path $r(x)=c_b(x) \jdeq b$.
  We choose this to be the composite $s_r(x) \ct \opp{s_r(\base)} \ct p$, where $s_r(x)$ is the spoke at $x$.


  Finally, we must show that when transported along this equality $r=c_b$, the path $p$ becomes $\refl b$.
  By transport in path types, this means we need
  \[\opp{(s_r(\base) \ct \opp{s_r(\base)} \ct p)} \ct p = \refl b.\]
  But this is immediate from path operations.
\end{proof}

(This construction fails for $n=-2$, but in that case we can simply define $\trunc{-2}{A}\defeq \unit$ for all $A$.
From now on we assume $n\ge -1$.)

\index{induction principle!for truncation}%
To show the desired universal property of the $n$-truncation, we need the induction principle.
We extract this from the constructors in the usual way; it says that given $P:\trunc nA\to\type$ together with
\begin{itemize}
\item For each $a:A$, an element $g(a) : P(\tproj na)$,
\item For each $r:\Sn^{n+1} \to \trunc n A$ and $r':\prd{x:\Sn^{n+1}} P(r(x))$, an element $h'(r,r'):P(h(r))$,
\item For each $r:\Sn^{n+1} \to \trunc n A$ and $r':\prd{x:\Sn^{n+1}} P(r(x))$, and each $x:\Sn^{n+1}$, a dependent path
$\dpath{P}{s_r(x)}{r'(x)}{h'(r,r')}$,
\end{itemize}
there exists a section $f:\prd{x:\trunc n A} P(x)$ with $f(\tproj n a) \jdeq g(a)$ for all $a:A$.
To make this more useful, we reformulate it as follows.

\begin{thm}\label{thm:truncn-ind}
  For any type family $P:\trunc n A \to \type$ such that each $P(x)$ is an $n$-type, and any function $g : \prd{a:A} P(\tproj n a)$, there
exists a section $f:\prd{x:\trunc n A} P(x)$ such that $f(\tproj n a)\defeq g(a)$ for all $a:A$.
\end{thm}
\begin{proof}
  It will suffice to construct the second and third data listed above, since $g$ has exactly the type of the first datum.
  Given $r:\Sn^{n+1} \to \trunc n A$ and $r':\prd{x:\Sn^{n+1}} P(r(x))$, we have $h(r):\trunc n A$ and $s_r :\prd{x:\Sn^{n+1}} (r(x) =
h(r))$.
  Define $t:\Sn^{n+1} \to P(h(r))$ by $t(x) \defeq \trans{s_r(x)}{r'(x)}$.
  Then since $P(h(r))$ is $n$-truncated, there exists a point $u:P(h(r))$ and a contraction $v:\prd{x:\Sn^{n+1}} (t(x) = u)$.
  Define $h'(r,r') \defeq u$, giving the second datum.
  Then (recalling the definition of dependent paths), $v$ has exactly the type required of the third datum.
\end{proof}

In particular, if $E$ is some $n$-type, we can consider the constant family of types equal to $E$ for every point of $A$.
\symlabel{extend}
\index{recursion principle!for truncation}%
Thus, every map $f:A\to{}E$ can be extended to a map $\extend{f}:\trunc nA\to{}E$ defined by $\extend{f}(\tproj na)\defeq f(a)$; this is the \emph{recursion principle} for $\trunc n A$.

The induction principle also implies a uniqueness principle for functions of this form.
\index{uniqueness!principle, propositional!for functions on a truncation}%
Namely, if $E$ is an $n$-type and $g,g':\trunc nA\to{}E$ are such
that $g(\tproj na)=g'(\tproj na)$ for every $a:A$, then $g(x)=g'(x)$ for all $x:\trunc nA$, since the type $g(x)=g'(x)$ is an $n$-type.
Thus, $g=g'$.
(In fact, this uniqueness principle holds more generally when $E$ is an $\nplusone$-type.)
This yields the following universal property.

\begin{lem}[Universal property of truncations]\label{thm:trunc-reflective}
  \index{universal!property!of truncation}%
  Let $n\ge-2$, $A:\type$ and $B:\typele{n}$. The following map is an
  equivalence:
  \[\function{(\trunc nA\to{}B)}{(A\to{}B)}{g}{g\circ\tprojf n}\]
\end{lem}

\begin{proof}
  Given that $B$ is $n$-truncated, any $f:A\to{}B$ can be extended to a map $\extend{f}:\trunc nA\to{}B$.
  The map $\extend{f}\circ\tprojf n$ is equal to $f$, because for every $a:A$ we have $\extend{f}(\tproj na)=f(a)$ by definition.
  And the map $\extend{g\circ\tprojf n}$ is equal to $g$, because they both send $\tproj na$ to $g(\tproj na)$.
\end{proof}

In categorical language, this says that the $n$-types form a \emph{reflective subcategory} of the category of types.
\index{reflective!subcategory}%
(To state this fully precisely, one ought to use the language of $(\infty,1)$-categories.)
\index{.infinity1-category@$(\infty,1)$-category}%
In particular, this implies that the $n$-truncation is functorial:
given $f:A\to B$, applying the recursion principle to the composite $A\xrightarrow{f} B \to \trunc n B$ yields a map $\trunc n f: \trunc n A \to \trunc n B$.
By definition, we have a homotopy
\begin{equation}
  \mathsf{nat}^f_n : \prd{a:A} \trunc n f(\tproj n a) = \tproj n {f(a)},\label{eq:trunc-nat}
\end{equation}
expressing \emph{naturality} of the maps $\tprojf n$.

Uniqueness implies functoriality laws such as $\trunc n {g\circ f} = \trunc n g \circ \trunc n f$ and $\trunc n{\idfunc[A]} = \idfunc[\trunc n A]$, with attendant coherence laws.
We also have higher functoriality, for instance:

\begin{lem}\label{thm:trunc-htpy}
  Given $f,g:A\to B$ and a homotopy $h:f\htpy g$, there is an induced homotopy $\trunc n h : \trunc n f \htpy \trunc n g$ such that the composite
  \begin{equation}
    \xymatrix@C=3.6pc{\tproj n{f(a)} \ar@{=}[r]^-{\opp{\mathsf{nat}^f_n(a)}} &
      \trunc n f(\tproj n a) \ar@{=}[r]^-{\trunc n h(\tproj na)} &
      \trunc n g(\tproj n a) \ar@{=}[r]^-{\mathsf{nat}^g_n(a)} &
      \tproj n{g(a)}}\label{eq:trunc-htpy}
  \end{equation}
  is equal to $\apfunc{\tprojf n}(h(a))$.
\end{lem}
\begin{proof}
  First, we indeed have a homotopy with components $\apfunc{\tprojf n}(h(a)) : \tproj n{f(a)} = \tproj n{g(a)}$.
  Composing on either sides with the paths $\tproj n{f(a)} = \trunc n f(\tproj n a)$ and $\tproj n{g(a)} = \trunc n g(\tproj n a)$, which arise from the definitions of $\trunc n f$ and $\trunc ng$, we obtain a homotopy $(\trunc n f \circ \tprojf n) \htpy (\trunc n g \circ \tprojf n)$, and hence an equality by function extensionality.
  But since $(\blank\circ \tprojf n)$ is an equivalence, there must be a path $\trunc nf = \trunc ng$ inducing it, and the coherence laws for function extensionality imply~\eqref{eq:trunc-htpy}.
\end{proof}

The following observation about reflective subcategories is also standard.

\begin{cor}
  A type $A$ is an $n$-type if and only if $\tprojf n : A \to \trunc n A$ is an equivalence.
\end{cor}
\begin{proof}
  ``If'' follows from closure of $n$-types under equivalence.
  On the other hand, if $A$ is an $n$-type, we can define $\ext(\idfunc[A]):\trunc n A\to{}A$.
  Then we have $\ext(\idfunc[A])\circ\tprojf n=\idfunc[A]:A\to{}A$ by
  definition.  In order to prove that
  $\tprojf n\circ\ext(\idfunc[A])=\idfunc[\trunc nA]$, we only need to prove
  that $\tprojf n\circ\ext(\idfunc[A])\circ\tprojf n=
  \idfunc[\trunc nA]\circ\tprojf n$.
  This is again true:
  \[\raisebox{\depth-\height+1em}{\xymatrix{
    A \ar^-{\tprojf n}[r] \ar_{\idfunc[A]}[rd] &
    \trunc nA \ar^>>>{\ext(\idfunc[A])}[d] \ar@/^40pt/^{\idfunc[\trunc nA]}[dd] \\
    & A \ar_{\tprojf n}[d] \\
    & \trunc nA}}
  \qedhere\]
\end{proof}

The category of $n$-types also has some special properties not possessed by all reflective subcategories.
For instance, the reflector $\trunc n-$ preserves finite products.

\begin{thm}\label{cor:trunc-prod}
  For any types $A$ and $B$, the induced map $\trunc n{A\times B} \to \trunc nA \times \trunc nB$ is an equivalence.
\end{thm}
\begin{proof}
  It suffices to show that $\trunc nA \times \trunc nB$ has the same universal property as $\trunc n{A\times B}$.
  Thus, let $C$ be an $n$-type; we have
  \begin{align*}
    (\trunc nA \times \trunc nB \to C)
    &= (\trunc nA \to (\trunc nB \to C))\\
    &= (\trunc nA \to (B \to C))\\
    &= (A \to (B \to C))\\
    &= (A \times B \to C)
  \end{align*}
  using the universal properties of $\trunc nB$ and $\trunc nA$, along with the fact that $B\to C$ is an $n$-type since $C$ is.
  It is straightforward to verify that this equivalence is given by composing with $\tprojf n \times \tprojf n$, as needed.
\end{proof}

The following related fact about dependent sums is often useful.

\begin{thm}\label{thm:trunc-in-truncated-sigma}
Let $P:A\to\type$ be a family of types. Then there is an equivalence
\begin{equation*}
\eqv{\Trunc n{\sm{x:A}\trunc n{P(x)}}}{\Trunc n{\sm{x:A}P(x)}}.
\end{equation*}
\end{thm}

\begin{proof}
We use the induction principle of $n$-truncation several times to construct
functions
\begin{align*}
\varphi & : \Trunc n{\sm{x:A}\trunc n{P(x)}}\to\Trunc n{\sm{x:A}P(x)}\\
\psi & : \Trunc n{\sm{x:A}P(x)}\to \Trunc n{\sm{x:A} \trunc n{P(x)}}
\end{align*}
and homotopies $H:\varphi\circ\psi\htpy \idfunc$ and $K:\psi\circ\varphi\htpy
\idfunc$ exhibiting them as quasi-inverses.
We define $\varphi$ by setting $\varphi(\tproj n{\pairr{x,\tproj nu}})\defeq\tproj n{\pairr{x,u}}$.
We define $\psi$ by setting $\psi(\tproj n{\pairr{x,u}})\defeq\tproj n{\pairr{x,\tproj nu}}$.
Then we define $H(\tproj n{\pairr{x,u}})\defeq \refl{\tproj n{\pairr{x,u}}}$ and
$K(\tproj n{\pairr{x,\tproj nu}})\defeq \refl{\tproj n{\pairr{x,\tproj nu}}}$.
\end{proof}

\begin{cor}\label{thm:refl-over-ntype-base}
  If $A$ is an $n$-type and $P:A\to\type$ is any type family, then
  \[ \eqv{\sm{a:A} \trunc n{P(a)}}{\Trunc n{\sm{a:A}P(a)}} \]
\end{cor}
\begin{proof}
  If $A$ is an $n$-type, then the left-hand type above is already an $n$-type, hence equivalent to its $n$-truncation; thus this follows from \cref{thm:trunc-in-truncated-sigma}.
\end{proof}

We can characterize the path spaces of a truncation using the same method that we used in \cref{sec:compute-coprod,sec:compute-nat} for
coproducts and natural numbers (and which we will use in \cref{cha:homotopy} to calculate homotopy groups).
Unsurprisingly, the path spaces in the $(n+1)$-truncation of $A$ are the $n$-truncations of the path spaces of $A$.
Indeed, for any $x,y:A$ there is a canonical map
\begin{equation}
  f:\ttrunc n{x=_Ay}\to \Big(\tproj {n+1}x=_{\trunc{n+1}A}\tproj {n+1}y\Big)\label{eq:path-trunc-map}
\end{equation}
defined by
\[f(\tproj n{p})\defeq \apfunc{\tprojf {n+1}}(p). \]
This definition uses the recursion principle for $\truncf n$, which is correct because $\trunc {n+1}A$ is $(n+1)$-truncated, so that the
codomain of $f$ is $n$-truncated.

\begin{thm} \label{thm:path-truncation}
  For any $A$ and $x,y:A$ and $n\ge -2$, the map~\eqref{eq:path-trunc-map} is an equivalence; thus we have
  \[ \eqv{\ttrunc n{x=_Ay}}{\Big(\tproj {n+1}x=_{\trunc{n+1}A}\tproj {n+1}y\Big)}. \]
\end{thm}

\begin{proof}
  The proof is a simple application of the encode-decode method:
  As in previous situations, we cannot directly define a quasi-inverse to the map~\eqref{eq:path-trunc-map} because there is no way to induct on an
equality between $\tproj {n+1}x$ and $\tproj {n+1}y$.
  Thus, instead we generalize its type, in order to have general elements of the type $\trunc{n+1}A$ instead of $\tproj {n+1}x$ and $\tproj
{n+1}y$.
  Define $P:\trunc {n+1}A\to\trunc {n+1}A\to\typele{n}$ by
  \[P(\tproj {n+1}x,\tproj {n+1}y)\defeq \trunc n{x=_Ay}\]
  This definition is correct because $\trunc n{x=_Ay}$ is $n$-truncated, and $\typele{n}$ is $(n+1)$-truncated by
\cref{thm:hleveln-of-hlevelSn}.
  Now for every $u,v:\trunc{n+1}A$, there is a map
  \[\decode:P(u,v) \to \big(u=_{\trunc{n+1}A}v\big)\]
  defined for $u=\tproj {n+1}x$ and $v=\tproj {n+1}y$ and $p:x=y$ by
  \[\decode(\tproj n{p})\defeq \apfunc{\tprojf{n+1}} (p).\]
  Since the codomain of $\decode$ is $n$-truncated, it suffices to define it only for $u$ and $v$ of this form, and then it's just the same
definition as before.
  We also define a function
  \[ r : \prd{u:\trunc{n+1} A} P(u,u) \]
  by induction on $u$, where $r(\tproj{n+1} x) \defeq \tproj n {\refl x}$.

  Now we can define an inverse map
  \[\encode: (u=_{\trunc{n+1}A}v) \to P(u,v)\]
  by
  \[\encode(p) \defeq \transfib{v\mapsto P(u,v)}{p}{r(u)}. \]
  To show that the composite
  \[ (u=_{\trunc{n+1}A}v) \xrightarrow{\encode} P(u,v) \xrightarrow{\decode} (u=_{\trunc{n+1}A}v) \]
  is the identity function, by path induction it suffices to check it for $\refl u : u=u$, in which case what we need to know is that
$\encode(r(u)) = \refl{u}$.
  But since this is an $n$-type, hence also an $(n+1)$-type, we may assume $u\jdeq \tproj {n+1} x$, in which case it follows by definition
of $r$ and $\encode$.
  Finally, to show that
  \[ P(u,v) \xrightarrow{\decode} (u=_{\trunc{n+1}A}v) \xrightarrow{\encode} P(u,v) \]
  is the identity function, since this goal is again an $n$-type, we may assume that $u=\tproj {n+1}x$ and $v=\tproj {n+1}y$ and that we are
considering $\tproj n p:P(\tproj{n+1}x,\tproj{n+1}y)$ for some $p:x=y$.
  Then we have
  \begin{align*}
    \encode(\decode(\tproj n p)) &= \encode(\apfunc{\tprojf{n+1}}(p))\\
    &= \transfib{v\mapsto P(\tproj{n+1}x,v)}{\apfunc{\tprojf{n+1}}(p)}{\tproj n {\refl x}}\\
    &= \transfib{v\mapsto \trunc n{u=v}}{p}{\tproj n {\refl x}}\\
    &= \tproj n {\transfib{v \mapsto (u=v)}{p}{\refl x}}\\
    &= \tproj n p.
  \end{align*}
  This completes the proof that \decode and \encode are quasi-inverses.
  The stated result is then the special case where $u=\tproj {n+1}x$ and $v=\tproj {n+1}y$.
\end{proof}

\begin{cor}
  Let $n\ge-2$ and $(A,a)$ be a pointed type. Then
  \[\ttrunc n{\Omega(A,a)}=\Omega\mathopen{}\left(\trunc{n+1}{(A,a)}\right)\]
\end{cor}
\begin{proof}
  This is a special case of the previous lemma where $x=y=a$.
\end{proof}

\begin{cor}
  Let $n\ge -2$ and $k\ge 0$ and $(A,a)$ a pointed type.  Then
  \[\ttrunc n{\Omega^k(A,a)} = \Omega^k\mathopen{}\left(\trunc{n+k}{(A,a)}\right). \]
\end{cor}
\begin{proof}
  By induction on $k$, using the recursive definition of $\Omega^k$.
\end{proof}

We also observe that ``truncations are cumulative'': if we truncate to an $n$-type and then to a $k$-type with $k\le n$, then we might as
well have truncated directly to a $k$-type.

\begin{lem} \label{lem:truncation-le}
  Let $k,n\ge-2$ with $k\le{}n$ and $A:\type$. Then
  $\trunc k{\trunc nA}=\trunc kA$.
\end{lem}
\begin{proof}
  We define two maps $f:\trunc k{\trunc nA}\to\trunc kA$ and
  $g:\trunc kA\to\trunc k{\trunc nA}$ by
  %
  \[
   f(\tproj k{\tproj na}) \defeq \tproj ka
   \qquad\text{and}\qquad
   g(\tproj ka) \defeq \tproj k{\tproj na}.
  \]
  %
  The map $f$ is well-defined because $\trunc kA$ is $k$-truncated and also
  $n$-truncated (because $k\le{}n$), and the map $g$ is well-defined because
  $\trunc k{\trunc nA}$ is $k$-truncated.

  The composition $f\circ{}g:\trunc kA\to\trunc kA$ satisfies
  $(f\circ{}g)(\tproj ka)=\tproj ka$, hence $f\circ{}g=\idfunc[\trunc kA]$.
  Similarly, we have $(g\circ{}f)(\tproj k{\tproj na})=\tproj k{\tproj na}$ and hence $g\circ{}f=\idfunc[\trunc k{\trunc nA}]$.
\end{proof}

% \begin{lem}
%   We have $\trunc n{\unit}=\unit$.
% \end{lem}
% \begin{proof}
%   Indeed, $\unit$ is $n$-truncated for every $n$ hence $\trunc n{\unit}=\unit$ by
%   \cref{reflectPequiv}.
% \end{proof}

\index{truncation!n-truncation@$n$-truncation|)}%

\section{Colimits of \texorpdfstring{$n$}{n}-types}
\label{sec:pushouts}

Recall that in \cref{sec:colimits}, we used higher inductive types to define pushouts of types, and proved their universal property.
In general, a (homotopy) colimit of $n$-types may no longer be an $n$-type (for an extreme counterexample, see \cref{ex:s2-colim-unit}).
However, if we $n$-truncate it, we obtain an $n$-type which satisfies the correct universal property with respect to other $n$-types.

In this section we prove this for pushouts, which are the most important and nontrivial case of colimits.
Recall the following definitions from \cref{sec:colimits}.

\begin{defn}
  A \define{span} % in $\P$
  \indexdef{span} %
  is a 5-tuple $\Ddiag=(A,B,C,f,g)$ with % $A,B,C:\P$ and
  $f:C\to{}A$ and $g:C\to{}B$.
  \[\Ddiag=\quad\vcenter{\xymatrix{C \ar^g[r] \ar_f[d] & B \\ A & }}\]
\end{defn}

\begin{defn}
  Given a span $\Ddiag=(A,B,C,f,g)$ and a type $D$, a %$D:\P$, a
  \define{cocone under $\Ddiag$ with base $D$} is a triple $(i, j, h)$
  \index{cocone} %
  with $i:A\to{}D$, $j:B\to{}D$ and $h : \prd{c:C}i(f(c))=j(g(c))$:
  \[\uppercurveobject{{ }}\lowercurveobject{{ }}\twocellhead{{ }}
  \xymatrix{C \ar^g[r] \ar_f[d] \drtwocell{^h} & B \ar^j[d] \\ A \ar_i[r] & D
  }\]
  We denote by $\cocone{\Ddiag}{D}$ the type of all such cocones.
\end{defn}

The type of cocones is (covariantly) functorial.
For instance, given $D,E$ % $D,E:\P$
and a map $t:D\to{}E$, there is a map
  \[\function{\cocone{\Ddiag}{D}}{\cocone{\Ddiag}{E}}{c}{\composecocone{t}c}\]
  defined by:
  \[\composecocone{t}(i,j,h)=(t\circ{}i,t\circ{}j,\mapfunc{t}\circ{}h)\]
And given $D,E,F$, %$:\P$,
functions $t:D\to{}E$, $u:E\to{}F$ and $c:\cocone{\Ddiag}{D}$, we have
\begin{align}
  \composecocone{\idfunc[D]}c &= c \label{eq:composeconeid}\\
  \composecocone{(u\circ{}t)}c&=\composecocone{u}(\composecocone{t}c). \label{eq:composeconefunc}
\end{align}

\begin{defn}
  Given a span $\Ddiag$ of $n$-types, an $n$-type $D$, and a cocone
  $c:\cocone{\Ddiag}{D}$, the pair $(D,c)$ is said to be a \define{pushout
  of $\Ddiag$ in $n$-types}
  \indexdef{pushout!in ntypes@in $n$-types}%
  if for every $n$-type $E$, the map
  \[\function{(D\to{}E)}{\cocone{\Ddiag}{E}}{t}{\composecocone{t}c}\]
  is an equivalence.
\end{defn}

\begin{comment}
We showed in \cref{thm:pushout-ump} that pushouts exist when $\P$ is \type itself, by giving a direct construction in terms of higher
inductive types.
For a general \P, pushouts may or may not exist, but if they do, then they are unique.

\begin{lem}
  If $(D,c)$ and $(D',c')$ are two pushouts of $\Ddiag$ in $\P$, then
  $(D,c)=(D',c')$.
\end{lem}
\begin{proof}
  We first prove that the two types $D$ and $D'$ are equivalent.

  Using the universal property of $D$ with $D'$, we see that the following map is an
  equivalence
  %
  \[
    \function{(D\to{}D')}{\cocone{\Ddiag}{D'}}{t}{\composecocone{t}c}
  \]
  %
  In particular, there is a function $f:D\to{}D'$ satisfying $\composecocone{f}c=c'$. In the
  same way there is a function $g:D'\to{}D$ such that $\composecocone{g}c'=c$.

  In order to prove that $g\circ{}f=\idfunc[D]$ we use the universal property of
  $D$ for $D$, which says that the following map is an equivalence:
  %
  \[
  \function{(D\to{}D)}{\cocone{\Ddiag}{D}}{t}{\composecocone{t}c}
  \]
  %
  Using the functoriality of $t\mapsto{}\composecocone{t}c$ we see that
  \begin{align*}
    \composecocone{(g\circ{}f)}c &= \composecocone{g}(\composecocone{f}c) \\
    &= \composecocone{g}c' \\
    &= c \\
    &= \composecocone{\idfunc[D]}c
  \end{align*}
  hence
  $g\circ{}f=\idfunc[D]$, because equivalences are injective. The same argument
  with $D'$ instead of $D$ shows that $f\circ{}g=\idfunc[D']$.

  Hence $D$ and $D'$ are equal, and the fact that $(D,c)=(D',c')$ follows from
  the fact that the equivalence between $D$ and $D'$ we just defined sends $c$
  to $c'$.
\end{proof}

\begin{cor}
  The type of pushouts of $\Ddiag$ in $\P$ is a mere proposition. In particular if
  pushouts merely exist then they actually exist.
\end{cor}

As in the case of pullbacks, if \P is reflective, then pushouts in \P always exist.
However, unlike the case of pullbacks, pushouts in \P are not the same as the pushouts in \type: they are obtained by applying the
reflector.
\end{comment}

In order to construct pushouts of $n$-types, we need to explain how to reflect spans and cocones.

\bgroup
\def\reflect(#1){\trunc n{#1}}

\begin{defn}
  Let
  \[\Ddiag=\quad\vcenter{\xymatrix{C \ar^g[r] \ar_f[d] & B \\ A & }}\]
  be a span. We denote by $\reflect(\Ddiag)$ the following
  span of $n$-types:
  \[\reflect(\Ddiag)\defeq\quad \vcenter{\xymatrix{\reflect(C) \ar^{\reflect(g)}[r]
      \ar_{\reflect(f)}[d] & \reflect(B) \\ \reflect(A) & }}\]
\end{defn}

\begin{defn}
  Let $D:\type$ and $c=(i,j,h):\cocone{\Ddiag}{D}$.
  We define
  \[\reflect(c)=(\reflect(i),\reflect(j),\reflect(h)):
  \cocone{\reflect(\Ddiag)}{\reflect(D)}\]
  where $\reflect(h): \reflect(i) \circ \reflect(f) \htpy \reflect(j) \circ \reflect(g)$ is defined as in \cref{thm:trunc-htpy}.
  % \[\reflect(h):\prd{c:\reflect(C)}\reflect(i)(\reflect(f)(c))=\reflect(j)(\reflect(g)(c))\]
  % is defined in the following way:
\end{defn}

\egroup

We now observe that the maps from each type to its $n$-truncation assemble into a map of spans, in the following sense.

\begin{defn}
  Let
  \[\Ddiag=\quad\vcenter{\xymatrix{C \ar^g[r] \ar_f[d] & B \\ A & }}
  \qquad\text{and}\qquad
  \Ddiag'=\quad\vcenter{\xymatrix{C' \ar^{g'}[r] \ar_{f'}[d] & B' \\ A' & }}
  \]
  be spans.
  A \define{map of spans}
  \indexdef{map!of spans}%
  $\Ddiag \to \Ddiag'$ consists of functions $\alpha:A\to A'$, $\beta:B\to B'$, and $\gamma:C\to C'$ and homotopies $\phi: \alpha\circ f \htpy f'\circ \gamma$ and $\psi:\beta\circ g \htpy g' \circ \gamma$.
\end{defn}

Thus, for any span $\Ddiag$, we have a map of spans $\tprojf[\Ddiag] n : \Ddiag \to \trunc n\Ddiag$ consisting of $\tprojf[A]n$, $\tprojf[B]n$, $\tprojf[C]n$, and the naturality homotopies $\mathsf{nat}^f_n$ and $\mathsf{nat}^g_n$ from~\eqref{eq:trunc-nat}.

We also need to know that maps of spans behave functorially.
Namely, if $(\alpha,\beta,\gamma,\phi,\psi):\Ddiag \to \Ddiag'$ is a map of spans and $D$ any type, then we have
\[ \function{\cocone{\Ddiag'}{D}}{\cocone{\Ddiag}{D}}{(i,j,h)}{(i\circ \alpha,j\circ\beta, k)} \]
where $k: \prd{z:C} i(\alpha(f(z))) = j(\beta(g(z)))$ is the composite
\begin{equation}\label{eq:mapofspans-htpy}
\xymatrix{
  i(\alpha(f(z))) \ar@{=}[r]^{\apfunc{i}(\phi)} &
  i(f'(\gamma(z))) \ar@{=}[r]^{h(\gamma(z))} &
  j(g'(\gamma(z))) \ar@{=}[r]^{\apfunc{j}(\psi)} &
  j(\beta(g(z))). }
\end{equation}
We denote this cocone by $(i,j,h) \circ (\alpha,\beta,\gamma,\phi,\psi)$.
Moreover, this functorial action commutes with the other functoriality of cocones:

\begin{lem}\label{thm:conemap-funct}
  Given $(\alpha,\beta,\gamma,\phi,\psi):\Ddiag \to \Ddiag'$ and $t:D\to E$, the following diagram commutes:
  \begin{equation*}
    \vcenter{\xymatrix{
        \cocone{\Ddiag'}{D}\ar[r]^{t \circ {\blank}}\ar[d] &
        \cocone{\Ddiag'}{E}\ar[d]\\
        \cocone{\Ddiag}{D}\ar[r]_{t \circ {\blank}} &
        \cocone{\Ddiag}{E}
      }}
  \end{equation*}
\end{lem}
\begin{proof}
  Given $(i,j,h):\cocone{\Ddiag'}{D}$, note that both composites yield a cocone whose first two components are $t\circ i\circ \alpha$ and $t\circ j\circ\beta$.
  Thus, it remains to verify that the homotopies agree.
  For the top-right composite, the homotopy is~\eqref{eq:mapofspans-htpy} with $(i,j,h)$ replaced by $(t\circ i, t\circ j, \apfunc{t}\circ h)$:
  \begin{equation*}
    \xymatrix@+2.8em{
      {t \, i \, \alpha \, f \, z} \ar@{=}[r]^{\apfunc{t\circ i}(\phi)} &
      {t \, i \, f' \, \gamma \, z} \ar@{=}[r]^{\apfunc{t}(h(\gamma(z)))} &
      {t \, j \, g' \, \gamma \, z} \ar@{=}[r]^{\apfunc{t\circ j}(\psi)} &
      {t \, j \, \beta \, g \, z}
    }
  \end{equation*}
  (For brevity, we are omitting the parentheses around the arguments of functions.)
  On the other hand, for the left-bottom composite, the homotopy is $\apfunc{t}$ applied to~\eqref{eq:mapofspans-htpy}.
  Since $\apfunc{}$ respects path-concatenation, this is equal to
  \begin{equation*}
    \xymatrix@+2.8em{
      {t \, i \, \alpha \, f \, z} \ar@{=}[r]^{\apfunc{t}(\apfunc{i}(\phi))} &
      {t \, i \, f' \, \gamma \, z} \ar@{=}[r]^{\apfunc{t}(h(\gamma(z)))} &
      {t \, j \, g' \, \gamma \, z} \ar@{=}[r]^{\apfunc{t}(\apfunc{j}(\psi))} &
      {t \, j \, \beta \, g \, z}. }
  \end{equation*}
  But $\apfunc{t}\circ \apfunc{i} = \apfunc{t\circ i}$ and similarly for $j$, so these two homotopies are equal.
\end{proof}

Finally, note that since we defined $\trunc nc : \cocone{\trunc n \Ddiag}{\trunc n D}$ using \cref{thm:trunc-htpy}, the additional condition~\eqref{eq:trunc-htpy} implies
\begin{equation}
  \tprojf[D] n \circ c = \trunc n c \circ \tprojf[\Ddiag]n. \label{eq:conetrunc}
\end{equation}
for any $c:\cocone{\Ddiag}{D}$.
Now we can prove our desired theorem.

\begin{thm}
  \label{reflectcommutespushout}
  \index{universal!property!of pushout}%
  Let $\Ddiag$ be a span and $(D,c)$ its pushout.
  Then $(\trunc nD,\trunc n c)$ is a pushout of $\trunc n\Ddiag$ in $n$-types.
\end{thm}
\begin{proof}
  Let $E$ be an $n$-type, and consider the following diagram:
\bgroup
\def\reflect(#1){\trunc n{#1}}
  \begin{equation*}
  \vcenter{\xymatrix{
      (\trunc nD \to E)\ar[r]^-{\blank\circ \tprojf[D] n}\ar[d]_{\blank\circ \trunc nc} &
      (D\to E)\ar[d]^{\blank\circ c}\\
      \cocone{\trunc n \Ddiag}{E}\ar[r]^-{\blank\circ \tprojf[\Ddiag]n}\ar@{<-}[d]_{\ell_1} &
      \cocone{\Ddiag}{E}\ar@{<-}[d]^{\ell_2}\\
      (\reflect(A)\to{}E)\times_{(\reflect(C)\to{}E)}(\reflect(B)\to{}E)\ar[r] &
      (A\to{}E)\times_{(C\to{}E)}(B\to{}E)
      }}
  \end{equation*}
\egroup
  The upper horizontal arrow is an equivalence since $E$ is an $n$-type, while $\blank\circ c$ is an equivalence since $c$ is a pushout cocone.
  Thus, by the 2-out-of-3 property, to show that $\blank\circ \trunc nc$ is an equivalence, it will suffice to show that the upper square commutes and that the middle horizontal arrow is an equivalence.
  To see that the upper square commutes, let $t:\trunc nD \to E$; then
  \begin{align}
    \big(t \circ \trunc n c\big) \circ \tprojf[\Ddiag] n
    &= t \circ \big(\trunc n c \circ \tprojf[\Ddiag] n\big)
    \tag{by \cref{thm:conemap-funct}}\\
    &= t\circ \big(\tprojf[D]n \circ c\big)
    \tag{by~\eqref{eq:conetrunc}}\\
    &= \big(t\circ \tprojf[D]n\big) \circ c
    \tag{by~\eqref{eq:composeconefunc}}.
  \end{align}
  To show that the middle horizontal arrow is an equivalence, consider the lower square.
  The two lower vertical arrows are simply applications of $\happly$:
  \begin{align*}
    \ell_1(i,j,p) &\defeq (i,j,\happly(p))\\
    \ell_2(i,j,p) &\defeq (i,j,\happly(p))
  \end{align*}
  and hence are equivalences by function extensionality.
  The lowest horizontal arrow is defined by
  \[ (i,j,p) \mapsto \big( i\circ \tprojf[A]n,\;\; j \circ \tprojf[B] n,\;\; q\big) \]
  where $q$ is the composite
  \begin{align}
    i\circ \tprojf[A]n \circ f
    &= i\circ \trunc nf \circ \tprojf[C]n
    \tag{by $\funext(\lam{z} \apfunc{i}(\mathsf{nat}^f_n(z)))$}\\
    &= j\circ \trunc ng \circ \tprojf[C]n
    \tag{by $\apfunc{\blank\circ \tprojf[C] n}(p)$}\\
    &= j\circ \tprojf[B]n \circ g.
    \tag{by $\funext(\lam{z} \apfunc{j}(\mathsf{nat}^g_n(z)))$}
  \end{align}
  This is an equivalence, because it is induced by an equivalence of cospans.
  Thus, by 2-out-of-3, it will suffice to show that the lower square commutes.
  But the two composites around the lower square agree definitionally on the first two components, so it suffices to show that for $(i,j,p)$ in the lower left corner and $z:C$, the path
  \[ \happly(q,z) : i(\tproj n{f(z)}) = j(\tproj n{g(z)}) \]
  (with $q$ as above)
  is equal to the composite
  \begin{align}
    i(\tproj n{f(z)})
    &= i(\trunc nf(\tproj nz))
    \tag{by $\apfunc{i}(\mathsf{nat}^f_n(z))$}\\
    &= j(\trunc ng(\tproj nz))
    \tag{by $\happly(p,\tproj nz)$}\\
    &= j(\tproj n{g(z)}).
    \tag{by $\apfunc{j}(\mathsf{nat}^g_n(z))$}
  \end{align}
  However, since $\happly$ is functorial, it suffices to check equality for the three component paths:
  \begin{align*}
    \happly({\funext(\lam{z} \apfunc{i}(\mathsf{nat}^f_n(z)))},z)
    &= {\apfunc{i}(\mathsf{nat}^f_n(z))}\\
    \happly(\apfunc{\blank\circ \tprojf[C] n}(p), z)
    &= {\happly(p,\tproj nz)}\\
    \happly({\funext(\lam{z} \apfunc{j}(\mathsf{nat}^g_n(z)))},z)
    &= {\apfunc{j}(\mathsf{nat}^g_n(z))}.
  \end{align*}
  The first and third of these are just the fact that $\happly$ is quasi-inverse to $\funext$, while
  the second is an easy general lemma about $\happly$ and precomposition.
\end{proof}


\section{Connectedness}
\label{sec:connectivity}

An $n$-type is one that has no interesting information above dimension $n$.
By contrast, an \emph{$n$-connected type} is one that has no interesting information \emph{below} dimension $n$.
It turns out to be natural to study a more general notion for functions as well.

\begin{defn}
A function $f:A\to B$ is said to be \define{$n$-connected}
\indexdef{function!n-connected@$n$-connected}%
\indexsee{n-connected@$n$-connected!function}{function, $n$-connected}%
if for all $b:B$, the type $\trunc n{\hfiber f b}$ is contractible:
\begin{equation*}
  \mathsf{conn}_n(f)\defeq \prd{b:B}\iscontr(\trunc n{\hfiber{f}b}).
\end{equation*}
A type $A$ is said to be \define{$n$-connected}
\indexsee{n-connected@$n$-connected!type}{type, $n$-connected}%
\indexdef{type!n-connected@$n$-connected}%
 if the unique function $A\to\unit$ is $n$-connected, i.e.\ if $\trunc nA$ is contractible.
\end{defn}
\indexsee{connected!function}{function, $n$-connected}

Thus, a function $f:A\to B$ is $n$-connected if and only if $\hfib{f}b$ is $n$-connected for every $b:B$.
Of course, every function is $(-2)$-connected.
At the next level, we have:

\begin{lem}\label{thm:minusoneconn-surjective}
  \index{function!surjective}%
  A function $f$ is $(-1)$-connected if and only if it is surjective in the sense of \cref{sec:mono-surj}.
\end{lem}
\begin{proof}
  We defined $f$ to be surjective if $\trunc{-1}{\hfiber f b}$ is inhabited for all $b$.
  But since it is a mere proposition, inhabitation is equivalent to contractibility.
\end{proof}

Thus, $n$-connectedness of a function for $n\ge 0$ can be thought of as a strong form of surjectivity.
Category-theoretically, $(-1)$-connectedness corresponds to essential surjectivity on objects, while $n$-connectedness corresponds to essential surjectivity on $k$-morphisms for $k\le n+1$.

\cref{thm:minusoneconn-surjective} also implies that a type $A$ is $(-1)$-connected if and only if it is merely inhabited.
When a type is $0$-connected we may simply say that it is \define{connected},
\indexdef{connected!type}%
\indexdef{type!connected}%
and when it is $1$-connected we say it is \define{simply connected}.
\indexdef{simply connected type}%
\indexdef{type!simply connected}%

\begin{rmk}\label{rmk:connectedness-indexing}
  While our notion of $n$-connectedness for types agrees with the standard notion in homotopy theory, our notion of $n$-connectedness for \emph{functions} is off by one from a common indexing in classical homotopy theory.
  Whereas we say a function $f$ is $n$-connected if all its fibers are $n$-connected, some classical homotopy theorists would call such a function $(n+1)$-connected.
  (This is due to a historical focus on \emph{cofibers} rather than fibers.)
\end{rmk}

We now observe a few closure properties of connected maps.
\index{function!n-connected@$n$-connected}

\begin{lem}
\index{retract!of a function}%
Suppose that $g$ is a retract of a $n$-connected function $f$.  Then $g$ is
$n$-connected.
\end{lem}
\begin{proof}
This is a direct consequence of \cref{lem:func_retract_to_fiber_retract}.
\end{proof}

\begin{cor}
If $g$ is homotopic to a $n$-connected function $f$, then $g$ is $n$-connected.
\end{cor}

\begin{lem}\label{lem:nconnected_postcomp}
Suppose that $f:A\to B$ is $n$-connected. Then $g:B\to C$ is $n$-connected if and only if $g\circ f$ is
$n$-connected.
\end{lem}

\begin{proof}
For any $c:C$, we have
\begin{align*}
  \trunc n{\hfib{g\circ f}c}
  & \eqvsym \Trunc n{ \sm{w:\hfib{g}c}\hfib{f}{\proj1 w}}
  \tag{by \cref{ex:unstable-octahedron}}\\
  & \eqvsym \Trunc n{\sm{w:\hfib{g}c} \trunc n{\hfib{f}{\proj1 w}}}
  \tag{by \cref{thm:trunc-in-truncated-sigma}}\\
  & \eqvsym \trunc n{\hfib{g}c}.
  \tag{since $\trunc n{\hfib{f}{\proj1 w}}$ is contractible}
\end{align*}
It follows that $\trunc n{\hfib{g}c}$ is contractible if and only if $\trunc n{\hfib{g\circ f}c}$ is
contractible.
\end{proof}

Importantly, $n$-connected functions can be equivalently characterized as those which satisfy an ``induction principle'' with respect to $n$-types.\index{induction principle!for connected maps}
This idea will lead directly into our proof of the Freudenthal suspension theorem in \cref{sec:freudenthal}.

\begin{lem}\label{prop:nconnected_tested_by_lv_n_dependent types}
For $f:A\to B$ and $P:B\to\type$, consider the following function:
\begin{equation*}
\lam{s} s\circ f :\Parens{\prd{b:B} P(b)}\to\Parens{\prd{a:A}P(f(a))}.
\end{equation*}
For a fixed $f$ and $n\ge -2$, the following are equivalent.
\begin{enumerate}
\item $f$ is $n$-connected.\label{item:conntest1}
\item For every $P:B\to\ntype{n}$, the map $\lam{s} s\circ f$ is an equivalence.\label{item:conntest2}
\item For every $P:B\to\ntype{n}$, the map $\lam{s} s\circ f$ has a section.\label{item:conntest3}
\end{enumerate}
\end{lem}

\begin{proof}
Suppose that $f$ is $n$-connected and let $P:B\to\ntype{n}$. Then we have the equivalences
\begin{align}
  \prd{b:B} P(b) & \eqvsym \prd{b:B} \Parens{\trunc n{\hfib{f}b} \to P(b)}
  \tag{since $\trunc n{\hfib{f}b}$ is contractible}\\
  & \eqvsym \prd{b:B} \Parens{\hfib{f}b\to P(b)}
  \tag{since $P(b)$ is an $n$-type}\\
  & \eqvsym \prd{b:B}{a:A}{p:f(a)= b} P(b)
  \tag{by the left universal property of $\Sigma$-types}\\
  & \eqvsym \prd{a:A} P(f(a)).
  \tag{by the left universal property of path types}
\end{align}
We omit the proof that this equivalence is indeed given by $\lam{s} s\circ f$.
Thus,~\ref{item:conntest1}$\Rightarrow$\ref{item:conntest2}, and clearly~\ref{item:conntest2}$\Rightarrow$\ref{item:conntest3}.
To show~\ref{item:conntest3}$\Rightarrow$\ref{item:conntest1}, consider the type family
\begin{equation*}
P(b)\defeq \trunc n{\hfib{f}b}.
\end{equation*}
Then~\ref{item:conntest3} yields a map $c:\prd{b:B} \trunc n{\hfib{f}b}$ with
$c(f(a))=\tproj n{\pairr{a,\refl{f(a)}}}$. To show that each $\trunc n{\hfib{f}b}$ is contractible,
we will find a function of type
\begin{equation*}
\prd{b:B}{w:\trunc n{\hfib{f}b}} w= c(b).
\end{equation*}
By \cref{thm:truncn-ind}, for this it suffices to find a function of type
\begin{equation*}
\prd{b:B}{a:A}{p:f(a)= b} \tproj n{\pairr{a,p}}= c(b).
\end{equation*}
But by rearranging variables and path induction, this is equivalent to the type
\begin{equation*}
\prd{a:A} \tproj n{\pairr{a,\refl{f(a)}}}= c(f(a)).
\end{equation*}
This property holds by our choice of $c(f(a))$.
\end{proof}

\begin{cor}\label{cor:totrunc-is-connected}
For any $A$, the canonical function $\tprojf n:A\to\trunc n A$ is $n$-connected.
\end{cor}
\begin{proof}
By \cref{thm:truncn-ind} and the associated uniqueness principle, the condition of \cref{prop:nconnected_tested_by_lv_n_dependent types} holds.
\end{proof}

For instance, when $n=-1$, \cref{cor:totrunc-is-connected} says that the map $A\to \brck A$ from a type to its propositional truncation is surjective.

\begin{cor}\label{thm:nconn-to-ntype-const}\label{connectedtotruncated}
A type $A$ is $n$-connected if and only if the map
\begin{equation*}
  \lam{b}{a} b: B \to (A\to B)
\end{equation*}
is an equivalence for every $n$-type $B$.
In other words, ``every map from $A$ to an $n$-type is constant''.
\end{cor}
\begin{proof}
  By \cref{prop:nconnected_tested_by_lv_n_dependent types} applied to a function with codomain $\unit$.
\end{proof}

\begin{lem}\label{lem:nconnected_to_leveln_to_equiv}
Let $B$ be an $n$-type and let $f:A\to B$ be a function. Then the induced function $g:\trunc n A\to B$ is an
equivalence if and only if $f$ is $n$-connected.
\end{lem}

\begin{proof}
By \cref{cor:totrunc-is-connected}, $\tprojf n$ is $n$-connected.
Thus, since $f = g\circ \tprojf n$, by
\cref{lem:nconnected_postcomp} $f$ is $n$-connected if and only if $g$ is $n$-connected.
But since $g$ is a function between $n$-types, its fibers are also $n$-types.
Thus, $g$ is $n$-connected if and only if it is an equivalence.
\end{proof}

We can also characterize connected pointed types in terms of connectivity of the inclusion of their basepoint.

\begin{lem}\label{thm:connected-pointed}
  \index{basepoint}%
  Let $A$ be a type and $a_0:\unit\to A$ a basepoint, with $n\ge -1$.
  Then $A$ is $n$-connected if and only if the map $a_0$ is $(n-1)$-connected.
\end{lem}
\begin{proof}
  First suppose $a_0:\unit\to A$ is $(n-1)$-connected and let $B$ be an $n$-type; we will use \cref{thm:nconn-to-ntype-const}.
  The map $\lam{b}{a} b: B \to (A\to B)$ has a retraction given by $f\mapsto f(a_0)$, so it suffices to show it also has a section, i.e.\ that for any $f:A\to B$ there is $b:B$ such that $f = \lam{a}b$.
  We choose $b\defeq f(a_0)$.
  Define $P:A\to\type$ by $P(a) \defeq (f(a)=f(a_0))$.
  Then $P$ is a family of $(n-1)$-types and we have $P(a_0)$; hence we have $\prd{a:A} P(a)$ since $a_0:\unit\to A$ is $(n-1)$-connected.
  Thus, $f = \lam{a} f(a_0)$ as desired.

  Now suppose $A$ is $n$-connected, and let $P:A\to\ntype{(n-1)}$ and $u:P(a_0)$ be given.
  By \cref{prop:nconnected_tested_by_lv_n_dependent types}, it will suffice to construct $f:\prd{a:A} P(a)$ such that $f(a_0)=u$.
  Now $\ntype{(n-1)}$ is an $n$-type and $A$ is $n$-connected, so by \cref{thm:nconn-to-ntype-const}, there is an $n$-type $B$ such that $P = \lam{a} B$.
  Hence, we have a family of equivalences $g:\prd{a:A} (\eqv{P(a)}{B})$.
  Define $f(a) \defeq \opp{g_a}(g_{a_0}(u))$; then $f:\prd{a:A} P(a)$ and $f(a_0) = u$ as desired.
\end{proof}

In particular, a pointed type $(A,a_0)$ is 0-connected if and only if $a_0:\unit\to A$ is surjective, which is to say $\prd{x:A} \brck{x=a_0}$.

A useful variation on \cref{lem:nconnected_postcomp} is:

\begin{lem}\label{lem:nconnected_postcomp_variation}
Let $f:A\to B$ be a function and $P:A\to\type$ and $Q:B\to\type$ be type families. Suppose that $g:\prd{a:A} P(a)\to Q(f(a))$
is a fiberwise $n$-connected%
\index{fiberwise!n-connected family of functions@$n$-connected family of functions}
family of functions, i.e.\ each function $g_a : P(a) \to Q(f(a))$ is $n$-connected. Then the function
\begin{align*}
\varphi &:\Parens{\sm{a:A} P(a)}\to\Parens{\sm{b:B} Q(b)}\\
\varphi(a,u) &\defeq \pairr{f(a),g_a(u)}
\end{align*}
is $n$-connected if and only if $f$ is $n$-connected.
\end{lem}

\begin{proof}
For $b:B$ and $v:Q(b)$ we have
{\allowdisplaybreaks
\begin{align*}
\trunc n{\hfib{\varphi}{\pairr{b,v}}} & \eqvsym \Trunc n{\sm{a:A}{u:P(a)}{p:f(a)= b} \trans{\ap f p }{g_a(u)}= v}\\
& \eqvsym \Trunc n{\sm{w:\hfib{f}b}{u:P(\proj1(w))} g_{\proj 1 w}(u)= \trans{\opp{\ap f {\proj2 w}}}{v}}\\
& \eqvsym \Trunc n{\sm{w:\hfib{f}b} \hfib{g(\proj1 w)}{\trans{\opp{\ap f {\proj 2 w}}}{v}}}\\
& \eqvsym \Trunc n{\sm{w:\hfib{f}b} \trunc n{\hfib{g(\proj1 w)}{\trans{\opp{\ap f {\proj 2 w}}}{v}}}}\\
& \eqvsym \trunc n{\hfib{f}b}
\end{align*}}
where the transportations along $f(p)$ and $f(p)^{-1}$ are with respect to $Q$.
Therefore, if either is contractible, so is the other.
\end{proof}

In the other direction, we have

\begin{lem}\label{prop:nconn_fiber_to_total}
Let $P,Q:A\to\type$ be type families and consider a fiberwise transformation\index{fiberwise!transformation}
\begin{equation*}
f:\prd{a:A} \Parens{P(a)\to Q(a)}
\end{equation*}
from $P$ to $Q$. Then the induced map $\total f: \sm{a:A}P(a) \to \sm{a:A} Q(a)$ is $n$-connected if and only if each $f(a)$ is $n$-connected.
\end{lem}

\begin{proof}
By \cref{fibwise-fiber-total-fiber-equiv}, we have
$\hfib{\total f}{\pairr{x,v}}\eqvsym\hfib{f(x)}v$
for each $x:A$ and $v:Q(x)$. Hence $\trunc n{\hfib{\total f}{\pairr{x,v}}}$ is contractible if and only if
$\trunc n{\hfib{f(x)}v}$ is contractible.
\end{proof}

Another useful fact about connected maps is that they induce an
equivalence on $n$-truncations:

\begin{lem} \label{lem:connected-map-equiv-truncation}
If $f : A \to B$ is $n$-connected, then it induces an equivalence
$\eqv{\trunc{n}{A}}{\trunc{n}{B}}$.
\end{lem}
\begin{proof}
Let $c$ be the proof that $f$ is $n$-connected.  From left to right, we
use the map $\trunc{n}{f} : \trunc{n}{A} \to \trunc{n}{B}$.
To define the map from right to left, by the universal property of
truncations, it suffices to give a map $\mathsf{back} : B \to {\trunc{n}{A}}$.  We can
define this map as follows:
\[
\mathsf{back}(y) \defeq \trunc{n}{\proj{1}}{(\proj{1}{(c(y))})}
\]
By definition, $c(y)$ has type $\iscontr(\trunc n {\hfiber{f}y})$, so its
first component has type $\trunc n{\hfiber{f}y}$, and we can obtain an
element of $\trunc n A$ from this by projection.

Next, we show that the composites are the identity.  In both directions,
because the goal is a path in an $n$-truncated type, it suffices to
cover the case of the constructor $\tprojf{n}$.

In one direction, we must show that for all $x:A$,
\[
\trunc{n}{\proj{1}}{(\proj{1}{(c(f(x)))})} = \tproj{n}{x}
\]
But $\tproj{n}{(x, \refl{f(x)})} : \trunc n{\hfiber{f}{f(x)}}$, and
$c(f(x))$ says that this type is contractible, so
\[
\proj{1}{(c(f(x)))} = \tproj{n}{(x, \refl{})}
\]
Applying $\trunc{n}{\proj{1}}$ to both sides of this equation gives the
result.

In the other direction, we must show that for all $y:B$,
\[
\trunc{n}{f}(\trunc{n}{\proj{1}} (\proj{1}{(c(y))})) = \tproj{n}{y}
\]
$\proj{1}{(c(y))}$ has type $\trunc n {\hfiber{f}y}$, and the path we
want is essentially the second component of the $\hfiber{f}y$, but we
need to make sure the truncations work out.

In general, suppose we are given $p:\trunc{n}{\sm{x:A} B(x)}$ and wish to prove
$P(\trunc{n}{\proj{1}{}}(p))$. By truncation induction, it suffices to
prove $P(\tproj{n}{a})$ for all $a:A$ and $b:B(a)$.  Applying this
principle in this case, it suffices to prove
\[
\trunc{n}{f}(\tproj{n}{a}) = \tproj{n}{y}
\]
given $a:A$ and $b:f (a) = y$.  But the left-hand side equals $\tproj{n}{f (a)}$,
so applying $\tprojf{n}$ to both sides of $b$ gives the result.
\end{proof}

One might guess that this fact characterizes the $n$-connected maps, but in fact being $n$-connected is a bit stronger than this.
For instance, the inclusion $\bfalse:\unit \to\bool$ induces an equivalence on $(-1)$-truncations, but is not surjective (i.e.\ $(-1)$-connected).
In \cref{sec:long-exact-sequence-homotopy-groups} we will see that the difference in general is an analogous extra bit of surjectivity.


\section{Orthogonal factorization}
\label{sec:image-factorization}

\index{unique!factorization system|(}%
\index{orthogonal factorization system|(}%
In set theory, the surjections and the injections form a unique factorization system: every function factors essentially uniquely as a surjection followed by an injection.
We have seen that surjections generalize naturally to $n$-connected maps, so it is natural to inquire whether these also participate in a factorization system.
Here is the corresponding generalization of injections.

\begin{defn}
  A function $f:A\to B$ is \define{$n$-truncated}
  \indexdef{n-truncated@$n$-truncated!function}%
  \indexdef{function!n-truncated@$n$-truncated}%
if the fiber $\hfib f b$ is an $n$-type for all $b:B$.
\end{defn}

In particular, $f$ is $(-2)$-truncated if and only if it is an equivalence.
And of course, $A$ is an $n$-type if and only if $A\to\unit$ is $n$-truncated.
Moreover, $n$-truncated maps could equivalently be defined recursively, like $n$-types.

\begin{lem}\label{thm:modal-mono}
  For any $n\ge -2$, a function $f:A\to B$ is $(n+1)$-truncated if and only if for all $x,y:A$, the map $\apfunc{f}:(x=y) \to (f(x)=f(y))$ is $n$-truncated.
  \index{function!embedding}%
  \index{function!injective}%
  In particular, $f$ is $(-1)$-truncated if and only if it is an embedding in the sense of \cref{sec:mono-surj}.
\end{lem}
\begin{proof}
  Note that for any $(x,p),(y,q):\hfib f b$, we have
  \begin{align*}
    \big((x,p) = (y,q)\big)
    &= \sm{r:x=y} (p = \apfunc f(r)\ct q)\\
    &= \sm{r:x=y} (\apfunc f (r) = p\ct \opp q)\\
    &= \hfib{\apfunc{f}}{p\ct \opp q}.
  \end{align*}
  Thus, any path space in any fiber of $f$ is a fiber of $\apfunc{f}$.
  On the other hand, choosing $b\defeq f(y)$ and $q\defeq \refl{f(y)}$ we see that any fiber of $\apfunc f$ is a path space in a fiber of $f$.
  The result follows, since $f$ is $\nplusone$-truncated if all path spaces of its fibers are $n$-types.
\end{proof}

We can now construct the factorization, in a fairly obvious way.

\begin{defn}\label{defn:modal-image}
Let $f:A\to B$ be a function. The \define{$n$-image}
\indexdef{image}%
\indexdef{image!n-image@$n$-image}%
\indexdef{n-image@$n$-image}%
\indexdef{function!n-image of@$n$-image of}%
of $f$ is defined as
\begin{equation*}
\im_n(f)\defeq \sm{b:B} \trunc n{\hfib{f}b}.
\end{equation*}
When $n=-1$, we write simply $\im(f)$ and call it the \define{image} of $f$.
\end{defn}

\begin{lem}\label{prop:to_image_is_connected}
For any function $f:A\to B$, the canonical function $\tilde{f}:A\to\im_n(f)$ is $n$-connected.
Consequently, any function factors as an $n$-connected function followed by an $n$-truncated function.
\end{lem}

\begin{proof}
Note that $A\eqvsym\sm{b:B}\hfib{f}b$. The function $\tilde{f}$ is the function on total spaces induced by the canonical fiberwise transformation
\begin{equation*}
\prd{b:B} \Parens{\hfib{f}b\to\trunc n{\hfib{f}b}}.
\end{equation*}
Since each map $\hfib{f}b\to\trunc n{\hfib{f}b}$ is $n$-connected by \cref{cor:totrunc-is-connected}, $\tilde{f}$ is $n$-connected by \cref{prop:nconn_fiber_to_total}.
Finally, the projection $\proj1:\im_n(f) \to B$ is $n$-truncated, since its fibers are equivalent to the $n$-truncations of the fibers of $f$.
\end{proof}

In the following lemma we set up some machinery to prove the unique factorization theorem.

\begin{lem}\label{prop:factor_equiv_fiber}
Suppose we have a commutative diagram of functions
\begin{equation*}
  \xymatrix{
    {A} \ar[r]^{g_1} \ar[d]_{g_2} &
    {X_1} \ar[d]^{h_1} &
    \\
    {X_2} \ar[r]_{h_2}
    &
    {B}
  }
\end{equation*}
with $H:h_1\circ g_1\htpy h_2\circ g_2$, where $g_1$ and $g_2$ are $n$-connected and where $h_1$ and $h_2$ are $n$-truncated.
Then there is an equivalence
\begin{equation*}
E(H,b):\hfib{h_1}b\eqvsym\hfib{h_2}b
\end{equation*}
for any $b:B$, such that for any $a:A$ we have an identification
\[\overline{E}(H,a) :  E(H,h_1(g_1(a)))({g_1(a),\refl{h_1(g_1(a))}}) = \pairr{g_2(a),\opp{H(a)}}.\]
\end{lem}

\begin{proof}
Let $b:B$. Then we have the following equivalences:
\begin{align}
\hfib{h_1}b
& \eqvsym \sm{w:\hfib{h_1}b} \trunc n{ \hfib{g_1}{\proj1 w}}
\tag{since $g_1$ is $n$-connected}\\
& \eqvsym \Trunc n{\sm{w:\hfib{h_1}b}\hfib{g_1}{\proj1 w}}
\tag{by \cref{thm:refl-over-ntype-base}, since $h_1$ is $n$-truncated}\\
& \eqvsym \trunc n{\hfib{h_1\circ g_1}b}
\tag{by \cref{ex:unstable-octahedron}}
\end{align}
and likewise for $h_2$ and $g_2$.
Also, since we have a homotopy $H:h_1\circ g_1\htpy h_2\circ g_2$, there is an obvious equivalence $\hfib{h_1\circ g_1}b\eqvsym\hfib{h_2\circ g_2}b$.
Hence we obtain
\begin{equation*}
\hfib{h_1}b\eqvsym\hfib{h_2}b
\end{equation*}
for any $b:B$. By analyzing the underlying functions, we get the following representation of what happens to the element
$\pairr{g_1(a),\refl{h_1(g_1(a))}}$ after applying each of the equivalences of which $E$ is composed.
Some of the identifications are definitional, but others (marked with a $=$ below) are only propositional; putting them together we obtain $\overline E(H,a)$.
{\allowdisplaybreaks
\begin{align*}
\pairr{g_1(a),\refl{h_1(g_1(a))}} &
    \overset{=}{\mapsto} \Pairr{\pairr{g_1(a),\refl{h_1(g_1(a))}}, \tproj n{ \pairr{a,\refl{g_1(a)}}}}\\
  & \mapsto \tproj n { \pairr{\pairr{g_1(a),\refl{h_1(g_1(a))}}, \pairr{a,\refl{g_1(a)}} }}\\
  & \mapsto \tproj n { \pairr{a,\refl{h_1(g_1(a))}}}\\
  & \overset{=}{\mapsto} \tproj n { \pairr{a,\opp{H(a)}}}\\
  & \mapsto \tproj n { \pairr{\pairr{g_2(a),\opp{H(a)}},\pairr{a,\refl{g_2(a)}}} }\\
  & \mapsto \Pairr{\pairr{g_2(a),\opp{H(a)}}, \tproj n {\pairr{a,\refl{g_2(a)}}} }\\
  & \mapsto \pairr{g_2(a),\opp{H(a)}}
\end{align*}}
The first equality is because for general $b$, the map
\narrowequation{ \hfib{h_1}b \to \sm{w:\hfib{h_1}b} \trunc n{ \hfib{g_1}{\proj1 w}} }
inserts the center of contraction for $\trunc n{ \hfib{g_1}{\proj1 w}}$ supplied by the assumption that $g_1$ is $n$-truncated; whereas in the case in question this type has the obvious inhabitant $\tproj n{ \pairr{a,\refl{g_1(a)}}}$, which by contractibility must be equal to the center.
The second propositional equality is because the equivalence $\hfib{h_1\circ g_1}b\eqvsym\hfib{h_2\circ g_2}b$ concatenates the second components with $\opp{H(a)}$, and we have $\opp{H(a)} \ct \refl{} = \opp{H(a)}$.
The reader may check that the other equalities are definitional (assuming a reasonable solution to \cref{ex:unstable-octahedron}).
\end{proof}

% The equivalences $E(H,b)$ are such that $E(H^{-1},b)= E(H,b)^{-1}$.

Combining \cref{prop:to_image_is_connected,prop:factor_equiv_fiber}, we have the following unique factorization result:

\begin{thm}\label{thm:orth-fact}
For each $f:A\to B$, the space $\fact_n(f)$ defined by
\begin{equation*}
\sm{X:\type}{g:A\to X}{h:X\to B} (h\circ g\htpy f)\times\mathsf{conn}_n(g)\times\mathsf{trunc}_n(h).
\end{equation*}
is contractible.
Its center of contraction is the element
\begin{equation*}
\pairr{\im_n(f),\tilde{f},\proj1,\theta,\varphi,\psi}:\fact_n(f)
\end{equation*}
arising from \cref{prop:to_image_is_connected},
where $\theta:\proj1\circ\tilde{f}\htpy f$ is the canonical homotopy, where $\varphi$ is the proof of
\cref{prop:to_image_is_connected}, and where $\psi$ is the obvious proof that $\proj1:\im_n(f)\to B$ has $n$-truncated fibers.
\end{thm}

\begin{proof}
By \cref{prop:to_image_is_connected} we know that there is an element of $\fact_n(f)$, hence it is enough to
show that $\fact_n(f)$ is a mere proposition. Suppose we have two $n$-factorizations
\begin{equation*}
\pairr{X_1,g_1,h_1,H_1,\varphi_1,\psi_1}\qquad\text{and}\qquad\pairr{X_2,g_2,h_2,H_2,\varphi_2,\psi_2}
\end{equation*}
of $f$. Then we have the pointwise-concatenated homotopy
\[ H\defeq (\lam{a} H_1(a) \ct H_2^{-1}(a)) \,:\, (h_1\circ g_1\htpy h_2\circ g_2).\]
By univalence and the characterization of paths and transport in $\Sigma$-types, function types, and path types, it suffices to show that
\begin{enumerate}
\item there is an equivalence $e:X_1\eqvsym X_2$,
\item there is a homotopy $\zeta:e\circ g_1\htpy g_2$,
% \note{Is it easy enough to see that these elements are the various transports?}
\item there is a homotopy $\eta:h_2\circ e\htpy h_1$,
\item for any $a:A$ we have $\opp{\apfunc{h_2}(\zeta(a))} \ct \eta(g_1(a)) \ct H_1(a) = H_2(a)$.
\end{enumerate}
%where $\underline{e}$ is the function underlying the equivalence.
We prove these four assertions in that order.
\begin{enumerate}
\item By \cref{prop:factor_equiv_fiber}, we have a fiberwise equivalence
% \note{It could be a nice exercise for the book to show
% that if $f_1:A_1\to B$ and $f_2:A_2\to B$ have equivalent fibers, then $A_1\eqvsym A_2$}.
\begin{equation*}
E(H) : \prd{b:B} \eqv{\hfib{h_1}b}{\hfib{h_2}b}.
\end{equation*}
This induces an equivalence of total spaces, i.e.\ we have
\begin{equation*}
\eqvspaced{\Parens{\sm{b:B} \hfib{h_1}b}}{\Parens{\sm{b:B}\hfib{h_2}b}}.
\end{equation*}
Of course, we also have the equivalences $X_1\eqvsym\sm{b:B}\hfib{h_1}b$ and $X_2\eqvsym\sm{b:B}
\hfib{h_2}b$ from \cref{thm:total-space-of-the-fibers}.
This gives us our equivalence $e:X_1\eqvsym X_2$; the reader may verify that the underlying function of $e$ is given by
\begin{equation*}
e(x) \jdeq \proj1(E(H,h_1(x))(x,\refl{h_1(x)})).
\end{equation*}
\item By \cref{prop:factor_equiv_fiber}, we may choose
  $\zeta(a) \defeq \apfunc{\proj1}(\overline E(H,a)) : e(g_1(a)) = g_2(a)$.
  \label{item:orth-fact-2}
\item For every $x:X_1$, we have
\begin{equation*}
\proj2(E(H,h_1(x))({x,\refl{h_1(x)}})) :h_2(e(x))= h_1(x),
\end{equation*}
giving us a homotopy $\eta:h_2\circ e\htpy h_1$.
\item By the characterization of paths in fibers (\cref{lem:hfib}), the path $\overline E(H,a)$ from \cref{prop:factor_equiv_fiber} gives us
  $\eta(g_1(a)) = \apfunc{h_2}(\zeta(a)) \ct \opp{H(a)}$.
  The desired equality follows by substituting the definition of $H$ and rearranging paths.\qedhere
\end{enumerate}
\end{proof}

% I can't make sense of this, and it doesn't seem necessary
%
% \begin{cor}
% A function $f:A\to B$ is $n$-connected if and only if
% \begin{equation*}
% \prd C\prd{g:\modalfunc(B\to C)} \iscontr\big(\sm{h:\modalfunc(B\to C)}\underline{h}\circ
% f\htpy\underline{g}\circ f\big).
% \end{equation*}
% \end{cor}

By standard arguments, this yields the following orthogonality principle.

\begin{thm}
  Let $e:A\to B$ be $n$-connected and $m:C\to D$ be $n$-truncated.
  Then the map
  \[ \varphi: (B\to C) \;\to\; \sm{h:A\to C}{k:B\to D} (m\circ h \htpy k \circ e) \]
  is an equivalence.
\end{thm}
\begin{proof}[Sketch of proof]
  For any $(h,k,H)$ in the codomain, let $h = h_2 \circ h_1$ and $k = k_2 \circ k_1$, where $h_1$ and $k_1$ are $n$-connected and $h_2$ and $k_2$ are $n$-truncated.
  Then $f = (m\circ h_2) \circ h_1$ and $f = k_2 \circ (k_1\circ e)$ are both $n$-factorizations of $m \circ h = k\circ e$.
  Thus, there is a unique equivalence between them.
  It is straightforward (if a bit tedious) to extract from this that $\hfib\varphi{(h,k,H)}$ is contractible.
\end{proof}

\index{orthogonal factorization system|)}%
\index{unique!factorization system|)}%

We end by showing that images are stable under pullback.
\index{image!stability under pullback}
\index{factorization!stability under pullback}

\begin{lem}\label{lem:hfiber_wrt_pullback}
Suppose that the square
\begin{equation*}
  \vcenter{\xymatrix{
      A\ar[r]\ar[d]_f &
      C\ar[d]^g\\
      B\ar[r]_-h &
      D
      }}
\end{equation*}
is a pullback square and let $b:B$. Then $\hfib{f}b\eqvsym\hfib{g}{h(b)}$.
\end{lem}

\begin{proof}
This follows from pasting of pullbacks (\cref{ex:pullback-pasting}), since the type $X$ in the diagram
\begin{equation*}
  \vcenter{\xymatrix{
      X\ar[r]\ar[d] &
      A\ar[r]\ar[d]_f &
      C\ar[d]^g\\
      \unit\ar[r]_b &
      B\ar[r]_h &
      D
      }}
\end{equation*}
is the pullback of the left square if and only if it is the pullback of the outer rectangle, while $\hfib{f}b$ is the pullback of the square on the left and $\hfib{g}{h(b)}$ is the pullback of the outer rectangle.
\end{proof}

\begin{thm}\label{thm:stable-images}
\index{stability!of images under pullback}%
Consider functions $f:A\to B$, $g:C\to D$ and the diagram
\begin{equation*}
  \vcenter{\xymatrix{
      A\ar[r]\ar[d]_{\tilde{f}_n} &
      C\ar[d]^{\tilde{g}_n}\\
      \im_n(f)\ar[r]\ar[d]_{\proj1} &
      \im_n(g)\ar[d]^{\proj1}\\
      B\ar[r]_h &
      D
      }}
\end{equation*}
If the outer rectangle is a pullback, then so is the bottom square (and hence so is the top square, by \cref{ex:pullback-pasting}). Consequently, images are stable under pullbacks.
\end{thm}

\begin{proof}
Assuming the outer square is a pullback, we have equivalences
\begin{align*}
B\times_D\im_n(g) & \jdeq \sm{b:B}{w:\im_n(g)} h(b)=\proj1 w\\
& \eqvsym \sm{b:B}{d:D}{w:\trunc n{\hfib{g}d}} h(b)= d\\
& \eqvsym \sm{b:B} \trunc n{\hfib{g}{h(b)}}\\
& \eqvsym \sm{b:B} \trunc n{\hfib{f}b} &&
\text{(by \cref{lem:hfiber_wrt_pullback})}\\
& \equiv \im_n(f). && \qedhere
\end{align*}
\end{proof}

\index{n-type@$n$-type|)}%

\section{Modalities}
\label{sec:modalities}

\index{modality|(}

Nearly all of the theory of $n$-types and connectedness can be done in much greater generality.
This section will not be used in the rest of the book.

Our first thought regarding generalizing the theory of $n$-types might be to take \cref{thm:trunc-reflective} as a definition.

\begin{defn}\label{defn:reflective-subuniverse}
  A \define{reflective subuniverse}
  \indexdef{reflective!subuniverse}%
  \indexdef{subuniverse, reflective}%
  is a predicate $P:\type\to\prop$ such that
  for every $A:\type$ we have a type $\reflect A$ such that $P(\reflect A)$ and a map
  $\project_A:A\to\reflect A$, with the property that for every $B:\type$ with $P(B)$, the following map is an equivalence:
  \[\function{(\reflect A\to{}B)}{(A\to{}B)}{f}{f\circ\project_A}.\]
\end{defn}

We write $\P \defeq \setof{A:\type | P(A)}$, so $A:\P$ means that $A:\type$ and we have $P(A)$.
We also write $\rec{\modal}$ for the quasi-inverse of the above map.
The notation $\reflect$ may seem slightly odd, but it will make more sense soon.

For any reflective subuniverse, we can prove all the familiar facts about reflective subcategories from category theory, in the usual way.
For instance, we have:
\begin{itemize}
\item A type $A$ lies in $\P$ if and only if $\project_A:A\to\reflect A$ is an equivalence.
\item $\P$ is closed under retracts.
  In particular, $A$ lies in $\P$ as soon as $\project_A$ admits a retraction.
\item The operation $\reflect$ is a functor in a suitable up-to-coherent-homotopy sense, which we can make precise at as high levels as necessary.
\item The types in $\P$ are closed under all limits such as products and pullbacks.
  In particular, for any $A:\P$ and $x,y:A$, the identity type $(x=_A y)$ is also in $\P$, since it is a pullback of two functions $\unit\to A$.
\item Colimits in $\P$ can be constructed by applying $\reflect$ to ordinary colimits of types.
\end{itemize}

Importantly, closure under products extends also to ``infinite products'', i.e.\ dependent function types.

\begin{thm}\label{thm:reflsubunv-forall}
  If $B:A\to\P$ is any family of types in a reflective subuniverse \P, then $\prd{x:A} B(x)$ is also in \P.
\end{thm}
\begin{proof}
  For any $x:A$, consider the function $\mathsf{ev}_x : (\prd{x:A} B(x)) \to B(x)$ defined by $\mathsf{ev}_x(f) \defeq f(x)$.
  Since $B(x)$ lies in $P$, this extends to a function
  \[ \rec{\modal}(\mathsf{ev}_x) : \reflect\Parens{\prd{x:A} B(x)} \to B(x). \]
  Thus we can define $h:\reflect(\prd{x:A} B(x)) \to \prd{x:A} B(x)$ by $h(z)(x) \defeq \rec{\modal}(\mathsf{ev}_x)(z)$.
  Then $h$ is a retraction of $\project_{\prd{x:A} B(x)}$, so that ${\prd{x:A} B(x)}$ is in $\P$.
\end{proof}

In particular, if $B:\P$ and $A$ is any type, then $(A\to B)$ is in \P.
In categorical language, this means that any reflective subuniverse is an \define{exponential ideal}.
\indexdef{exponential ideal}%
This, in turn, implies by a standard argument that the reflector preserves finite products.

\begin{cor}\label{cor:trunc_prod}
  For any types $A$ and $B$ and any reflective subuniverse, the induced map $\reflect(A\times B) \to \reflect(A) \times \reflect(B)$ is an equivalence.
\end{cor}
\begin{proof}
  It suffices to show that $\reflect(A) \times \reflect(B)$ has the same universal property as $\reflect(A\times B)$.
  Thus, let $C:\P$; we have
  \begin{align*}
    (\reflect(A) \times \reflect(B) \to C)
    &= (\reflect(A) \to (\reflect(B) \to C))\\
    &= (\reflect(A) \to (B \to C))\\
    &= (A \to (B \to C))\\
    &= (A \times B \to C)
  \end{align*}
  using the universal properties  of $\reflect(B)$ and $\reflect(A)$, along with the fact that $B\to C$ is in \P since $C$ is.
  It is straightforward to verify that this equivalence is given by composing with $\mreturn_A \times \mreturn_B$, as needed.
\end{proof}

It may seem odd that every reflective subcategory of types is automatically an exponential ideal, with a product-preserving reflector.
However, this is also the case classically in the category of \emph{sets}, for the same reasons.
It's just that this fact is not usually remarked on, since the classical category of sets---in contrast to the category of homotopy
types---does not have many interesting reflective subcategories.

Two basic properties of $n$-types are \emph{not} shared by general reflective subuniverses: \cref{thm:ntypes-sigma} (closure under $\Sigma$-types) and \cref{thm:truncn-ind} (truncation induction).
However, the analogues of these two properties are equivalent to each other.


\begin{thm}\label{thm:modal-char}
  For a reflective subuniverse \P, the following are logically equivalent.
  \begin{enumerate}
  \item If $A:\P$ and $B:A\to \P$, then $\sm{x:A} B(x)$ is in \P.\label{item:mchr1}
  \item for every $A:\type$, type family $B:\reflect A\to\P$, and map $g:\prd{a:A} B(\project(a))$, there exists $f:\prd{z:\reflect A} B(z)$ such that $f(\project(a)) = g(a)$ for all $a:A$.\label{item:mchr2}
  \end{enumerate}
\end{thm}
\begin{proof}
  Suppose~\ref{item:mchr1}.
  Then in the situation of~\ref{item:mchr2}, the type $\sm{z:\reflect A} B(z)$ lies in $\P$, and we have $g':A\to \sm{z:\reflect A} B(z)$ defined by $g'(a)\defeq (\project(a),g(a))$.
  Thus, we have $\rec{\modal}(g'):\reflect A \to \sm{z:\reflect A} B(z)$ such that $\rec{\modal}(g')(\project(a)) = (\project(a),g(a))$.

  Now consider the functions $\proj1 \circ \rec{\modal}(g') : \reflect A \to \reflect A$ and $\idfunc[\reflect A]$.
  By assumption, these become equal when precomposed with $\project$.
  Thus, by the universal property of $\reflect$, they are equal already, i.e.\ we have $p_z:\proj1(\rec{\modal}(g')(z)) = z$ for all $z$.
  Now we can define
  %
  \narrowequation{f(z) \defeq \trans{p_z}{\proj2(\rec{\modal}(g')(z))},}
  %
  Using the adjunction property of the equivalence of
  definition~\ref{defn:reflective-subuniverse}, one can show that the first component of
  %
  \narrowequation{\rec{\modal}(g')(\project(a)) = (\project(a),g(a))}
  %
  is equal to $p_{\project(a)}$.  Thus, its second component yields
  $f(\project(a)) = g(a)$, as needed.

  Conversely, suppose~\ref{item:mchr2}, and that $A:\P$ and $B:A\to\P$.
  Let $h$ be the composite
  \[ \reflect\Parens{\sm{x:A} B(x)} \xrightarrow{\reflect(\proj1)} \reflect A \xrightarrow{\opp{(\project_A)}} A. \]
  Then for $z:\sm{x:A} B(x)$ we have
  \begin{align*}
    h(\project(z)) &= \opp\project(\reflect(\proj1)(\project(z)))\\
    &= \opp\project(\project(\proj1(z)))\\
    &= \proj1(z).
  \end{align*}
  Denote this path by $p_z$.
  Now if we define $C:\reflect(\sm{x:A} B(x)) \to \type$ by $C(w) \defeq B(h(w))$, we have
  \[ g \defeq \lam{z} \trans{p_z}{\proj2(z)} \;:\; \prd{z:\sm{x:A} B(x)} C(\project(z)). \]
  Thus, the assumption yields
  %
  \narrowequation{f:\prd{w:\reflect(\sm{x:A}B(x))} C(w)}
  %
  such that $f(\project(z)) = g(z)$.
  Together, $h$ and $f$ give a function
  %
  \narrowequation{k:\reflect(\sm{x:A}B(x)) \to \sm{x:A}B(x)}
  %
  defined by $k(w) \defeq (h(w),f(w))$, while $p_z$ and the equality $f(\project(z)) = g(z)$ show that $k$ is a retraction of $\project_{\sm{x:A}B(x)}$.
  Therefore, $\sm{x:A}B(x)$ is in \P.
\end{proof}

Note the similarity to the discussion in \cref{sec:htpy-inductive}.
\index{recursion principle!for a modality}%
\index{induction principle!for a modality}%
\index{uniqueness!principle, propositional!for a modality}%
The universal property of the reflector of a reflective subuniverse is like a recursion principle with its uniqueness property, while \cref{thm:modal-char}\ref{item:mchr2} is like the corresponding induction principle.
Unlike in \cref{sec:htpy-inductive}, the two are not equivalent here, because of the restriction that we can only eliminate into types that lie in $\P$.
Condition~\ref{item:mchr1} of \cref{thm:modal-char} is what fixes the disconnect.

Unsurprisingly, of course, if we have the induction principle, then we can derive the recursion principle.
We can also derive its uniqueness property, as long as we allow ourselves to eliminate into path types.
This suggests the following definition.
Note that any reflective subuniverse can be characterized by the operation $\reflect:\type\to\type$ and the functions $\project_A:A\to \reflect A$, since we have $P(A) = \isequiv(\project_A)$.

\begin{defn}\label{defn:modality}
A \define{modality}
\indexdef{modality}
is an operation $\modal:\type\to\type$ for which there are
\begin{enumerate}
\item functions $\mreturn^\modal_A:A\to\modal(A)$ for every type $A$.\label{item:modal1}
\item for every $A:\type$ and every type family $B:\modal(A)\to\type$, a function\label{item:modal2}
\begin{equation*}
\ind{\modal}:\Parens{\prd{a:A}\modal(B(\mreturn^\modal_A(a)))}\to\prd{z:\modal(A)}\modal(B(z)).
\end{equation*}
\item A path $\ind\modal(f)(\mreturn^\modal_A(a)) = f(a)$ for each $f:\prd{a:A}\modal(B(\mreturn^\modal_A(a)))$.\label{item:modal3}
\item For any $z,z':\modal(A)$, the function $\mreturn^\modal_{z=z'} : (z=z') \to \modal(z=z')$ is an equivalence.\label{item:modal4}
\end{enumerate}
We say that $A$ is \define{modal}
\indexdef{modal!type}%
\indexdef{type!modal}%
for $\modal$ if $\mreturn^\modal_A:A\to\modal(A)$ is an equivalence, and we write
\begin{equation}
  \modaltype\defeq\setof{X:\type | X \text{ is $\modal$-modal} }\label{eq:modaltype}
\end{equation}
for the type of modal types.
\end{defn}

Conditions~\ref{item:modal2} and~\ref{item:modal3} are very similar to \cref{thm:modal-char}\ref{item:mchr2}, but phrased using $\modal B(z)$ rather than assuming $B$ to be valued in $\P$.
This allows us to state the condition purely in terms of the operation $\modal$, rather than requiring the predicate $P:\type\to\prop$ to be given in advance.
(It is not entirely satisfactory, since we still have to refer to $P$ not-so-subtly in clause~\ref{item:modal4}.
We do not know whether~\ref{item:modal4} follows from~\ref{item:modal1}--\ref{item:modal3}.)
However, the stronger-looking property of \cref{thm:modal-char}\ref{item:mchr2} follows from \cref{defn:modality}\ref{item:modal2} and~\ref{item:modal3}, since for any $C:\modal A \to \modaltype$ we have $C(z) \eqvsym \modal C(z)$, and we can pass back across this equivalence.

\index{universal!property!of a modality}%
As with other induction principles, this implies a universal property.

\begin{thm}\label{prop:lv_n_deptype_sec_equiv_by_precomp}
Let $A$ be a type and let $B:\modal(A)\to\modaltype$. Then the function
\begin{equation*}
(\blank\circ \mreturn^\modal_A) : \Parens{\prd{z:\modal(A)}B(z)} \to \Parens{\prd{a:A}B(\mreturn^\modal_A(a))}
\end{equation*}
is an equivalence.
\end{thm}
\begin{proof}
By definition, the operation $\ind{\modal}$ is a right inverse to $(\blank\circ \mreturn^\modal_A)$.
Thus, we only need to find a homotopy
\begin{equation*}
\prd{z:\modal(A)}s(z)= \ind{\modal}(s\circ \mreturn^\modal_A)(z)
\end{equation*}
for each $s:\prd{z:\modal(A)}B(z)$, exhibiting it as a left inverse as well.
By assumption, each $B(z)$ is modal, and hence each type $s(z)= R^\modal_X(s\circ \mreturn^\modal_A)(z)$
is also modal.
Thus, it suffices to find a function of type
\begin{equation*}
\prd{a:A}s(\mreturn^\modal_A(a))= \ind{\modal}(s\circ \mreturn^\modal_A)(\mreturn^\modal_A(a)).
\end{equation*}
which follows from \cref{defn:modality}\ref{item:modal3}.
\end{proof}

In particular, for every type $A$ and every modal type $B$, we have an equivalence $(\modal A\to B)\eqvsym (A\to B)$.

\begin{cor}
  For any modality $\modal$, the $\modal$-modal types form a reflective subuniverse satisfying the equivalent conditions of \cref{thm:modal-char}.
\end{cor}

Thus, modalities can be identified with reflective subuniverses closed under $\Sigma$-types.
The name \emph{modality} comes, of course, from \emph{modal logic}\index{modal!logic}, which studies logic where we can form statements such as ``possibly $A$'' (usually written $\diamond A$) or ``necessarily $A$'' (usually written $\Box A$).
The symbol $\modal$ is somewhat common for an arbitrary modal operator\index{modal!operator}. % (rather than a specific one such as $\diamond$ or $\Box$).
Under the propositions-as-types principle, a modality in the sense of modal logic corresponds to an operation on \emph{types}, and \cref{defn:modality} seems a reasonable candidate for how such an operation should be defined.
(More precisely, we should perhaps call these \emph{idempotent, monadic} modalities; see the Notes.)
\index{idempotent!modality}%
As mentioned in \cref{subsec:when-trunc}, we may in general use adverbs\index{adverb} to speak informally about such modalities, such as ``merely''\index{merely} for the propositional truncation and ``purely''\index{purely} for the identity modality
\index{identity!modality}%
\index{modality!identity}%
(i.e.\ the one defined by $\modal A \defeq A$).

For any modality $\modal$, we define a map $f:A\to B$ to be \define{$\modal$-connected}
\indexdef{function!.circle-connected@$\modal$-connected}%
\indexdef{.circle-connected function@$\modal$-connected function}%
if $\modal(\hfib f b)$ is contractible for all $b:B$, and to be \define{$\modal$-truncated}
\indexdef{function!.circle-truncated@$\modal$-truncated}%
\indexdef{.circle-truncated function@$\modal$-truncated function}%
if $\hfib f b$ is modal for all $b:B$.
All of the theory of \cref{sec:connectivity,sec:image-factorization} which doesn't involve relating $n$-types for different values of $n$ applies verbatim in this generality.
\index{orthogonal factorization system}%
\index{unique!factorization system}%
In particular, we have an orthogonal factorization system.

An important class of modalities which does \emph{not} include the $n$-trun\-ca\-tions is the \emph{left exact} modalities: those for which the functor $\modal$ preserves pullbacks as well as finite products.
\index{topology!Lawvere-Tierney}%
These are a categorification of ``Lawvere-Tierney\index{Lawvere}\index{Tierney} topologies'' in elementary topos\index{topos} theory,
and correspond in higher-categorical semantics to sub-$(\infty,1)$-toposes.
\index{.infinity1-topos@$(\infty,1)$-topos}%
However, this is beyond the scope of this book.

Some particular examples of modalities other than $n$-truncation can be found in the exercises.

\index{modality|)}

\sectionNotes

The notion of homotopy $n$-type in classical homotopy theory is quite old.
It was Voevodsky who realized that the notion can be defined recursively in homotopy type theory, starting from contractibility.

\index{axiom!Streicher's Axiom K}%
The property ``Axiom K'' was so named by Thomas Streicher, as a property of identity types which comes after J, the latter being the traditional name for the eliminator of identity types.
\cref{thm:hedberg} is due to Hedberg~\cite{hedberg1998coherence}; \cite{krausgeneralizations} contains more information and generalizations.

The notions of $n$-connected spaces and functions are also classical in homotopy theory, although as mentioned before, our indexing for connectedness of functions is off by one from the classical indexing.
The importance of the resulting factorization system has been emphasized by recent work in higher topos theory by Rezk, Lurie, and others.%
\index{.infinity1-topos@$(\infty,1)$-topos}
In particular, the results of this chapter should be compared with~\cite[\S6.5.1]{lurie:higher-topoi}.
In \cref{sec:freudenthal}, the theory of $n$-connected maps will be crucial to our proof of the Freudenthal suspension theorem.

Modal operators\index{modal!operator} in \emph{simple} type theory have been studied extensively; see e.g.~\cite{modalTT}.  In the setting of dependent type theory, \cite{ab:bracket-types} treats the special case of propositional truncation ($(-1)$-truncation) as a modal operator\index{modal!operator}.  The development presented here greatly extends and generalizes this work, while drawing also on ideas from topos theory.\index{topos}

Generally, modal operators\index{modal!operator} come in (at least) two flavors: those such as $\diamond$ (``possibly'') for which $A\Rightarrow \diamond A$, and those such as $\Box$ (``necessarily'') for which $\Box A \Rightarrow A$.
When they are also \emph{idempotent} (i.e.\ $\diamond A = \diamond{\diamond A}$ or $\Box A = \Box{\Box A}$), the former may be identified with reflective subcategories (or equivalently, idempotent monads), and the latter with coreflective subcategories (or idempotent comonads).
\index{monad}
\index{comonad}
However, in dependent type theory it is trickier to deal with the comonadic sort, since they are more rarely stable under pullback, and thus cannot be interpreted as operations on the universe \UU.
Sometimes there are ways around this (see e.g.~\cite{QGFTinCHoTT12}), but for simplicity, here we stick to the monadic sort.

On the computational side, monads (and hence modalities\index{modality}) are used to model computational effects in functional programming~\cite{Moggi89}.%
\index{programming}%
\index{computational effect}%
A computation is said to be \emph{pure} if its execution results in no side effects (such as printing a message to the screen, playing music, or sending data over the Internet).
There exist ``purely functional'' programming languages, such as Haskell\index{Haskell}, in which it is technically only possible to write pure functions: side effects are represented by applying ``monads'' to output types.
For instance, a function of type $\mathsf{Int}\to\mathsf{Int}$ is pure, while a function of type $\mathsf{Int}\to \mathsf{IO}(\mathsf{Int})$ may perform input and output along the way to computing its result; the operation $\mathsf{IO}$ is a monad.
\index{purely}%
(This is the origin of our use of the adverb ``purely'' for the identity monad, since it corresponds computationally to pure functions with no side-effects.)
The modalities we have considered in this chapter are all idempotent, whereas those used in functional programming rarely are, but the ideas are still closely related.


\sectionExercises

\begin{ex}\label{ex:all-types-sets}\
  \begin{enumerate}
    \item Use \cref{thm:h-set-refrel-in-paths-sets} to show
    that if $\brck{A}\to A$ for every type $A$,
    then every type is a set.
    \item Show that if every surjective function (purely) splits,
    i.e.~if
    %
    \narrowequation{\prd{b:B}\brck{\hfib{f}{b}}\to\prd{b:B}\hfib{f}{b}}
    %
    for every $f:A\to B$, then every type is a set.
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:s2-colim-unit}
  For this exercise, we consider the following general notion of colimit.
  Define a \define{graph}\indexdef{graph} $\Gamma$ to consist of a type $\Gamma_0$ and a family $\Gamma_1 : \Gamma_0 \to \Gamma_0 \to \UU$.
  A \define{diagram}\index{diagram} (of types) over a graph $\Gamma$ consists of a family $F:\Gamma_0 \to \UU$ together with for each $x,y:\Gamma_0$, a function $F_{x,y}:\Gamma_1(x,y) \to F(x) \to F(y)$.
  The \define{colimit}\index{colimit!of types} of such a diagram is the higher inductive type $\colim(F)$ generated by
  \begin{itemize}
  \item for each $x:\Gamma_0$, a function $\inc_x:F(x) \to \colim(F)$, and
  \item for each $x,y:\Gamma_0$ and $\gamma:\Gamma_1(x,y)$ and $a:F(x)$, a path $\inc_y(F_{x,y}(\gamma,a)) = \inc_x(a)$.
  \end{itemize}
  There are more general kinds of colimits as well (see e.g.\ \cref{ex:s2-colim-unit-2}), but this is good enough for many purposes.
  \begin{enumerate}
  \item Exhibit a graph $\Gamma$ such that colimits of $\Gamma$-diagrams can be identified with pushouts as defined in \cref{sec:colimits}.
    In other words, each span should induce a diagram over $\Gamma$ whose colimit is the pushout of the span.
  \item Exhibit a graph $\Gamma$ and a diagram $F$ over $\Gamma$ such that $F(x)=\unit$ for all $x$, but such that $\colim(F)=\Sn^2$.
    Note that $\unit$ is a $(-2)$-type, while $\Sn^2$ is not expected to be an $n$-type for any finite $n$.
    See also \cref{ex:s2-colim-unit-2}.
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:ntypes-closed-under-wtypes}
  Show that if $A$ is an $n$-type and $B:A\to \ntype{n}$ is a family of $n$-types, where $n\ge -1$, then the $W$-type $\wtype{a:A} B(a)$ (see \cref{sec:w-types}) is also an $n$-type.
\end{ex}

\begin{ex}\label{ex:connected-pointed-all-section-retraction}
  Use \cref{prop:nconn_fiber_to_total} to extend \cref{thm:connected-pointed} to any section-retraction pair.
\end{ex}

\begin{ex}\label{ex:ntype-from-nconn-const}
  Show that \cref{thm:nconn-to-ntype-const} also works as a characterization in the other direction: $B$ is an $n$-type if and only if every map into $B$ from an $n$-con\-nect\-ed type is constant.
  Ideally, your proof should work for any modality as in \cref{sec:modalities}.
\end{ex}

\begin{ex}\label{ex:connectivity-inductively}
  Prove that for $n\ge -1$, a type $A$ is $n$-connected if and only if it is merely inhabited and for all $a,b:A$ the type $\id[A]ab$ is $(n-1)$-connected.
  Thus, since every type is $(-2)$-connected, $n$-connectedness of types can be defined inductively using only propositional truncations.
\end{ex}

\begin{ex}\label{ex:lemnm}
  \indexdef{excluded middle!LEMnm@$\LEM{n,m}$}%
  For $-1\le n,m \le\infty$, let $\LEM{n,m}$ denote the statement
  \[ \prd{A:\ntype{n}} \trunc m{A + \neg A},\]
  where $\ntype{\infty} \defeq \type$ and $\trunc{\infty}{X}\defeq X$.
  Show that:
  \begin{enumerate}
  \item If $n=-1$ or $m=-1$, then $\LEM{n,m}$ is equivalent to $\LEM{}$ from \cref{sec:intuitionism}.
  \item If $n\ge 0$ and $m\ge 0$, then $\LEM{n,m}$ is inconsistent with univalence.
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:acnm}
  \indexdef{axiom!of choice!ACnm@$\choice{n,m}$}%
  For $-1\le n,m\le\infty$, let $\choice{n,m}$ denote the statement
  \[ \prd{X:\set}{Y:X\to\ntype{n}}
  \Parens{\prd{x:X} \trunc m{Y(x)}}
  \to
  \Trunc m{\prd{x:X} Y(x)},
  \]
  with conventions as in \cref{ex:lemnm}.
  Thus $\choice{0,-1}$ is the axiom of choice from \cref{sec:axiom-choice}, while $\choice{\infty,\infty}$ is \cref{thm:ttac}.
  It is known that $\choice{\infty,-1}$ is consistent with univalence, since it holds in Voevodsky's simplicial model.
  \begin{enumerate}
  \item Without using univalence, show that $\LEM{n,\infty}$ implies $\choice{n,m}$ for all $m$.
    (On the other hand, in \cref{subsec:emacinsets} we will show that $\choice{}=\choice{0,-1}$ implies $\LEM{}=\LEM{-1,-1}$.)
  \item Of course, $\choice{n,m}\Rightarrow \choice{k,m}$ if $k\le n$.
    Are there any other implications between the principles $\choice{n,m}$?
    Is $\choice{n,m}$ consistent with univalence for any $m\ge 0$ and any $n$?
    (These are open questions.)\index{open!problem}
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:acnm-surjset}
  Show that $\choice{n,-1}$ implies that for any $n$-type $A$, there merely exists a set $B$ and a surjection $B\to A$.
\end{ex}

\begin{ex}\label{ex:acconn}
  Define the \define{$n$-connected axiom of choice}
  \indexdef{n-connected@$n$-connected!axiom of choice}%
  \indexdef{axiom!of choice!n-connected@$n$-connected}%
  to be the statement
  \begin{quote}
    If $X$ is a set and $Y:X\to \type$ is a family of types such that each $Y(x)$ is $n$-connected, then $\prd{x:X} Y(x)$ is $n$-connected.
  \end{quote}
  Note that the $(-1)$-connected axiom of choice is $\choice{\infty,-1}$ from \cref{ex:acnm}.
  \begin{enumerate}
  \item Prove that the $(-1)$-connected axiom of choice implies the $n$-con\-nect\-ed axiom of choice for all $n\ge -1$.
  \item Are there any other implications between the $n$-connected axioms of choice and the principles $\choice{n,m}$?
    (This is an open question.)\index{open!problem}
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:n-truncation-not-left-exact}
  Show that the $n$-truncation modality is not left exact for any $n\ge -1$.
  That is, exhibit a pullback which it fails to preserve.
\end{ex}

\begin{ex}\label{ex:double-negation-modality}
  Show that $X\mapsto (\neg\neg X)$ is a modality.\index{modal!operator}%
\end{ex}

\begin{ex}\label{ex:prop-modalities}
  Let $P$ be a mere proposition.
  \begin{enumerate}
  \item Show that $X\mapsto (P\to X)$ is a left exact modality.
    This is called the \define{open modality}
    \indexdef{open!modality}%
    \indexdef{modality!open}%
    associated to $P$.
  \item Show that $X\mapsto P*X$ is a left exact modality, where $*$ denotes the join (see \cref{sec:colimits}).
    This is called the \define{closed modality}
    \indexdef{closed!modality}%
    \indexdef{modality!closed}%
    associated to $P$.
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:f-local-type}
  Let $f:A\to B$ be a map; a type $Z$ is \define{$f$-local}
  \indexdef{f-local type@$f$-local type}%
  \indexdef{type!f-local@$f$-local}%
  if $(\blank\circ f):(B\to Z) \to (A\to Z)$ is an equivalence.
  \begin{enumerate}
  \item Prove that the $f$-local types form a reflective subuniverse.
    You will want to use a higher inductive type to define the reflector (localization).
  \item Prove that if $B=\unit$, then this subuniverse is a modality.
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:trunc-spokes-no-hub}
  Show that in contrast to \cref{rmk:spokes-no-hub}, we could equivalently define $\trunc nA$ to be generated by a function $\tprojf n : A \to \trunc n A$ together with for each $r:\Sn^{n+1} \to \trunc n A$ and each $x:\Sn^{n+1}$, a path $s_r(x):r(x) = r(\base)$.
\end{ex}

\begin{ex}\label{ex:s2-colim-unit-2}
  In this exercise, we consider a slightly fancier notion of colimit than in \cref{ex:s2-colim-unit}.
  Define a \define{graph with composition}\indexdef{graph!with composition} $\Gamma$ to be a graph as in \cref{ex:s2-colim-unit} together with for each $x,y,z:\Gamma_0$, a function $\Gamma_1(y,z) \to \Gamma_1(x,y) \to \Gamma_1(x,z)$, written as $\delta\mapsto\gamma \mapsto \delta \circ \gamma$.
  (For instance, any precategory as in \cref{cha:category-theory} is a graph with composition.)
  A \define{diagram}\index{diagram} $F$ over a graph with composition $\Gamma$ consists of a diagram over the underlying graph, together with for each $x,y,z:\Gamma_0$ and $\gamma:\Gamma_1(x,y)$ and $\delta:\Gamma_1(y,z)$, a homotopy $\cmp_{x,y,z}(\delta,\gamma) : F_{y,z}(\delta) \circ F_{x,y}(\gamma) \htpy F_{x,z}(\delta\circ\gamma)$.
  The \define{colimit}\index{colimit!of types} of such a diagram is the higher inductive type $\colim(F)$ generated by
  \begin{itemize}
  \item for each $x:\Gamma_0$, a function $\inc_x:F(x) \to \colim(F)$,
  \item for each $x,y:\Gamma_0$ and $\gamma:\Gamma_1(x,y)$ and $a:F(x)$, a path $\glue_{x,y}(\gamma,a) : \inc_y(F_{x,y}(\gamma,a)) = \inc_x(a)$, and
  \item for each $x,y,z:\Gamma_0$ and $\gamma:\Gamma_1(x,y)$ and $\delta:\Gamma_1(y,z)$ and $a:F(x)$, a path
    \[ \ap{\inc_z}{\cmp_{x,y,z}(\delta,\gamma,a)} \ct \glue_{x,z}(\delta\circ \gamma,a) = \glue_{y,z}(\delta,F_{x,y}(\gamma,a)) \ct \glue_{x,y}(\gamma,a). \]
  \end{itemize}
  (This is a ``second-order approximation'' to a fully homotopy-theoretic notions of diagram and colimit, which ought to involve ``coherence paths'' of this sort at all higher levels.
  Defining such things in type theory is an important open problem.)
  
  Exhibit a graph with composition $\Gamma$ such that $\Gamma_0$ is a set and each type $\Gamma_1(x,y)$ is a mere proposition, and a diagram $F$ over $\Gamma$ such that $F(x)=\unit$ for all $x$, for which $\colim(F)=\Sn^2$.
\end{ex}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "hott-online"
%%% End: