# HoTT/book

### Subversion checkout URL

You can clone with HTTPS or Subversion.

Make the proof that reflectors commute with pushouts a bit more rigorous

 @@ -4,8 +4,6 @@ \newcommand{\typele}[1]{\ensuremath{\type_{\le #1}}\xspace} % Natural numbers \newcommand{\N}{\mathbb{N}} -% Type of truncation levels (integers starting at -2) -\newcommand{\Nt}{\N_{-2}} % Function definition with domain and codomain \newcommand{\function}[4]{\left\{\begin{array}{rcl}#1 & \longrightarrow & #2 \\ #3 & \longmapsto & #4 \end{array}\right.} @@ -36,7 +34,7 @@ \newcommand{\ext}{\mathsf{ext}} % Projection and extension for truncations \newcommand{\tproj}{\mathsf{proj}} -\newcommand{\extendsmb}{\mathsf{extend}} +\newcommand{\extendsmb}{\mathsf{ext}} \newcommand{\extend}[1]{\extendsmb(#1)} % Apply a function to a cocone \newcommand{\composecocone}[2]{#1\circ#2} @@ -60,7 +58,7 @@ \subsection{Definition} Let’s consider \P a subuniverse of \type. More precisely we have a map $P:\type\to\prop$ and we use the notation $A:\P$ to mean that $A:\type$ and $P(A)$ holds. For instance \P could be \prop, \set, or more generally -$\typele{n}$ for any $n\in\Nt$. +$\typele{n}$ for any $n\ge-2$. \begin{defn} A \emph{pushout diagram} in $\P$ is 5-uple $\Ddiag=(A,B,C,f,g)$ with @@ -391,16 +389,21 @@ \section{Homotopy pullbacks} \section{Reflective subuniverses of $\type$} +Reflective subuniverses are particularly nice subuniverses in the sense that +every type $A:\type$ can be reflected down to a type $\reflect(A)$ in the +subuniverse which is (in a precise way) the free type generated by $A$ in the +subuniverse. + \begin{defn} - A subuniverse $\P$ of $\type$ is said to be a \emph{reflective subuniverse} of - $\type$ if for every $A:\type$ we have a type $\reflect(A):\P$ and a map + A subuniverse $\P$ of $\type$ is a \emph{reflective subuniverse of $\type$} if + for every $A:\type$ we have a type $\reflect(A):\P$ and a map $\project_A:A\to\reflect(A)$ satisfying the following universal property: For every $A:\type$ and $B:\P$, the following map is an equivalence $\function{(\reflect(A)\to{}B)}{(A\to{}B)}{f}{f\circ\project_A}$ - In other words, for every $g:A\to{}B$ in the following diagram there is a - unique map $\ext(g):\reflect(A)\to{}B$ making the diagram commute. + In other words, for every $B:\P$ and $g:A\to{}B$ there is a unique map + $\ext(g):\reflect(A)\to{}B$ making the following diagram commute. $\uppercurveobject{{ }}\lowercurveobject{{ }}\twocellhead{{ }} \xymatrix{A \ar^{\project_A}[r] \ar_g[rd] \druppertwocell{=} & \reflect(A) @@ -408,50 +411,50 @@ \section{Reflective subuniverses of \type} & B}$ \end{defn} -% If $\P$ is a reflective subuniverse of $\type$, then we can construct pushouts -% in $\P$ by reflecting the corresponding pushout in $\type$. - -The reflector $\reflect$ is a map $\type\to\P$ and using the universal property -we should be able to prove that $\reflect$ is $(\infty,1)$-functorial. But as -before we don’t know how to express this property, so we will only express a few -bits of it. +The universal property means that $\reflect$ is left adjoint to the inclusion +$\iota:\P\to\type$ with $\project_A$ as the unit, because the last $B$ in the +universal property can be replaced by $\iota(B)$ given that $B$ is in $\P$. -\begin{defn} - If $f:A\to{}B$, there is a map $\reflect(f):\reflect(A)\to\reflect(B)$ and - this operation satisfy the following functoriality conditions: - \begin{align*} - \reflect(\idfunc[A])=\idfunc[\reflect(A)]\\ - \reflect(f\circ{}g)=\reflect(f)\circ\reflect(g) - \end{align*} -\end{defn} +\begin{lem} + Let \P be a subuniverse of \type. The fact that \P is reflective is \anhprop. +\end{lem} \begin{proof} - The map $\reflect(f)$ is defined to be the unique map - $\reflect(A)\to\reflect(B)$ such that - $\reflect(f)\circ\project_A=\project_B\circ{}f$ (using the universal property - of $\reflect$), or in other words $\reflect(f)=\ext(\project_B\circ{}f)$. + Let’s assume that \P is reflective in two different ways + $(\reflect,\project,\ext)$ and $(\reflect',\project',\ext')$. We need to + construct an equivalence between $\reflect(A)$ and $\reflect'(A)$ for every + $A:\type$ and we need to prove that the following diagram commutes: $\uppercurveobject{{ }}\lowercurveobject{{ }}\twocellhead{{ }} - \xymatrix{A \ar^-{\project_A}[r] \ar_-f[d] \drtwocell{=} & \reflect(A) - \ar@{-->}^-{\reflect(f)}[d] - \\ B \ar_-{\project_B}[r] & \reflect(B)}$ - In order to prove that $\reflect(\idfunc[A])=\idfunc[\reflect(A)]$, we only - need to prove that - $\reflect(\idfunc[A])\circ\project_A=\idfunc[\reflect(A)]\circ\project_A$. But - both sides are equal to $\project_A$. - - Similarly, to prove that $\reflect(f\circ{}g)=\reflect(f)\circ\reflect(g)$ we - only need to prove that $\reflect(f\circ{}g)\circ\project_A= - \reflect(f)\circ\reflect(g)\circ\project_A$ and both sides are equal to - $\project_C\circ{}f\circ{}g$. + \xymatrix{A \ar^{\project_A}[r] \ar_{\project'_A}[rd] \druppertwocell{=} & + \reflect(A) \ar@{->}^\sim[d] \\ + & \reflect'(A)}\] + + The type $\reflect'(A)$ is in \P, so we can define the map + $\ext(\project'_A):\reflect(A)\to\reflect'(A)$ + which is exactly the map making the previous diagram commute. + + We can also define + $\ext'(\project_A):\reflect'(A)\to\reflect(A)$ + + In order to prove that the composite is the identity, we only need to prove + that $\ext'(\project_A)\circ\ext(\project'_A)\circ\project_A=\project_A$ + which is the case: + $\uppercurveobject{{ }}\lowercurveobject{{ }}\twocellhead{{ }} + \xymatrix{A \ar^{\project_A}[r] \ar_{\project'_A}[rd] + \ar@/_5mm/_{\project_A}[rdd] & + \reflect(A) \ar@{->}^{\ext(\project'_A)}[d] \\ + & \reflect'(A) \ar@{->}^{\ext'(\project_A)}[d] \\ + & \reflect(A)}$ \end{proof} +For the rest of this section, we assume that $\P$ is a reflective subuniverse of +$\type$. + +The following lemma says that the counit of the adjunction is an equivalence. \begin{lem} \label{reflectPequiv} If $A:\P$, then the map $\project_A:A\to\reflect(A)$ is an equivalence. - - Moreover, if $f:A\to{}B$ with $B:\P$, then - $\project_B^{-1}\circ\reflect(f)\circ\project_A = f$. \end{lem} \begin{proof} Given that $A$ is in $\P$, we can define $\ext(\idfunc[A]):\reflect(A)\to{}A$. @@ -460,27 +463,118 @@ \section{Reflective subuniverses of $\type$} definition, and in order to prove that $\project_A\circ\ext(\idfunc[A])=\idfunc[\reflect(A)]$ we only need to prove that $\project_A\circ\ext(\idfunc[A])\circ\project_A= - \idfunc[\reflect(A)]\circ\project_A$ which is true. + \idfunc[\reflect(A)]\circ\project_A$which is again true. - For the second point is just a consequence of the fact that -$\reflect(f)\circ\project_A=\project_B\circ{}f$. + $\xymatrix{ + A \ar^{\project_A}[r] \ar_{\idfunc[A]}[rd] & + \reflect(A) \ar^>>>{\ext(\idfunc[A])}[d] \ar@/^40pt/^{\idfunc[\reflect(A)]}[dd] \\ + & A \ar_{\project_A}[d] \\ + & \reflect(A)}$ \end{proof} -\begin{lem} - For every$A,B,C:\type$,$f:A\to{}B$and$i:B\to{}C$we have +The reflector$\reflect$is a map$\type\to\P$and using the universal property +we should be able to prove that$\reflect$is$(\infty,1)$-functorial. But we +don’t know how to express$(\infty,1)$-functoriality so we will only prove a +few bits of it. + +\begin{defn} + If$f:A\to{}B$, there is a map$\reflect(f):\reflect(A)\to\reflect(B)$defined + by + $\reflect(f)\circ\project_A=\project_B\circ{}f$ + (or in other words$\reflect(f)=\ext(\project_B\circ{}f)). + + $\uppercurveobject{{ }}\lowercurveobject{{ }}\twocellhead{{ }} + \xymatrix{A \ar^-{\project_A}[r] \ar_-f[d] \drtwocell{=} & \reflect(A) + \ar@{-->}^-{\reflect(f)}[d] + \\ B \ar_-{\project_B}[r] & \reflect(B)}$ + + This operation satisfies the following functoriality conditions: + \begin{align*} + \reflect(\idfunc[A])=\idfunc[\reflect(A)]\\ + \reflect(f\circ{}g)=\reflect(f)\circ\reflect(g) + \end{align*} + + In order to define these equalities, we only need to define them after + composition by\project(A)$because of the universal property. + + The first one is defined by + + $\xymatrix{ + \reflect(\idfunc[A])\circ\project_A \ar@{==}[r] \ar@{=}[d] & + \idfunc[\reflect(A)]\circ\project_A \ar@{=}[d] \\ + \project_A \ar@{=}[r] & \project_A + }$ + + The second one is defined by + + $\xymatrix{ + \reflect(f\circ g)\circ\project_A \ar@{==}[r] \ar@{=}[d] & + \reflect(f)\circ\reflect(g)\circ\project_A \ar@{=}[d] \\ + \project_C\circ f\circ g \ar@{=}[r] & \reflect(f)\circ\project_B\circ g + }$ +\end{defn} + +% \begin{proof} +% The map$\reflect(f)$is defined to be the unique map +%$\reflect(A)\to\reflect(B)$such that +%$\reflect(f)\circ\project_A=\project_B\circ{}f$(using the universal property +% of$\reflect$), or in other words$\reflect(f)=\ext(\project_B\circ{}f)$. + +% $\uppercurveobject{{ }}\lowercurveobject{{ }}\twocellhead{{ }} +% \xymatrix{A \ar^-{\project_A}[r] \ar_-f[d] \drtwocell{=} & \reflect(A) +% \ar@{-->}^-{\reflect(f)}[d] +% \\ B \ar_-{\project_B}[r] & \reflect(B)}$ +% In order to prove that$\reflect(\idfunc[A])=\idfunc[\reflect(A)]$, we only +% need to prove that +%$\reflect(\idfunc[A])\circ\project_A=\idfunc[\reflect(A)]\circ\project_A$. But +% both sides are equal to$\project_A$. + +% Similarly, to prove that$\reflect(f\circ{}g)=\reflect(f)\circ\reflect(g)$we +% only need to prove that$\reflect(f\circ{}g)\circ\project_A= +% \reflect(f)\circ\reflect(g)\circ\project_A$and both sides are equal to +%$\project_C\circ{}f\circ{}g$. + +% Note that by definition, the following diagram commutes: + +% $\xymatrix{ +% \reflect(f\circ g)\circ\project_A \ar@{=}[r] \ar@{=}[d] & +% \reflect(f)\circ\reflect(g)\circ\project_A \ar@{=}[d] \\ +% \project_C\circ f\circ g \ar@{=}[r] & \reflect(f)\circ\project_B\circ g +% }$ +% \end{proof} + +\begin{defn} + For every$A,B:\type$,$C:\P$,$f:A\to{}B$and$i:B\to{}C$we have $\ext(i\circ{}f)=\ext(i)\circ\reflect(f)$ -\end{lem} -\begin{proof} - $\xymatrix{A \ar^{\project_A}[r] \ar_f[d] & \reflect(A) \ar^{\reflect(f)}[d] - \\ - B \ar^{\project_B}[r] \ar_i[d] & \reflect(B) \ar^{\ext(i)}[ld] \\ - C &}$ + $\xymatrix{ + A \ar^{\project_A}[r] \ar_f[d] & \reflect(A) \ar^{\reflect(f)}[d] + \ar@/^15mm/^{\ext(i\circ f)}[dd] \\ + B \ar^{\project_B}[r] \ar_i[rd] & \reflect(B) \ar^{\ext(i)}[d] \\ + & C}$ + + This equality is defined by + $\xymatrix{ + \ext(i\circ f)\circ\project_A \ar@{==}[r] \ar@{=}[d] & + \ext(i)\circ\reflect(f)\circ\project_A \ar@{=}[d] \\ + i\circ f \ar@{=}[r] & \ext(i)\circ\project_B\circ f + }$ - We only have to prove that - $\ext(i\circ{}f)\circ\project_A=\ext(i)\circ\reflect(f)\circ\project_A$ - which is the case because they are both equal to$i\circ{}f$. -\end{proof} +\end{defn} + +% \begin{proof} +% $\xymatrix{A \ar^{\project_A}[r] \ar_f[d] & \reflect(A) \ar^{\reflect(f)}[d] +% \\ +% B \ar^{\project_B}[r] \ar_i[d] & \reflect(B) \ar^{\ext(i)}[ld] \\ +% C &}$ + +% We only have to prove that +% $\ext(i\circ{}f)\circ\project_A=\ext(i)\circ\reflect(f)\circ\project_A$ +% which is the case because they are both equal to$i\circ{}f$. +% \end{proof} + +We now want to prove that pushouts in \P are related to pushouts in \type. We +first need to explain how to reflect pushout diagrams and cocones. \begin{defn} Let @@ -489,9 +583,11 @@ \section{Reflective subuniverses of$\type$} pushout diagram in$\P$: $\reflect(\Ddiag)=\xymatrix{\reflect(C) \ar^{\reflect(g)}[r] \ar_{\reflect(f)}[d] & \reflect(B) \\ \reflect(A) & }$ +\end{defn} - We can also reflect cocones. If$D:\P$and$c=(i,j,h):\cocone{\Ddiag}{D}$we - define +\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 @@ -505,7 +601,7 @@ \section{Reflective subuniverses of$\type$} $\mapfunc{\reflect}(\funext(h)):\reflect(i\circ{}f)=\reflect(j\circ{}g)$ Now we can compose with the fact that$\reflect$commutes with composition and we get the following (the proofs that$\reflect$commutes with composition are - not written in order to keep terms readable, and we will see that they don’t + not written in order to keep terms readable, we will later see that they don’t get in the way): $\mapfunc{\reflect}(\funext(h)): \reflect(i)\circ\reflect(f)=\reflect(j)\circ\reflect(g)$ @@ -538,7 +634,8 @@ \section{Reflective subuniverses of$\type$} proving that it’s a composite of five maps which are already known to be equivalences. - The first map comes from the universal property of$\reflect$, we have + The first map comes from the universal property of$\reflect$and the fact + that$E$is in \P, we have $f_1(t)=t\circ\project_D$ The second map comes from the universal property of$(D,c)$, as a pushout of @@ -562,18 +659,25 @@ \section{Reflective subuniverses of$\type$} The fifth map comes from \autoref{coneispb}, we have $f_5(a,b,q)=(a,b,\happly(q))$ - Putting everything together we get + We now need to prove that the diagram commutes because it’s not enough to + know that$(\reflect(D)\to{}E)$is equivalent to +$\cocone{\reflect(\Ddiag)}{E}$, we need to know that this is the map +$t\mapsto{}t\circ\reflect(c)which is an equivalence. + + We have \begin{align*} f_5(f_4(f_3(f_2(f_1(t))))) &= f_5(f_4(f_3(f_2(t\circ\project_D)))) \\ &= f_5(f_4(f_3(t\circ\project_D\circ{}i,t\circ\project_D\circ{}j, \mapfunc{(t\circ\project_D)}\circ{}h))) \\ &=f_5(f_4(t\circ\project_D\circ{}i,t\circ\project_D\circ{}j, \funext(\mapfunc{(t\circ\project_D)}\circ{}h))) \\ - &=f_5(\ext(t\circ\project_D\circ{}i),\ext(t\circ\project_D\circ{}j), - \mapfunc{\ext}(\funext(\mapfunc{(t\circ\project_D)}\circ{}h))) \\ + &=f_5(\ext(t\circ\project_D\circ{}i),\ext(t\circ\project_D\circ{}j),\\ + &\qquad\qquad\mapfunc{\ext}(\funext(\mapfunc{(t\circ\project_D)}\circ{}h))) + \\ &=f_5(\ext(t\circ\project_D)\circ\reflect(i), - \ext(t\circ\project_D)\circ\reflect(j), - \mapfunc{\ext}(\funext(\mapfunc{(t\circ\project_D)}\circ{}h))) \\ + \ext(t\circ\project_D)\circ\reflect(j),\\ + &\qquad\qquad\mapfunc{\ext}(\funext(\mapfunc{(t\circ\project_D)}\circ{}h))) + \\ &=f_5(t\circ\reflect(i), t\circ\reflect(j), \mapfunc{\ext}(\funext(\mapfunc{(t\circ\project_D)}\circ{}h))) \\ @@ -581,6 +685,19 @@ \section{Reflective subuniverses of\type} \happly(\mapfunc{\ext}(\funext(\mapfunc{(t\circ\project_D)}\circ{}h)))) \end{align*} + Note that in the two steps before the last equality we are using the fact + that ifa=a'$and$b=b'$, then$(a,b,q)=(a',b',q)$. This is actually not + even well typed given that the type of$q$depends on$a$and$b$, so we + have to transport$q$along the proofs$p:a=a'$and$q:b=b'$. In the present + case we have$q:a\circ\reflect(f)=b\circ\reflect(g)hence the correct + statement is + $(a,b,q)=(a',b',q')$ where + $q'\defeq\map{(\lambda{}u.\,u\circ\reflect(f))}{\rev p} \ct q \ct + \map{(\lambda{}u.\,u\circ\reflect(g))}{p'})$ Again we will leave this + implicit and take care of it only when it will be needed. + + \bigskip + In order to prove that the diagram commutes, we now only need to prove that \begin{align*} \happly(\mapfunc{\ext}(\funext(\mapfunc{(t\circ\project_D)}\circ{}h))) &= @@ -611,38 +728,158 @@ \section{Reflective subuniverses of\type$} $\map{\ext}{\map{(\lambda{}u.\,t\circ\project_D\circ{}u)}{\funext(h)}}= \map{(\lambda{}u.\,t\circ{}u)}{\map{\reflect}{\funext(h)}}$ - This is the point where we need to check that the implicit equalities around -$\mapfunc{\ext}$and$\mapfunc{\reflect}$cancel (TODO, this seems true but - awfully complicated) + The idea is now to do an induction on the path$\funext(h):i\circ f = j\circ + g$which should be allowed because nothing in the previous expression seems to + depend on the fact that$\funext(h)$goes from a composition to another + composition. But let’s not forget that there are implicit equalities around + both sides of the equation and they do use the fact that$i\circ f$and +$j\circ g$are compositionss, so we first need to get rid of that. - After that, using functoriality of$f\mapsto\mapfunc{f}$it will be enough to - prove the following: + % After that, using the fact that for every$k:C\to{}Dwe have - $\ext\circ(\lambda{}u.\,t\circ\project_D\circ{}u)= - (\lambda{}u.\,t\circ{}u)\circ\reflect$ + % \begin{align*} + % \ext(t\circ\project_D\circ{}k) &= \ext(t\circ\project_D)\circ\reflect(k) \\ + % &= t\circ\reflect(k) + % \end{align*} - We apply function extensionality, so for everyu:C\to{}D$we have to prove + % We will have - $\ext(t\circ\project_D\circ{}u) = t\circ\reflect(u) : \reflect(C)\to E$ + % $\ext\circ(\lambda{}u.\,t\circ\project_D\circ{}u)= + % (\lambda{}u.\,t\circ{}u)\circ\reflect$ - But we have -$\ext(t\circ\project_D\circ{}u)=\ext(t\circ\project_D)\circ\reflect(u)=t\circ\reflect(u)$- hence the equality holds. + % Hence the result, using the functoriality of$f\mapsto{}f_*$. + + \bigskip + + % Let’s prove that the implicit equalities around$\mapfunc{r}$and + %$\mapfunc{\ext}$cancel. + We have the following diagram: + + $\xymatrix{ + t\circ\reflect(i\circ f) \ar@{=}[r] \ar@{=}[d] & + t\circ\reflect(j\circ g) \ar@{=}[d] \\ + t\circ\reflect(i)\circ\reflect(f) \ar@{=}[d] & + t\circ\reflect(j)\circ\reflect(g) \ar@{=}[d] \\ + \extend{t\circ\project_D}\circ\reflect(i)\circ\reflect(f) \ar@{=}[d] & + \extend{t\circ\project_D}\circ\reflect(j)\circ\reflect(g) \ar@{=}[d] \\ + \extend{t\circ\project_D\circ i}\circ\reflect(f) \ar@{=}[d] & + \extend{t\circ\project_D\circ j}\circ\reflect(g) \ar@{=}[d] \\ + \extend{t\circ\project_D\circ i\circ f} \ar@{=}[r] & + \extend{t\circ\project_D\circ j\circ g}\\ + }$ + + \begin{itemize} + \item The top horizontal equality is +$\map{(\lambda{}u.\,t\circ{}u)}{\map{\reflect}{\funext(h)}}$without the + implicit equalities around + \item The first line of vertical equalities are the implicit equalities around + the term$\map{(\lambda{}u.\,t\circ{}u)}{\map{\reflect}{\funext(h)}}$(the + right hand side of the equality we want to prove) + \item The next two lines of vertical equalities are around the left hand side + of the equality we want to prove and come from the long computation a few + pages ago + \item The last line of vertical equalities are the implicit equalities around +$\mapfunc{\extendsmb}$+ \item The bottom horizontal equality is +$\map{\ext}{\map{(\lambda{}u.\,t\circ\project_D\circ{}u)}{\funext(h)}}$+ without the implicit equalities around + \end{itemize} + + The commutation of the diagram is exactly the equality we want to prove and + the fact that the compositions$i\circ f$and$j\circ g$are being split in + the middle of the diagram is the reason why we cannot directly induct on +$\funext(h)$. + + So we will prove that the following diagram (where the vertical part is the + right hand side of the previous diagram) commutes. Note that in the right hand + side of this diagram, we do not use anymore the fact that$j\circ g$is a + composition of two functions, so induction on it will be allowed. + + $\xymatrix{ + t\circ\reflect(j\circ g) \ar@{=}[d] & \\ + t\circ\reflect(j)\circ\reflect(g) \ar@{=}[d] & \\ + \extend{t\circ\project_D}\circ\reflect(j)\circ\reflect(g) \ar@{=}[d] & + \extend{t\circ\project_D}\circ\reflect(j\circ g) \ar@{=}[l] \ar@{=}[luu] + \ar@{=}[ldd] \\ + \extend{t\circ\project_D\circ j}\circ\reflect(g) \ar@{=}[d] & \\ + \extend{t\circ\project_D\circ j\circ g} & \\ + }$ + + The top square commutes because it’s the concatenation of the two equalities +$t=\extend{t\circ\project_D}$and$\reflect(j)\circ\reflect(g)=\reflect(j\circ + g)$in two different orders (interchange law). In order to prove that the + bottom square commute, we only have to prove that it commutes after + composition with$\project_C$to the right. Let’s write$u=t\circ\project_D$+ and let’s consider the following diagram. + + $\xymatrix@C=-30pt{ + \extend{u}\circ\reflect(j)\circ\reflect(g)\circ\project_C + \ar@{=}[rrrr] \ar@{=}[ddd] \ar@{=}[rd] & & & & + \extend{u}\circ\reflect(j\circ g)\circ\project_C + \ar@{=}[ld] \ar@{=}[ddd] \\ & + \extend{u}\circ\reflect(j)\circ\project_B\circ g + \ar@{=}[rr] \ar@{=}[d] & {\phantom{thisisanuglyhack}} & + \extend{u}\circ\project_D\circ j\circ g + \ar@{=}[d] & \\ & + \extend{u\circ j}\circ\project_B\circ g + \ar@{=}[rr] \ar@{=}[ld] & & + u\circ j\circ g + \ar@{=}[rd] & \\ + \extend{u\circ j}\circ\reflect(g)\circ\project_C + \ar@{=}[rrrr] & & & & + \extend{u\circ j\circ g}\circ\project_C + }$ + + We need to prove that the exterior square commutes. + + \begin{itemize} + \item The left square commutes because of the interchange law + \item The top square commutes because of the definition of the equality +$\reflect(j\circ g)=\reflect(j)\circ\reflect(g)$+ \item The bottom, right and interior squares commute because of the definition + of the equality$\extend{a}\circ\reflect(b)=\extend{a\circ b}$+ \end{itemize} + + This proves that the exterior square commutes, hence the previous triangular + diagram commutes. We can do the same for the left part of the first + rectangular diagram so we now only have to prove that the following diagram + commutes: + + $\xymatrix{ + t\circ\reflect(i\circ f) \ar@{=}[r] \ar@{=}[d] & + t\circ\reflect(j\circ g) \ar@{=}[d] \\ + \extend{t\circ\project_D}\circ\reflect(i\circ f) \ar@{=}[d] & + \extend{t\circ\project_D}\circ\reflect(j\circ g) \ar@{=}[d] \\ + \extend{t\circ\project_D\circ i\circ f} \ar@{=}[r] & + \extend{t\circ\project_D\circ j\circ g}\\ + }$ + + And now we are finally allowed to induct on$\funext(h)$because the diagram + is not relying anymore on the fact that$i\circ f$and$j\circ g$are + compositions. + + \bigskip This proves that the diagram commutes, hence the map$t\mapsto{}\composecocone{t}\reflect(c)$is an equivalence which proves that the reflector commutes with pushouts. \end{proof} +This proof was rather tedious, but we can hope that at some point we will +understand better what$(\infty,1)$-functorial means in homotopy type theory and +that we will be able to rigorously omit the equalities I left implicit and just +say that every coherence condition is always satisfied. + \begin{cor} Every pushout diagram$\Ddiag$in$\P$has a pushout in$\P$. \end{cor} \begin{proof} - According to \autoref{reflectPequiv}, the diagram$\reflect(\Ddiag)$is - equivalent to$\Ddiag$. But we just proved that$\reflect(\Ddiag)$has a - pushout, namely the reflection of the pushout in \type of$\Ddiag$, hence -$\Ddiag$has a pushout in \P. + According to \autoref{reflectPequiv} and to the diagram defining the action of +$\reflect$on functions, the diagram$\reflect(\Ddiag)$is equivalent to +$\Ddiag$. But we just proved that$\reflect(\Ddiag)$has a pushout, namely the + reflection of the pushout in \type of$\Ddiag$, hence$\Ddiag$has a pushout + in \P. \end{proof} \section{Truncations} @@ -747,7 +984,7 @@ \section{Connectedness of suspensions} connectedness. \begin{thm} - Let$n:\Nt$and$A:\type$. + Let$n\ge-2$and$A:\type$. If$A$is$n$-connected then the suspension of$A$is$(n+1)\$-connected. \end{thm}