that is it for today. I have to pick from 6.4.4 and finish the 'nested' diagram of tau

2cat.tex

@@ -262,9 +262,9 @@ From the previous proposition, we deduce the following very useful corollary.
        \displaystyle\coprod_{x \in E}F_x \ar[r] \ar[d] & E \ar[d]&\\
        A \ar[d,"\alpha"] \ar[r] & G \ar[d] \ar[r] & B \ar[d,"\delta"]\\
        C \ar[r] & H \ar[r] & D 
-       \ar[from=1-1,to=2-2,phantom,"\ulcorner" very near end,"\textcircled{\tiny \textbf{1}}" near start, description]
-       \ar[from=2-1,to=3-2,phantom,"\ulcorner" very near end,"\textcircled{\tiny \textbf{2}}", description]
-                  \ar[from=2-2,to=3-3,phantom,"\ulcorner" very near end,"\textcircled{\tiny \textbf{3}}", description]
+       \ar[from=1-1,to=2-2,phantom,"\ulcorner" very near end,"\text{\textcircled{\tiny \textbf{1}}}" near start, description]
+       \ar[from=2-1,to=3-2,phantom,"\ulcorner" very near end,"\text{\textcircled{\tiny \textbf{2}}}", description]
+                  \ar[from=2-2,to=3-3,phantom,"\ulcorner" very near end,"\text{\textcircled{\tiny \textbf{3}}}", description]
   \end{tikzcd}.
   \]
   What we want to prove is that the image by the functor $L$ of the pasting of squares \textcircled{\tiny \textbf{2}} and \textcircled{\tiny \textbf{3}} is homotopy cocartesian. Since the morphism $G \to B$ is a monomorphism, we deduce from Corollary \ref{cor:hmtpysquaregraph} that the image by the functor $L$ of square \textcircled{\tiny \textbf{3}} is homotopy cocartesian. Hence, all we have to show is that the image by $L$ of square \textcircled{\tiny \textbf{2}} is homotopy cocartesian. \todo{Parler du pasting lemma ?} On the other hand, we know that both morphisms
@@ -689,3 +689,61 @@ It also follows from Lemma \ref{lemma:binervthom} that the bisimplicial nerve in
 This is an immediate consequence of Proposition \ref{prop:streetvsbisimplicial} and Corollary \ref{cor:bisimplicialsquare}.
 \end{proof}
 
+\section{Zoology of $2$-categories : Basic examples}
+
+\begin{paragr}
+  Let $n,m \geq 0$. We denote by $A_{(m,n)}$ the free $2$-category with only one generating $2$-cell whose source is a chain of length $m$ and its target a chain of length $n$:
+  \[
+  \underbrace{\overbrace{\begin{tikzcd}[column sep=small, ampersand replacement=\&] \&\bullet \ar[r,description,"\cdots",phantom,""{name=A,below}] \& \bullet \ar[rd] \& \\ \bullet \ar[ru] \ar[rd] \& \& \&\bullet \\ \&\bullet \ar[r,description,"\cdots",phantom,""{name=B,above}] \& \bullet \ar[ru]\ar[from=A,to=B,shorten <= 2em, shorten >= 2em,Rightarrow]\end{tikzcd}}^{m}}_{n}.\]
+  More formally, $A_{(m,n)}$ is described in the following way:
+  \begin{itemize}[label=-]
+  \item generating $0$-cells: $A_0,\cdots, A_m$, $B_1,\cdots,B_{n-1}$
+  \item generating $1$-cells: $\begin{cases} f_{i+1} : A_i \to A_{i+1} & \text{ for } 0\leq i \leq m-1 \\ g_{j+1} : B_j \to B_{j+1} &\text{ for } 1 \leq j \leq n-2 \\g_1 : A_0 \to B_1 &  \\g_{n} : B_{n-1} \to A_m & 
+  \end{cases}$
+    \item generating $2$-cell: $ \alpha : f_{m}\circ \cdots \circ f_1 \Rightarrow g_n \circ \cdots \circ g_1$.
+  \end{itemize}
+  We are going to prove that if $n\neq 0$ or $m\neq 0$, then $A_{(m,n)}$ is \good{} and has the homotopy type of a point. When $m\neq0$ \emph{and} $n\neq0$, this result is not surprising, but when $n=0$ or $m=0$ (but not both), it is \emph{a priori} less clear what the homotopy type of $A_{(m,n)}$ is and whether it is \good{} or not. For example, $A_{(1,0)}$ can be pictured as follows
+  \[
+  \begin{tikzcd}
+    A \ar[r, bend left=70, "f",""{name=A,below}] \ar[r,bend right=70,"1_A"',""{name=B,above}] & A \ar[from=A,to=B,Rightarrow,"\alpha"]
+    \end{tikzcd},
+  \]
+  and has many non trivial $2$-cells, such as $f\comp_0 \alpha \comp_0 f$.
+
+  Note that when $m=0$ \emph{and} $n=0$, then the $2$-category $A_{(0,0)}$ is nothing but the commutative monoid $\mathbb{N}$ seen as a $2$-category (\ref{paragr:bubble}) and we have already seen that it is \emph{not} \good{}. We shall refer to this $2$-category as the \emph{bubble}.
+\end{paragr}
+\begin{paragr}
+  Recall that for $n\geq 0$, we denote by $\Delta_n$ the linear order ${0 \leq \cdots \leq n}$ seen as a small category. Let $i : \Delta_1 \to \Delta_n$ be the unique functor such that
+  \[
+  i(0)=0 \text{ and } i(1)=n.
+  \]
+\end{paragr}
+\begin{lemma}
+  For $n\neq0$, the functor $i : \Delta_1 \to \Delta_n$ is a strong deformation retract (\ref{paragr:defrtract}).
+\end{lemma}
+\begin{proof}
+  Let $r : \Delta_n \to \Delta_1$ the unique functor such that
+  \[
+  r(n)=1\text{ and } r(k)=1 \text{ for } k\neq n.
+  \]
+  By definition we have $r \circ i = 1_{\Delta_1}$. Now, the natural order on $\Delta_n$ induces a natural transformation
+  \[
+  \alpha : i\circ r \Rightarrow \mathrm{id}_{\Delta_n},
+  \]
+  and it is straightforward to check that $\alpha \ast i = \mathrm{id}_i$.
+  \todo{Est-ce qu'il ne faudra pas dire quelque part qu'une transfo naturelle donne une transfo oplax}.
+\end{proof}
+\begin{paragr}
+  In particular, it follows from Lemma \ref{lemma:pushoutstrngdefrtract} that if $n\neq0$, then $i : \Delta_1 \to \Delta_n$ is a co-universal Thomason weak equivalences. Now consider the following cocartesian square
+  \[
+  \begin{tikzcd}
+    \Delta_1 \ar[r,"i"] \ar[d,"\tau"] & \Delta_n \ar[d] \\
+    A_{(1,1)} \ar[r] & A_{(1,n)}
+    \ar[from=1-1,to=2-2,phantom,very near end,"\ulcorner"]
+  \end{tikzcd},
+  \]
+  where $\sigma : \Delta_1 \to A_{(1,1)}$ is the $2$-functor that points to the the target of the generating $2$-cell of $A_{(1,1)}$
+  \[
+  \tau = \begin{tikzcd} {0 \to 1} \ar[d,"\langle f \rangle"] \\ A \end{tikzcd}
+  \]
+\end{paragr}

hmtpy.tex

@@ -322,7 +322,7 @@ From now on, we will consider that the category $\Psh{\Delta}$ is equipped with
         \end{enumerate}
         A deformation retract is a particular case of homotopy equivalence and thus of Thomason weak equivalence. 
       \end{paragr}
-      \begin{lemma}
+      \begin{lemma}\label{lemma:pushoutstrngdefrtract}
        The pushout of a strong deformation retract is a strong deformation retract.
       \end{lemma}
       \begin{proof}