( s D(\varphi)_0 , D(\varphi)_1 (\ell_B)'_1 \pi_1 ) ) c_{\varphi ; 1_B} \pi_0 \\
&= (
s ( 1_{D(A)_0} , e_A D(\varphi)_1 )
, \
( s D(\varphi)_0 , D(\varphi)_1 (\ell_B)'_1 \pi_1 ) ) p_0 \pi_0 \\
s ( 1_{D(A)_0} , e_A D(\varphi)_1 ) \pi_0 \\
&= s 1_{D(A)_0} \\
&= s
\end{align*}

and by Lemma <ref> and functoriality of $D(\varphi)$ we have

\begin{align*}
& \ \ \ \
s ( 1_{D(A)_0} , e_A D(\varphi)_1 )
, \
( s D(\varphi)_0 , D(\varphi)_1 (\ell_B)'_1 \pi_1 ) ) c_{\varphi ; 1_B} \pi_1\\
&= (
s ( 1_{D(A)_0} , e_A D(\varphi)_1 )
, \
( s D(\varphi)_0 , D(\varphi)_1 (\ell_B)'_1 \pi_1 ) ) c'_{\delta ; \varphi ; 1_B} c\\
&= ( s \delta_{\varphi ; 1_B} , s e_A D(\varphi)_1 D(1_B)_1 , D(\varphi)_1 (\ell_B)'_1 \pi_1 ) c  \\
&= ( s \delta_{\varphi ; 1_B} , s D(\varphi)_0 e_B D(1_B)_1 , D(\varphi)_1 (\ell_B)'_1 \pi_1 ) c
\end{align*}

\[ (
s ( 1_{D(A)_0} , e_A D(\varphi)_1 )
, \
D(\varphi)_1 (\ell_B)'_1 ) \iota_{\varphi ; 1_B}
= (
s ( 1_{D(A)_0} , e_A D(\varphi)_1 ) \iota_\varphi
, \
D(\varphi)_1 (\ell_B)'_1 \iota_{1_B} ) \]

By the universal property of $\mD_2$, it suffices to check

\begin{align*}
s ( 1_{D(A)_0} , e_A D(\varphi)_1 )
, \
D(\varphi)_1 (\ell_B)'_1 ) \iota_{\varphi ; 1_B} \rho_0
&= (
s ( 1_{D(A)_0} , e_A D(\varphi)_1 )
, \
D(\varphi)_1 (\ell_B)'_1 ) p_0 \iota_\varphi \\
s ( 1_{D(A)_0} , e_A D(\varphi)_1 ) \iota_\varphi
\end{align*}

\begin{align*}
s ( 1_{D(A)_0} , e_A D(\varphi)_1 )
, \
D(\varphi)_1 (\ell_B)'_1 ) \iota_{\varphi ; 1_B} \rho_1
&= (
s ( 1_{D(A)_0} , e_A D(\varphi)_1 )
, \
D(\varphi)_1 (\ell_B)'_1 ) p_1 \iota_{1_B} \\
D(\varphi)_1 (\ell_B)'_1 \iota_{1_B}
\end{align*}

§ INTERNAL CATEGORY OF FRACTIONS

§.§ Defining Span Composition on Representatives

This appendix consists of technical lemmas which are really just computations used in the proof of Lemma <ref> in Chapter <ref>. We use these to define the composition structure of the internal category of fractions and prove it forms an internal category. They are heavily dependant on their context in that lemma so we restate the beginning of that proof and include the diagrams of covers that define the lifts from the fractions axioms being referred to in the lemmas.

First, pullbacks of $u : U \to \spn \tensor[_{t}]{\times}{_s} \spn$ are taken along $p_0^2$ and $p_1^2$ to get two covers of $\slb \tensor[_{t}]{\times}{_s}\slb$ that witness composition of the sailboat projections, $p_0^2$ and $p_1^2$:

\[\label{dgm slb proj pb along span comp cover (appendix)}
\begin{tikzcd}[]
\bar{U}_0 \arrow[dr, phantom, "\usebox\pullback" , very near start, color=black] \dar["/" marking, "\bar{u}_0"' near end] \rar["\pi_1"] & U \dar["/" marking, "u" near start] & \bar{U}_1 \dar["/" marking, "\bar{u}_1" near start] \lar["\pi_1"'] \arrow[dl, phantom, "\usebox\urpullback" , very near start, color=black]\\
\slb \tensor[_{t}]{\times}{_s} \slb \rar["p_0^2"'] & \spn \tensor[_{t}]{\times}{_s} \spn & \slb \tensor[_{t}]{\times}{_s} \slb \lar["p_1^2"]
\end{tikzcd} \tag{1}
\]

A refinement

\[ \label{dgm slb proj pb along span comp cover refinement (appendix)}
\begin{tikzcd}[]
\bar{U} \ar[d,"\pi_0"'] \ar[r, "\pi_1"] \ar[dr, "/" marking, "\bar{u}" near start] & \bar{U}_1 \dar["/" marking,"\bar{u}_1" near start] \\
\bar{U}_0 \rar["/" marking,"\bar{u}_0"' near end] & \slb \tensor[_{t}]{\times}{_s} \slb
\end{tikzcd} \tag{2}
\]

is given by a pullback of $\bar{u}_0$ and $\bar{u}_1$ and provides us with a common cover domain for the cover. Next we need to describe composition for the intermediate pair of composable spans:

\begin{tikzcd}[]
&& & \cdot \dar[dotted] \ar[dl, "\circ" marking] \ar[dr,] & \\
\cdot & \cdot \lar["\circ" marking] \rar & \cdot & \cdot \rar[dotted] & \cdot
\end{tikzcd}
\right]$

The following figure shows the construction of three different composites being constructed.

\[ \label{fig intermediate span comp well-defined (appendix)} \begin{tikzcd}[]
&& \cdot \\
& \cdot & \cdot \\
& \cdot & \cdot & \cdot \\
\cdot & \cdot & \cdot & \cdot & \cdot \\
&& \cdot \\
&& \cdot
\arrow[from=4-2, to=4-1, "\circ" marking ]
\arrow[from=4-2, to=4-3]
\arrow[from=3-4, to=4-4]
\arrow[from=4-4, to=4-3, "\circ" marking ]
\arrow[from=4-4, to=4-5]
\arrow[from=3-2, to=4-2]
\arrow[from=3-2, to=4-1, "\circ" marking ]
\arrow[from=3-4, to=4-3, "\circ" marking ]
\arrow[from=2-3, to=3-4, color = teal]
\arrow[from=3-3, to=4-2, "\circ" marking, color = purple ]
\arrow[from=3-3, to=3-4, color = purple]
\arrow[from=5-3, to=4-2, "\circ" marking , color = orange ]
\arrow[from=5-3, to=4-4, color = orange ]
\arrow[from=6-3, to=5-3, color = orange ]
\arrow[from=1-3, to=2-3, color = teal]
\arrow[from=2-2, to=3-3, color = purple]
\arrow[from=2-3, to=3-2, crossing over, "\circ" marking, color = teal]
\arrow[curve={height=6pt}, from=2-2, to=4-1, "\circ" marking, color = purple]
\arrow[curve={height=30pt}, from=1-3, to=4-1, "\circ" marking , color = teal]
\arrow[curve={height=-6pt}, from=6-3, to=4-1, "\circ" marking , color = orange ]
\end{tikzcd} \tag{A}\]

We define composition for this intermediate span similarly to how we defined $\sigma_\circ$. This could actually have been done by taking a pullback of the cover, $u: U \to \spn \tensor[_{t}]{\times}{_s} \spn$, witnessing span composition in general and finding a common refinement for this with the previous refinement. The same result holds either way. Denote the comparison pair of composable spans by $\gamma$ and define it by the universal property in the following pullback diagram.

\[ \label{dgm intermediate compblespan (appendix)}
\begin{tikzcd}[column sep = large, row sep = large]
\bar{U} \ar[d, "/" marking, "\bar{u}"' near end] \ar[r, "/" marking, "\bar{u}" near end] \ar[dr, dotted, "\gamma"]
& \slb \tensor[_{t}]{\times}{_s} \slb \rar["p_1^2"]
& \spn \tensor[_{t}]{\times}{_s} \spn \dar["\pi_1"]
\\
\slb \tensor[_{t}]{\times}{_s} \slb \dar[ "p_0^2"']
& \spn \tensor[_{t}]{\times}{_s} \spn \dar["\pi_0"'] \rar["\pi_1"]
& \spn \dar["s"]
\\
\spn \tensor[_{t}]{\times}{_s} \spn \rar["\pi_0"']
&\spn \rar["t"']
& \mC_0
\end{tikzcd} \tag{3}
\]

The following diagram of covers shows how the intermediate composite span is constructed for $\gamma$.

\[ \label{dgm diagram of covers to include composite of intermediate comp'ble spans(appendix)}
\begin{tikzcd}[column sep = large ]
W_\circ \rar[rr, "(\pi_0 \pi_1 {,} \pi_0 \pi_2)"]
&& W \times_{\mC_0} W
& \\
\tilde{U}
\dar[shift left = 1.5, bend left =50, "\sigma_1", color = teal ]
\dar[color = purple, "\sigma_\gamma"']
\dar[shift right = 1.5, bend right= 50, "\sigma_0"' , color = orange]
\uar[color = purple, "\omega_\gamma"]
\rar[rr, "/" marking , "\tilde{u}_0" near start]
& \tilde{U}_0
\dar[color = purple, "\theta_\gamma"']
\uar[color = purple, "(\theta_\gamma \pi_0 \pi_0 {, } \tilde{u}_1 \gamma \pi_0 \pi_0) "']
\rar["/" marking , "\tilde{u}_1" near start]
& \bar{U}
% \dar[shift left = 1.5, "(\bar{u} p_0 \pi_0 \pi_1 {,} \bar{u} p_0 \pi_1 \pi_0)", color = orange]
\dar[color = purple, "(\gamma \pi_0 \pi_1 {, }\gamma \pi_1 \pi_0)"]
%\dar[shift right = 1.5, "(\bar{u} p_1 \pi_0 \pi_1 {,} \bar{u} p_1 \pi_1 \pi_0 )"', color = teal]
\\
\spn
& W_\square
\rar["(\pi_0 \pi_1 {,} \pi_1 \pi_1)"']
& \mC_1 \tensor[_{t}]{\times}{_{wt}} W
\end{tikzcd} \tag{$\star$}
\]

The left and right curved arrows, $\textcolor{orange}{\sigma_0}$ and $\textcolor{teal}{\sigma_1}$, into $\spn$ in the bottom left corner are defined by applying the composite of spans, $\sigma_\circ$, to the composable spans given by applying $p_0^2$ and $p_1^2$ to the pair of composable sailboats. Since $\sigma_\circ$ is only defined on $U$ we need to pass through the appropriate cover. The colours in the previous diagram and following equations indicate which of the three different span compositions in Figure (<ref>) the arrows in the following equations are witnessing.

\begin{align}\label{def sigma_0 (appendix)}
\begin{split}
\textcolor{orange}{\sigma_0}
&= \textcolor{orange}{\tilde{u} \pi_0 \pi_1 \sigma_\circ} \\
&= \textcolor{orange}{\tilde{u} \pi_0 \pi_1 \big( \omega \pi_1 , (\omega \pi_0 \pi_0 {,} u_0 \theta \pi_1 \pi_0 {,} u \pi_1 \pi_1 )c \big)}
\end{split}
\end{align}

\begin{align}\label{def sigma_1 (appendix)}
\begin{split}
\textcolor{teal}{\sigma_1 }
&= \textcolor{teal}{\tilde{u} \pi_1 \pi_1 \sigma_\circ} \\
&= \textcolor{teal}{\tilde{u} \pi_1 \pi_1 \big( \omega \pi_1 , (\omega \pi_0 \pi_0 {,} u_0 \theta \pi_1 \pi_0 {,} u \pi_1 \pi_1 )c \big)}.
\end{split}
\end{align}

The arrow into $\spn$ on the bottom left side of the cover diagram is the universal map

\[ \textcolor{purple}{\sigma_\gamma} = \big( \omega_\gamma \pi_1 {,} (\omega_\gamma \pi_0 \pi_0 {,} \tilde{u}' \theta_\gamma \pi_1 \pi_0{,} \tilde{u} \bar{u} p_1^2 \pi_1 \pi_1 )c \big).\]

The data necessary to construct witnessing sailboats for the equivalences between the pairs of spans $\textcolor{orange}{\sigma_0}$, $\textcolor{teal}{\sigma_1}$, and $\textcolor{purple}{ \sigma_\gamma}$ can be obtained by applying the Ore condition, followed by the diagram-extension twice, and then weak composition three times. Internally this corresponds to a chain of six covers and lifts. All of this is color-coded below using olive and brown for the Ore condition and cyan and violet for the zippering and weak composition step(s) that follow. Note that in both cases the first zippering is done to parallel pairs of composites that can be post-composed by the left leg of the bottom left span. The second zipper is done to parallel pairs of composites that can be post-composed with the left leg of the bottom right span in the pair of composale sailboats. Weak composition is then applied three times in to get comparison spans, $\textcolor{cyan}{\sigma_{0, \gamma}}$ and $\textcolor{violet}{\sigma_{1,\gamma}}$, whose left legs are in $W$.

\[ \label{fig Ore + zip + w.c. showing span comp is well def wrt equiv reln (appendix)}
\begin{tikzcd}
\cdot & \cdot & \cdot & \cdot \\
&&& \cdot \\
&&& \cdot \\
&& \cdot & \cdot & \cdot \\
&&& \cdot & \cdot & \cdot \\
{} && \cdot & \cdot & \cdot & \cdot & \cdot & \cdot & \cdot & \cdot \\
&&&& \cdot &&&&& \cdot \\
&&&& \cdot &&&&& \cdot \\
&&&&&&&&& \cdot
\arrow[from=6-4, to=6-3,"\circ" marking]
\arrow[from=6-4, to=6-5]
\arrow[from=6-6, to=6-5, "\circ" marking]
\arrow[from=6-6, to=6-7]
\arrow[from=5-6, to=6-6]
\arrow[from=5-6, to=6-5, "\circ" marking]
\arrow[from=5-5, to=6-4, purple, "\circ" marking]
\arrow[from=5-5, to=5-6, purple]
\arrow[curve={height=-90pt}, from=9-10, to=6-3, cyan, "\circ" marking]
\arrow[from=9-10, to=8-10, cyan]
\arrow[from=8-10, to=7-10, cyan]
\arrow[from=7-10, to=6-10, cyan]
\arrow[from=6-10, to=6-9, cyan, "\circ" marking]
\arrow[from=6-9, to=6-8, cyan, "\circ" marking]
\arrow[from=7-10, to=6-8, cyan, "\circ" marking]
\arrow[from=7-5, to=6-4, orange, "\circ" marking]
\arrow[from=7-5, to=6-6, orange]
\arrow[from=8-5, to=7-5, orange]
\arrow[curve={height=-12pt}, from=8-5, to=6-3, orange, "\circ" marking]
\arrow[curve={height=-18pt}, from=6-8, to=8-5, olive, "\circ" marking]
\arrow[curve={height=-12pt}, from=8-10, to=8-5, cyan, "\circ" marking]
\arrow[from=1-4, to=2-4, violet, "\circ" marking]
\arrow[curve={height=6pt}, from=4-3, to=6-3, teal, "\circ" marking]
\arrow[from=4-4, to=5-6, teal]
\arrow[from=4-5, to=5-5, purple, crossing over]
\arrow[from=4-3, to=4-4, teal]
\arrow[from=5-4, to=6-3, "\circ" marking]
\arrow[from=5-4, to=6-4]
\arrow[from=4-4, to=5-4, teal, "\circ" marking, near start]
\arrow[curve={height=15pt}, from=4-5, to=6-3, purple, "\circ" marking, crossing over]
\arrow[curve={height=18pt}, from=6-8, to=4-5, olive]
\arrow[from=2-4, to=3-4, violet, "\circ" marking]
\arrow[curve={height=6pt}, from=3-4, to=4-3, brown, "\circ" marking]
\arrow[curve={height=-6pt}, from=3-4, to=4-5, brown]
\arrow[curve={height=6pt}, from=1-3, to=3-4, violet, "\circ" marking]
\arrow[curve={height=6pt}, from=1-2, to=4-3, violet, "\circ" marking]
\arrow[curve={height=12pt}, from=1-1, to=6-3, violet, "\circ" marking]
\arrow[from=1-1, to=1-2, violet]
\arrow[from=1-2, to=1-3, violet]
\arrow[from=1-3, to=1-4, violet]
\end{tikzcd} \tag{B}
\]

The corresponding diagrams of covers and lifts which witness the arrows in the Ore squares and zippering in Diagram <ref> are:

\[\label{cover dgms for showing span comp well def : Ore + zip (appendix)}
\begin{tikzcd}[column sep = large]
& \cP(\mC) \rar["\pi_1"]
& \cP_{cq}(\mC)
\\
\hat{U}_3
\rar["/" marking, "\hat{u}_3" near start]
\dar[shift left, "\delta_{\rho_0}", color = cyan]
\dar[shift right, "\delta_{\rho_1}"', color = violet]
\rar["/" marking, "\hat{u}_4" near start]
\uar[shift right, "\delta_{\lambda_0}"', color = cyan]
\uar[shift left, "\delta_{\lambda_1}", color = violet]
\dar[shift left, "\rho_0", color = cyan]
\dar[shift right, "\rho_1"', color = violet]
\rar["/" marking, "\hat{u}_5" near start]
\dar[shift left, "\theta_{\gamma_0}", color = olive]
\dar[shift right, "\theta_{\gamma_1}"', color = brown]
\uar[shift right, "\lambda_0"', color = cyan]
\uar[shift left, "\lambda_1", color = violet]
\dar[shift right, "(\sigma_1 \pi_0 w {,} \sigma_\gamma \pi_0)"', color = brown]
\dar[shift left, "(\sigma_0 \pi_0 w {,} \sigma_\gamma \pi_0 )", color = olive]
\\
\cP(\mC) \rar["\pi_1"']
& \cP_{cq}(\mC)
& W_\square \rar["(\pi_0 \pi_1 {,} \pi_1 \pi_1)"']
& \mC_1 \tensor[_{t}]{\times}{_{wt}} W
\end{tikzcd} \tag{$\star \star$}
\]

The covers, $\hat{u}_2, \hat{u}_1,$ and $\hat{u}_0$, witness three applications of weak composition in each case as seen in the following continued sequence of covers:

\[\label{cover dgms for showing span comp well def : weak comp x3 (appendix)}
\begin{tikzcd}[column sep = large]
W_\circ \rar[r, "(\pi_0 \pi_1 {,} \pi_0 \pi_2)"]
& W \times_{\mC_0} W
W_\circ \rar[r, "(\pi_0 \pi_1 {,} \pi_0 \pi_2)"]
& W \times_{\mC_0} W
& \\
\hat{U}
\rar["/" marking, "\hat{u}_0" near start]
\uar[shift right, "\omega_{0,0}"', color = cyan]
\uar[shift left, "\omega_{1,0}", color = violet]
\dar[shift left = 1.5,""]
\dar[shift right= 1.5 ,""']
\dar[shift left=.5]
\dar[shift right= .5]
& \hat{U}_1
\rar["/" marking,"\hat{u}_1" near start]
\uar[shift right, "\omega_{0,0}'"', color = cyan]
\uar[shift left, "\omega_{1,0}'", color = violet]
\dar[shift left, "\omega_{0,1}", color = cyan]
\dar[shift right, "\omega_{1,1}"', color = violet]
& \hat{U}_2
\rar["/" marking,"\hat{u}_2" near start]
\uar[shift right, ""', color = cyan, "\omega_{0, 2}"']
\uar[shift left, "", color = violet, "\omega_{1, 2}"]
\dar[shift right, ""', color = violet, "\omega_{1, 1}'"']
\dar[shift left, "", color = cyan, "\omega_{0, 1}'"]
& \hat{U}_3
\uar[shift right, ""', color = cyan, "\omega_{0,2}'"']
\uar[shift left, "", color = violet, "\omega_{1,2}'"]
\\
\slb &
W_\circ \rar[r, "(\pi_0 \pi_1 {,} \pi_0 \pi_2)"']
& W \times_{\mC_0} W
\end{tikzcd} \tag{$\star \star \star$}
\]

The following lemmas refer to the labeled diagrams and equations above.

The maps

\[ \begin{tikzcd}[column sep = large]
\hat{U} \rar[shift right, cyan, "\lambda_0'"'] \rar[shift left, violet, "\lambda_1'"] & P(\mC) \tensor[_t]{\times}{_{ws}} W
\end{tikzcd}\]

are defined in a similar fashion to $\delta_0'$ in Lemma <ref>, namely by descending through the preceeding covers and expanding both sides of the Ore-square equations witnessed.

To define $\lambda_0 '$ we expand both sides of the Ore-square equation

\[\big( \textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0 w \
{,} \ \textcolor{olive}{\sigma_{\gamma_0}} \pi_0 \pi_1
\big) c
= \big( \textcolor{olive}{\theta_{\gamma_0}} \pi_1 \pi_0 w \
{,} \ \textcolor{olive}{\sigma_{\gamma_0}} \pi_1 \pi_1 w
\big) c \\\]

On the left-hand side we have

\begin{align}
\begin{split}
& \ \ \ \ \big( \textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0 w \
{,} \ \textcolor{olive}{\sigma_{\gamma_0}} \pi_0 \pi_1
\big) c \\
&= \big( \textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0 w \
{,} \ \hat{u}_5 \textcolor{orange}{\sigma_0} \pi_0 w
\big) c \\
&= \big( \textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0 w \
{,} \ \hat{u}_5 \tilde{u} \textcolor{orange}{\pi_0 \pi_1} \sigma \pi_0 w
\big) c \\
\big( \textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0 w \
{,} \ \hat{u}_5 \tilde{u} \textcolor{orange}{\pi_0 \pi_1 \omega} \pi_1 w
\big) c \\
\big(
\textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0 w \
{,} \ \hat{u}_5 \tilde{u} \textcolor{orange}{\pi_0 \pi_1 \omega} \pi_1 w
\big) c \\
\big(
\textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0 w \
{,} \ \hat{u}_5 \tilde{u} \textcolor{orange}{\pi_0 \pi_1}(\omega \pi_0 \pi_0 \
{,} \ u_0 \theta \pi_0 \pi_0 w \
{,} \ u \pi_0 \pi_0 w)c
\big) c \\
\big(
\textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0 w \
{,} \ (\hat{u}_5 \tilde{u} \textcolor{orange}{\pi_0 \pi_1 \omega} \pi_0 \pi_0 \
{,} \ \hat{u}_5 \tilde{u} \textcolor{orange}{\pi_0 \pi_1 u_0 \theta} \pi_0 \pi_0 w \
{,} \ \hat{u}_5 \tilde{u} \pi_0 \pi_1 u \pi_0 \pi_0 w )c
\big) c\\
\big(
\textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0 w \
{,} \ \hat{u}_5 \tilde{u} \textcolor{orange}{\pi_0 \pi_1 \omega} \pi_0 \pi_0 \
{,} \ \hat{u}_5 \tilde{u} \textcolor{orange}{\pi_0 \pi_1 u_0 \theta} \pi_0 \pi_0 w \
{,} \ \hat{u}_5 \tilde{u} \pi_0 \pi_1 u \pi_0 \pi_0 w
\big) c \\
\big(
\textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0 w \
{,} \ \hat{u}_5 \tilde{u} \textcolor{orange}{\pi_0 \pi_1 \omega} \pi_0 \pi_0 \
{,} \ \hat{u}_5 \tilde{u} \textcolor{orange}{\pi_0 \pi_1 u_0 \theta} \pi_0 \pi_0 w \
{,} \ \hat{u}_5 \tilde{u} \pi_0 \pi_0 p_0^2 \pi_0 \pi_0 w
\big) c \\
&= \big(
(\textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0 w \
{,} \ \hat{u}_5 \tilde{u} \textcolor{orange}{\pi_0 \pi_1 \omega} \pi_0 \pi_0 \
{,} \ \hat{u}_5 \tilde{u} \textcolor{orange}{\pi_0 \pi_1 u_0 \theta} \pi_0 \pi_0 w)c \
{,} \ \hat{u}_5 \tilde{u} \pi_0 \pi_0 p_0^2 \pi_0 \pi_0 w
\big) c
\end{split}
\end{align}

and on the right we have

\begin{align}
\begin{split}
& \ \ \ \  \big( \textcolor{olive}{\theta_{\gamma_0}} \pi_1 \pi_0 w \
{,} \ \textcolor{olive}{\sigma_{\gamma_0}} \pi_1 \pi_1 w
\big) c \\
&= \big( \textcolor{olive}{\theta_{\gamma_0}} \pi_1 \pi_0 w \
{,} \ \hat{u}_5 \textcolor{purple}{\sigma_\gamma} \pi_0 w
\big) c \\
&= \big( \textcolor{olive}{\theta_{\gamma_0}} \pi_1 \pi_0 w \
{,} \ \hat{u}_5 \textcolor{purple}{\omega_\gamma} \pi_1 w
\big) c \\
&= \big( \textcolor{olive}{\theta_{\gamma_0}} \pi_1 \pi_0 w \
{,} \ \hat{u}_5 ( \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 \
{,} \ \textcolor{purple}{\omega_\gamma} \pi_0 \pi_1 w\
{,} \ \textcolor{purple}{\omega_\gamma} \pi_0 \pi_2 w)c
\big) c \\
&= \big( \textcolor{olive}{\theta_{\gamma_0}} \pi_1 \pi_0 w \
{,} \ \hat{u}_5 ( \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 \
{,} \ \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w \
{,} \ \tilde{u} \gamma \pi_0 \pi_0w )c
\big) c \\
&= \big( \textcolor{olive}{\theta_{\gamma_0}} \pi_1 \pi_0 w \
{,} \ \hat{u}_5 ( \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 \
{,} \ \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w \
{,} \ \tilde{u} \pi_0 \pi_1 u \pi_0 \pi_0 w )c
\big) c \\
&= \big( \textcolor{olive}{\theta_{\gamma_0}} \pi_1 \pi_0 w \
{,} \ \hat{u}_5 ( \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 \
{,} \ \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w \
{,} \ \tilde{u} \pi_0 \pi_0 p_0^2 \pi_0 \pi_0 w )c
\big) c \\
&=  \textcolor{olive}{\theta_{\gamma_0}} \pi_1 \pi_0 w \
{,} \ \hat{u}_5 ( \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 \
{,} \ \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w \
{,} \ \tilde{u} \pi_0 \pi_0 p_0^2 \pi_0 \pi_0 w )c
\big) c \\
&=  \textcolor{olive}{\theta_{\gamma_0}} \pi_1 \pi_0 w \
{,} \ \hat{u}_5 \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 \
{,} \ \hat{u}_5 \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w \
{,} \ \hat{u}_5 \tilde{u} \pi_0 \pi_0 p_0^2 \pi_0 \pi_0 w
\big) c \\
&= \big( (\textcolor{olive}{\theta_{\gamma_0}} \pi_1 \pi_0 w \
{,} \ \hat{u}_5 \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 \
{,} \ \hat{u}_5 \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w )c \
{,} \ \hat{u}_5 \tilde{u} \pi_0 \pi_0 p_0^2 \pi_0 \pi_0 w
\big) c
\end{split}.
\end{align}

The last lines in equations $(1)$ and $(2)$ uniquely determine $\textcolor{cyan}{\lambda_0'}$ by

\begin{align*}
\textcolor{cyan}{\lambda_0'} \pi_1
&= \hat{u}_5 \tilde{u} \pi_0 \pi_0 p_0^2 \pi_0 \pi_0 w \\
\textcolor{cyan}{\lambda_0'} \pi_0 \pi_0
&= (\textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0 w \
{,} \ \hat{u}_5 \tilde{u} \textcolor{orange}{\pi_0 \pi_1 \omega} \pi_0 \pi_0 \
{,} \ \hat{u}_5 \tilde{u} \textcolor{orange}{\pi_0 \pi_1 u_0 \theta} \pi_0 \pi_0 w)c \\
\textcolor{cyan}{\lambda_0'} \pi_0 \pi_1
&=(\textcolor{olive}{\theta_{\gamma_0}} \pi_1 \pi_0 w \
{,} \ \hat{u}_5 \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 \
{,} \ \hat{u}_5 \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w )c
\end{align*}

The map $\textcolor{violet}{\lambda_1'}$ is similarly determined by expanding both sides of the Ore-square equation:

\[\big( \textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 w \
{,} \ \textcolor{brown}{\sigma_{\gamma_1}} \pi_0 \pi_1
\big) c
= \big( \textcolor{brown}{\theta_{\gamma_1}} \pi_1 \pi_0 w \
{,} \ \textcolor{brown}{\sigma_{\gamma_1}} \pi_1 \pi_1 w
\big) c \]

On the left-hand side we get

\begin{align}
\begin{split}
& \ \ \ \  \big( \textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 w
{,} \ \textcolor{brown}{\sigma_{\gamma_1}} \pi_0 \pi_1
\big) c \\
&= \big( \textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 w
{,} \ \hat{u}_5 \textcolor{teal}{\sigma_1} \pi_0 w
\big) c \\
&= \big( \textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 w
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1} \sigma \pi_0 w
\big) c \\
&= \big( \textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 w
{,} \ \hat{u}5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_1 w
\big) c \\
\big(
\textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 w
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_1 w
\big) c \\
\big(
\textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 w
{,} \\
& \ \ \ \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1}(\omega \pi_0 \pi_0
{,} \ u_0 \theta \pi_0 \pi_0 w
{,} \ u \pi_0 \pi_0 w)c
\big) c \\
\big(
\textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 w
{,} \\
& \ \ \ \ (\hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_0 \pi_0 w
{,} \ \hat{u}_5 \tilde{u} \pi_1 \pi_1 u \pi_0 \pi_0 w )c
\big) c\\
\big(
\textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0 w
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_0 \pi_0 w
{,} \ \hat{u}_5 \tilde{u} \pi_1 \pi_1 u \pi_0 \pi_0 w
\big) c \\
\big(
\textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 w
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_0 \pi_0 w
{,} \ \hat{u}_5 \tilde{u} \pi_1 \pi_0 p_1^2 \pi_0 \pi_0 w
\big) c \\
&= \big(
( \textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 w
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_0 \pi_0 w)c
{,} \\
& \ \ \ \
\hat{u}_5 \tilde{u} \pi_1 \pi_0 p_1^2 \pi_0 \pi_0 w
\big) c \\
&= \big(
(\textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 w
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_0 \pi_0 w)c
{,} \\
& \ \ \ \
\hat{u}_5 \tilde{u} \pi_1 \pi_0 \pi_0 \pi_0 \pi_1 w
\big) c \\
&= \big(
( \textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 w
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_0 \pi_0 w)c
{,} \\
& \ \ \ \
\hat{u}_5 \tilde{u} \bar{u} \pi_0 \pi_0 \pi_1 w
\big) c \\
&= \big(
(\textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 w
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_0 \pi_0 w)c
{,} \\
& \ \ \ \
(\hat{u}_5 \tilde{u} \bar{u} \pi_0 \pi_0 \pi_0 \pi_0
{,} \ \hat{u}_5 \tilde{u} \bar{u} \pi_0 \pi_0 \pi_0 \pi_1 w)c
\big) c \\
(\textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 w
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_0 \pi_0 w
{,} \ \hat{u}_5 \tilde{u} \bar{u} \pi_0 \pi_0 \pi_0 \pi_0 )c
{,} \\
& \ \ \ \
\hat{u}_5 \tilde{u} \bar{u} \pi_0 \pi_0 \pi_0 \pi_1 w
\big) c \\
( \textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 w
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_0 \pi_0 w
{,} \ \hat{u}_5 \tilde{u} \bar{u} \pi_0 \pi_0 \pi_0 \pi_0 )c
{,} \\
& \ \ \ \
\hat{u}_5 \tilde{u} \pi_0 \pi_0 \pi_0 \pi_0 \pi_0 \pi_1 w
\big) c \\
&= \big(
( \textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 w
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_0 \pi_0 w
{,} \ \hat{u}_5 \tilde{u} \bar{u} \pi_0 \pi_0 \pi_0 \pi_0 )c
{,} \\
& \ \ \ \
\hat{u}_5 \tilde{u} \pi_0 \pi_0 p_0^2 \pi_0 \pi_0 w
\big) c
\end{split}
\end{align}

and on the right-hand side we have

\begin{align}
\begin{split}
& \ \ \ \  \big( \textcolor{brown}{\theta_{\gamma_1}} \pi_1 \pi_0 w \
{,} \ \textcolor{brown}{\sigma_{\gamma_1}} \pi_1 \pi_1 w
\big) c \\
&= \big( \textcolor{brown}{\theta_{\gamma_1}} \pi_1 \pi_0 w \
{,} \ \hat{u}_5 \textcolor{purple}{\sigma_\gamma} \pi_0 w
\big) c \\
&= \big( \textcolor{brown}{\theta_{\gamma_1}} \pi_1 \pi_0 w \
{,} \ \hat{u}_5 \textcolor{purple}{\omega_\gamma} \pi_1 w
\big) c \\
&= \big( \textcolor{brown}{\theta_{\gamma_1}} \pi_1 \pi_0 w \
{,} \ \hat{u}_5 ( \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 \
{,} \ \textcolor{purple}{\omega_\gamma} \pi_0 \pi_1 w\
{,} \ \textcolor{purple}{\omega_\gamma} \pi_0 \pi_2 w)c
\big) c \\
&= \big( \textcolor{brown}{\theta_{\gamma_1}} \pi_1 \pi_0 w \
{,} \ \hat{u}_5 ( \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 \
{,} \ \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w \
{,} \ \tilde{u} \gamma \pi_0 \pi_0w )c
\big) c \\
&= \big( \textcolor{brown}{\theta_{\gamma_1}} \pi_1 \pi_0 w \
{,} \ \hat{u}_5 ( \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 \
{,} \ \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w \
{,} \ \tilde{u} \pi_0 \pi_1 u \pi_0 \pi_0 w )c
\big) c \\
&= \big( \textcolor{brown}{\theta_{\gamma_1}} \pi_1 \pi_0 w \
{,} \ \hat{u}_5 ( \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 \
{,} \ \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w \
{,} \ \tilde{u} \pi_0 \pi_0 p_0^2 \pi_0 \pi_0 w )c
\big) c \\
&= \big( \textcolor{brown}{\theta_{\gamma_1}} \pi_1 \pi_0 w \
{,} \ \hat{u}_5( \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 \
{,} \ \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w \
{,} \ \tilde{u} \pi_0 \pi_0 p_0^2 \pi_0 \pi_0 w )c
\big) c \\
&= \big( \textcolor{brown}{\theta_{\gamma_1}} \pi_1 \pi_0 w \
{,} \ \hat{u}_5 \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 \
{,} \ \hat{u}_5 \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w \
{,} \ \hat{u}_5 \tilde{u} \pi_0 \pi_0 p_0^2 \pi_0 \pi_0 w
\big) c \\
&= \big( ( \textcolor{brown}{\theta_{\gamma_1}} \pi_1 \pi_0 w \
{,} \ \hat{u}_5 \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 \
{,} \ \hat{u}_5 \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w )c \
{,} \ \hat{u}_5 \tilde{u} \pi_0 \pi_0 p_0^2 \pi_0 \pi_0 w
\big) c
\end{split}
\end{align}

The last lines of equations (3) and (4) uniquely determine the $\textcolor{violet}{\lambda_1'}$ by

\begin{align*}
\textcolor{violet}{\lambda_1'} \pi_1 &= \hat{u}_5 \tilde{u} \pi_0 \pi_0 p_0^2 \pi_0 \pi_0 , \\
\textcolor{violet}{\lambda_1'} \pi_0 \pi_0 &= (\textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 w \
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0 \
{,} \ \hat{u}_5 \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_0 \pi_0 w \
{,} \ \hat{u}_5 \tilde{u} \bar{u} \pi_0 \pi_0 \pi_0 \pi_0 )c,\\
\textcolor{violet}{\lambda_1'} \pi_0 \pi_1 &=( \textcolor{brown}{\theta_{\gamma_1}} \pi_1 \pi_0 w \
{,} \ \hat{u}_5 \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 \
{,} \ \hat{u}_5 \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w )c
\end{align*}

The equation

\begin{align*}
(\textcolor{cyan} {\rho_0'} \pi_0 \pi_0 , \textcolor{cyan} {\rho_0'} \pi_1) c
&= (\textcolor{cyan} {\rho_0'} \pi_0 \pi_1 , \textcolor{cyan} {\rho_0'} \pi_1) c
\end{align*}

the composite

\[\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0w , \
\hat{u}_4 \textcolor{olive}{\omega_{\gamma_0} } \pi_1 \pi_0 , \
\hat{u}_4 \hat{u}_5 \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 , \
\hat{u}_4 \hat{u}_5 \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0 , \
\hat{u}_4 \hat{u}_5\tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_0
)c , \
\hat{u}_4 \hat{u}_5 \tilde{u} \bar{u} p_0^2 \pi_1 \pi_0 w
\big) c \]

is equal to

\[ \big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{olive}{\omega_{\gamma_0} } \pi_1 \pi_0 , \
\hat{u}_4 \hat{u}_5 \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0
)c , \
\hat{u}_4 \hat{u}_5 \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0 ,\
\hat{u}_4 \hat{u}_5\tilde{u} \bar{u} p_1^2 \pi_1 \pi_0 w )c , \
\big) c\]

which, by the Ore condition, is equal to

\[\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{olive}{\omega_{\gamma_0} } \pi_1 \pi_0 , \
\hat{u}_4 \hat{u}_5 \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0
)c , \
\hat{u}_4 \hat{u}_5 \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w ,\
\hat{u}_4 \hat{u}_5 \tilde{u} \bar{u} p_0^2 \pi_0 \pi_1 )c , \
\big) c. \]

Associativity of composition and the zippering condition allow us to see this is equal to

\[\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{olive}{\omega_{\gamma_0} } \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \textcolor{orange}{\pi_0 \pi_1 \omega} \pi_0 \pi_0 , \
\hat{u}_4 \hat{u}_5 \tilde{u} \textcolor{orange}{\pi_0 \pi_1 u_0 \theta} \pi_0 \pi_0 w
)c ,\
\hat{u}_4 \hat{u}_5 \tilde{u} \bar{u} p_0^2 \pi_0 \pi_1 , \
\big) c\]

which is equal to

\[ \]

the Ore condition and associativity.

This follows from equality between the first and last lines in the following straightforward but tedious calculation. We repeatedly use associativity for internal composition in $\mC$ along with the definitions of the arrows and objects in Diagrams (<ref>), (<ref>), and <ref>) of Lemma <ref> in this calculation.

\begin{align*}
& \ \ \ \
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0w , \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_1 \pi_0 , \
\hat{u}_{4 ;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_0
)c , \\
& \ \ \ \
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_0 w
\big) c \\
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_1 \pi_0 , \
\hat{u}_{4;5}\textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0
)c ,\\
& \ \ \ \
(\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_0 w
\big) c \\
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0
)c ,\\
& \ \ \ \
(\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_1 w
\big) c \\
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0
)c ,\\
& \ \ \ \
\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_1 w
\big) c \\
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0
)c , \\
& \ \ \ \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_1 w )c
\big) c \\
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0
)c , \\
& \ \ \ \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \bar{u} p_1^2 \pi_1 \pi_0 w )c
\big) c \\
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w  , \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0
)c , \\
& \ \ \ \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w ,\
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_0 \pi_1 )c
\big) c \\
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0
)c , \\
& \ \ \ \
\hat{u}_{4;5}\tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w ,\
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_0 \pi_1 )c
\big) c \\
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w )c
& \ \ \ \
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_0 \pi_1
\big) c \\
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_0 \pi_0 , \
\hat{u}_{4 ;5} \tilde{u} \textcolor{orange}{\pi_0 \pi_1 \omega} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \textcolor{orange}{\pi_0 \pi_1 u_0 \theta} \pi_0 \pi_0 w
)c ,\\
& \ \ \ \
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_0 \pi_1
\big) c \\
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \textcolor{orange}{\pi_0 \pi_1 \omega} \pi_0 \pi_0 )c
, \\
& \ \ \ \
( \hat{u}_{4;5} \tilde{u} \textcolor{orange}{\pi_0 \pi_1 u_0 \theta} \pi_0 \pi_0 w ,\
\hat{u}_{4;5} \tilde{u} \bar{u} p_0 \pi_0 \pi_1 )c
\big) c \\
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \textcolor{orange}{\pi_0 \pi_1 \omega} \pi_0 \pi_0 )c
, \\
& \ \ \ \
( \hat{u}_{4;5} \tilde{u} \textcolor{orange}{\pi_0 \pi_1 u_0 \theta} \pi_1 \pi_0  ,\
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_0 w )c
\big) c \\
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \textcolor{orange}{\pi_0 \pi_1 \omega} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \textcolor{orange}{\pi_0 \pi_1 u_0 \theta} \pi_1 \pi_0 )c
& \ \ \ \
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_0 w
\big) c.
\end{align*}

uniquely determine the map $\textcolor{cyan}{\rho_0'}$, for which

\[ \textcolor{cyan}{\rho_0'} \pi_1 = \hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_0 \]

and $\textcolor{cyan}{\rho_0'} \pi_0 $ is the parallel pair with components

\[\textcolor{cyan}{\rho_0'} \pi_0 \pi_0 = (
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0w ,
\hat{u}_4 \textcolor{olive}{\omega_{\gamma_0} } \pi_1 \pi_0 ,
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 ,
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0 ,
\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_0
)c \]

\[\textcolor{cyan}{\rho_0'} \pi_0 \pi_1 = (
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w ,
\hat{u}_4 \textcolor{olive}{\omega_{\gamma_0} } \pi_0 \pi_0 ,
\hat{u}_{4;5} \tilde{u} \textcolor{orange}{\pi_0 \pi_1 \omega} \pi_0 \pi_0 ,
\hat{u}_{4;5} \tilde{u} \textcolor{orange}{\pi_0 \pi_1 u_0 \theta} \pi_1 \pi_0 )c . \]

This means that the first and last terms of the calculation above precisely says

\begin{align*}
(\textcolor{cyan} {\rho_0'} \pi_0 \pi_0 , \textcolor{cyan} {\rho_0'} \pi_1) c
&= (\textcolor{cyan} {\rho_0'} \pi_0 \pi_1 , \textcolor{cyan} {\rho_0'} \pi_1) c .
\end{align*}

The equation

\begin{align*}
(\textcolor{violet} {\rho_1'} \pi_0 \pi_0 , \textcolor{violet} {\rho_1'} \pi_1) c
&= (\textcolor{violet} {\rho_1'} \pi_0 \pi_1 , \textcolor{violet} {\rho_1'} \pi_1) c
\end{align*}

This follows from the first and last lines of the following computation which is saimilar to the one in Lemma <ref>:

\begin{align*}
&\ \ \ \
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0w , \
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_0
)c , \\
& \ \ \ \
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_0 w
\big) c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_1 \pi_0 , \
\hat{u}_{4;5}\textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0
)c ,\\
& \ \ \ \
(\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_0 w
\big) c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0
)c ,\\
& \ \ \ \
(\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_1 w
\big) c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0
)c ,\\
& \ \ \ \
\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_1 w
\big) c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0
)c , \\
& \ \ \ \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_1 w )c
\big) c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0
)c , \\
& \ \ \ \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \bar{u} p_1^2 \pi_1 \pi_0 w )c
\big) c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w  , \
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0
)c , \\
& \ \ \ \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w ,\
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_0 \pi_1 )c
\big) c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_1} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0
)c , \\
& \ \ \ \
\hat{u}_{4;5}\tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w ,\
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_0 \pi_1 )c
\big) c \\
\end{align*}

This calculation continues below, we just had to separate because it wouldn't fit on one page.

\begin{align*}
& \ \ \ \ \big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_1} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0
)c , \\
& \ \ \ \
\hat{u}_{4;5}\tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w ,\
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_0 \pi_1 )c
\big) c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_0 \pi_0 w )c
& \ \ \ \
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_0 \pi_1
\big) c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0 , \\
&\ \ \ \
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_0 \pi_0 w , \
\hat{u}_{4;5} \tilde{u} \bar{u} \pi_0 \pi_0 \pi_0 \pi_0
)c ,\\
& \ \ \ \
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_0 \pi_1
\big) c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_0 \pi_0 w
)c , \\
& \ \ \ \
(\hat{u}_{4;5} \tilde{u} \bar{u} \pi_0 \pi_0 \pi_0 \pi_0  ,
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_0 \pi_1
\big) c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_0 \pi_0 w
)c , \\
& \ \ \ \
\hat{u}_{4;5} \tilde{u} \bar{u} p_1^2 \pi_0 \pi_1
\big) c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0 )c
, \\
& \ \ \ \
( \hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_1 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \bar{u} p_1^2 \pi_1 \pi_0 w )c
\big) c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_1 \pi_0 )c
& \ \ \ \
\hat{u}_{4;5} \tilde{u} \bar{u} p_1^2 \pi_1 \pi_0 w
\big) c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_1 \pi_0 )c
&\ \ \ \
(\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_0 ,
\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_1 w
\big) c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0 , \\
& \ \ \ \
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_1 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_0
)c , \\
& \ \ \ \
\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_1 w
\big) c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0 , \\
& \ \ \ \
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_1 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_0
)c , \\
& \ \ \ \
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_0 w
\big) c.
\end{align*}

Unsurprisingly we get the same coequalizing arrow in $W$ for $\rho_1'$ as for $\rho_0'$

\[ \textcolor{violet}{\rho_1'} \pi_1 = \hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_0 \]

and the parallel pair $\textcolor{violet}{\rho_1'} \pi_0 $ is given by the pair of components

\[\textcolor{violet}{\rho_1'} \pi_0 \pi_0 = (
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0w , \
\hat{u}_4 \textcolor{brown}{\omega_{\gamma_1} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_0
)c \]

\begin{align*}
\textcolor{violet}{\rho_0'} \pi_0 \pi_1
& = (
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0 , \\
& \ \ \ \
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_1 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_0
\end{align*}

The first and last terms of the big equation above being equal then reduces to

\begin{align*}
(\textcolor{violet} {\rho_1'} \pi_0 \pi_0 , \textcolor{violet} {\rho_1'} \pi_1) c
&= (\textcolor{violet} {\rho_1'} \pi_0 \pi_1 , \textcolor{violet} {\rho_1'} \pi_1) c .
\end{align*}

There is a unique map $\textcolor{cyan}{\sigma_{0, \gamma}} : \hat{U} \to \spn $ determined by

\begin{align*}
\textcolor{cyan}{\sigma_{0, \gamma}} \pi_0
&= \textcolor{cyan}{\omega_{0, 0}} \pi_1 \\
\textcolor{cyan}{\sigma_{0, \gamma}} \pi_1
&= (
\textcolor{cyan}{\omega_0} , \
\hat{u}_{0;4} \textcolor{olive}{\theta_{\gamma_0} } \pi_0 \pi_0,\
\hat{u} \textcolor{orange}{\sigma_0} \pi_1
)c \\
&= (\textcolor{cyan}{\omega_0} , \
\hat{u}_{0;4} \textcolor{olive}{\theta_{\gamma_0} } \pi_1 \pi_0\ ,  \
\hat{u} \textcolor{purple}{\sigma_\gamma} \pi_1
\end{align*}

where $\textcolor{cyan}{\omega_0} : \hat{U} \to W_\circ$ is defined by

\[\textcolor{cyan}{\omega_0} = ( \textcolor{cyan}{\omega_{0,0}} \pi_0 \pi_0 , \
\hat{u}_0 \textcolor{cyan}{\omega_{0,1}} \pi_0 \pi_0, \
\hat{u}_{0;1} \textcolor{cyan}{\omega_{0,2}} \pi_1 ) c \]

First, by definition of $W_\circ$ we have

\[ \textcolor{cyan}{\omega_0} s = \textcolor{cyan}{\omega_{0,0}} \pi_0 \pi_0 s = \textcolor{cyan}{\omega_{0,0}} \pi_1 s =\]

showing that $\textcolor{cyan}{\omega_{0 , \gamma}} : \hat{U} \to \spn$ is well-defined. Now let $\textcolor{cyan}{\omega_{0}'}: \hat{U} \to \mC_1$ be defined by

\[\textcolor{cyan}{\omega_{0}'} = ( \textcolor{cyan}{\omega_{0,0}} \pi_0 \pi_0 ,\
\hat{u}_0 \textcolor{cyan}{\omega_{0,1}} \pi_0 \pi_0 , \
\hat{u}_{0;1} \textcolor{cyan}{\omega_{0,2}} \pi_0 \pi_0 )c . \]

By definition of $W_\circ$, $\textcolor{cyan}{\omega_0} $, and $\textcolor{cyan}{\omega_0'}$ we have

\begin{align}\label{appendix eq omega_0 for sigma_{0,gamma}}
\begin{split}
\textcolor{cyan}{\omega_0}
( \textcolor{cyan}{\omega_{0,0}} \pi_0 \pi_0 , \
\hat{u}_0 \textcolor{cyan}{\omega_{0,1}} \pi_0 \pi_0, \
\hat{u}_{0;1} \textcolor{cyan}{\omega_{0,2}} \pi_1 ) c\\
( \textcolor{cyan}{\omega_{0,0}} \pi_0 \pi_0 ,\
\hat{u}_0 \textcolor{cyan}{\omega_{0,1}} \pi_0 \pi_0, \
\hat{u}_{0;1} \textcolor{cyan}{\omega_{0,2}} \pi_0 \pi_0 , \
\hat{u}_{0;2} \textcolor{cyan}{\omega_{0,2}'}c ) c \\
( \textcolor{cyan}{\omega_{0,0}} \pi_0 \pi_0 ,\
\hat{u}_0 \textcolor{cyan}{\omega_{0,1}} \pi_0 \pi_0, \
\hat{u}_{0;1} \textcolor{cyan}{\omega_{0,2}} \pi_0 \pi_0 , \
\hat{u}_{0;2} \textcolor{cyan}{\delta_{\rho_0}} \pi_0 \iota_{eq} \pi_0 , \
\hat{u}_{0;3} \textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 ) c\\
\big( (\textcolor{cyan}{\omega_{0,0}} \pi_0 \pi_0 ,\
\hat{u}_0 \textcolor{cyan}{\omega_{0,1}} \pi_0 \pi_0, \
\hat{u}_{0;1} \textcolor{cyan}{\omega_{0,2}} \pi_0 \pi_0 , \
\hat{u}_{0;2} \textcolor{cyan}{\delta_{\rho_0}} \pi_0 \iota_{eq} \pi_0)c , \
\hat{u}_{0;3} \textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 \big) c\\
\big( \textcolor{cyan}{\omega_{0}'} , \
\hat{u}_{0;2} (\textcolor{cyan}{\delta_{\rho_0}} \pi_0 \iota_{eq} \pi_0 , \
\hat{u}_{3} \textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0)c \big) c
\end{split}
\end{align}

Notice that by definition of $\textcolor{orange}{\sigma_0}$ and $\textcolor{cyan} {\rho_0'} \pi_0 \pi_1$ and the refinement of covers $\bar{u} : \bar{U} \to \slb \tensor[_t]{\times}{_s} \slb$, we have

\begin{align}\label{appendix eq sigma_{0,gamma} side-calc sigma_0}
\begin{split}
& \ \ \ \ (\textcolor{cyan} {\rho_0'} \pi_0 \pi_1 ,  \hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_1 ) c \\
%&= (\textcolor{cyan} {\rho_0'} \pi_0 \pi_1 ,  \hat{u}_{4;5} \tilde{u} \pi_0 \pi_1 u \pi_1 \pi_1 ) c %\\
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w , \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_0 \pi_0,\
\hat{u}_{4;5} \tilde{u} \textcolor{orange}{\pi_0 \pi_1 \omega \pi_0 \pi_0} ,\
\hat{u}_{4 ;5} \tilde{u} \pi_0 \pi_1 u_0 \theta \pi_1 \pi_0
)c ,\\
&\ \ \ \
\hat{u}_{4;5} \tilde{u} \textcolor{orange}{\pi_0 \pi_1 u \pi_1 \pi_1 }
\big)c \\
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w, \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_0 \pi_0,\\
&\ \ \ \
\hat{u}_{4 ;5} \tilde{u} \textcolor{orange}{\pi_0 \pi_1 \omega \pi_0 \pi_0} ,\
\hat{u}_{4 ;5} \tilde{u} \textcolor{orange}{\pi_0 \pi_1 u_0 \theta \pi_1 \pi_0} ,\
\hat{u}_{4;5} \tilde{u} \pi_0 \pi_1 u \pi_1 \pi_1
\big)c \\
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w, \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_0 \pi_0,\
\hat{u}_{4;5} \textcolor{orange}{\sigma_0} \pi_1
\big)c
\end{split}
\end{align}

and similarly by definition of $\textcolor{purple}{\sigma_\gamma}$ and $\textcolor{cyan}{\rho_0'} \pi_0 \pi_0$

\begin{align}\label{appendix eq sigma_{0,gamma} side-calc sigma_gamma}
\begin{split}
& \ \ \ \ (\textcolor{cyan} {\rho_0'} \pi_0 \pi_0 , \hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0 )c \\
%\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_1 ) c \\
%&= ( \textcolor{cyan}{\rho_0'} \pi_0 \pi_0 , \hat{u}_{4;5} \tilde{u} \pi_0 \pi_1 u \pi_1 \pi_1 ) %c \\
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0w, \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_1 \pi_0\ ,  \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0, \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_0
)c , \\
&\ \ \ \
\hat{u}_{4;5} \tilde{u} \pi_0 \pi_1 u \pi_1 \pi_1
\big) c \\
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0w, \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_1 \pi_0\ ,  \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0, \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0
)c , \\
&\ \ \ \
(\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \pi_0 \pi_1 u \pi_1 \pi_1 )c
\big) c \\
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0w, \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_1 \pi_0\ ,  \
\hat{u}_{4 ;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0, \
\hat{u}_{4 ;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0
)c , \\
&\ \ \ \
\hat{u}_{4;5} \tilde{u} \bar{u} p_1 \pi_1 \pi_1
\big) c \\
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0w, \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_1 \pi_0\ ,  \\
&\ \ \ \
\hat{u}_{4 ;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0, \
\hat{u}_{4 ;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0
, \
\hat{u}_{4;5} \tilde{u} \bar{u} p_1 \pi_1 \pi_1
\big) c \\
\big(
\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0w, \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_1 \pi_0\ ,  \
\hat{u}_{4 ;5} \textcolor{purple}{\sigma_\gamma} \pi_1
\big) c .
\end{split}
\end{align}

Also notice since $\cP(\mC)$ is a pullback of $\cP_{eq}(\mC)$ and $\cP_{cq}(\mC)$ over the object of parallel pairs in $\mC$, $P(\mC)$, we have

\begin{align*}
\textcolor{cyan} {\delta_{\rho_0}} \pi_0 \iota_{eq} \pi_1
&= \textcolor{cyan} {\delta_{\rho_0}} \pi_1 \iota_{ceq} \pi_0\\
&= \hat{u}_3 \textcolor{cyan} {\rho_0} \iota_{ceq} \pi_0\\
&= \hat{u}_3 \textcolor{cyan} {\rho_0'} \pi_0
\end{align*}

and then by definition of $\cP_{eq}(\mC)$ the composable pairs

\begin{align*}
\textcolor{cyan} {\delta_{\rho_0}} \pi_0 \iota_{eq} (\pi_0 , \pi_1 \pi_0)
(\textcolor{cyan} {\delta_{\rho_0}} \pi_0 \iota_{eq} \pi_0 ,
\textcolor{cyan} {\delta_{\rho_0}} \pi_0 \iota_{eq} \pi_1 \pi_0 )
(\textcolor{cyan} {\delta_{\rho_0}} \pi_0 \iota_{eq} \pi_0,
\hat{u}_3 \textcolor{cyan} {\rho_0'} \pi_0 \pi_0 )
\end{align*}

\begin{align*}
\textcolor{cyan} {\delta_{\rho_0}} \pi_0 \iota_{eq} (\pi_0 , \pi_1 \pi_1)
(\textcolor{cyan} {\delta_{\rho_0}} \pi_0 \iota_{eq} \pi_0 ,
\textcolor{cyan} {\delta_{\rho_0}} \pi_0 \iota_{eq} \pi_1 \pi_1 )
= (\textcolor{cyan} {\delta_{\rho_0}} \pi_0 \iota_{eq} \pi_0,
\hat{u}_3 \textcolor{cyan} {\rho_0'} \pi_0 \pi_1 )
\end{align*}

are equal after post-composing with the composition structure map in $\mC$, $c : mC_2 \to \mC_1$:

\begin{align}\label{appendix eq final helper lemma for sigma_{0,gamma}}
(\textcolor{cyan} {\delta_{\rho_0}} \pi_0 \iota_{eq} \pi_0,
\hat{u}_3 \textcolor{cyan} {\rho_0'} \pi_0 \pi_0 ) c = (\textcolor{cyan} {\delta_{\rho_0}} \pi_0 \iota_{eq} \pi_0,
\hat{u}_3 \textcolor{cyan} {\rho_0'} \pi_0 \pi_1 ) c
\end{align}

Associativity of composition and equations ($\ref{appendix eq omega_0 for sigma_{0,gamma}} $); (<ref>); (<ref>); and (<ref>), allow us to see

\begin{align*}
\textcolor{cyan}{\omega_0} , \
\hat{u}_{0;4} \textcolor{olive}{\theta_{\gamma_0} } \pi_0 \pi_0,\
\hat{u} \textcolor{orange}{\sigma_0} \pi_1
\big(
\textcolor{cyan}{\omega_0'} , \
\hat{u}_{0;2} \textcolor{cyan}{\delta_{\rho_0}} \pi_0 \iota_{eq} \pi_0 , \\
&\ \ \ \
\hat{u}_{0;3} (\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w, \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_0 \pi_0,\
\hat{u}_{4;5} \textcolor{orange}{\sigma_0} \pi_1 )c \big) c\\
\big(
\textcolor{cyan}{\omega_0'} , \
\hat{u}_{0;2} \textcolor{cyan}{\delta_{\rho_0}} \pi_0 \iota_{eq} \pi_0 , \\
&\ \ \ \
\hat{u}_{0;3} (\textcolor{cyan} {\rho_0'} \pi_0 \pi_1 ,\
\hat{u}_{4;5} \tilde{u} \pi_0 \pi_1 u \pi_1 \pi_1 ) c
)c \\
\big(
\textcolor{cyan}{\omega_0'} , \
\hat{u}_{0;2} (\textcolor{cyan}{\delta_{\rho_0}} \pi_0 \iota_{eq} \pi_0 , \
\hat{u}_{3} \textcolor{cyan} {\rho_0'} \pi_0 \pi_1)c , \\
&\ \ \ \
\hat{u}_{0;5} \tilde{u} \pi_0 \pi_1 u \pi_1 \pi_1
\big)c \\
\big(
\textcolor{cyan}{\omega_0'} , \
\hat{u}_{0;2} (\textcolor{cyan} {\delta_{\rho_0}} \pi_0 \iota_{eq} \pi_0 , \
\hat{u}_3 \textcolor{cyan} {\rho_0'} \pi_0 \pi_0 )c , \\
&\ \ \ \
\hat{u}_{0;5} \tilde{u} \pi_0 \pi_1 u \pi_1 \pi_1
\big)c \\
\big(
(\textcolor{cyan}{\omega_0'} , \
\hat{u}_{0;2} \textcolor{cyan} {\delta_{\rho_0}} \pi_0 \iota_{eq} \pi_0)c , \\
&\ \ \ \
\hat{u}_{0;3} (\textcolor{cyan} {\rho_0'} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u} \pi_0 \pi_1 u \pi_1 \pi_1 )c
\big)c \\
\big(
(\textcolor{cyan}{\omega_0'} , \
\hat{u}_{0;2} \textcolor{cyan}{\delta_{\rho_0}} \pi_0 \iota_{eq} \pi_0) c , \\
&\ \ \ \
\hat{u}_{0;3} (\textcolor{cyan}{\delta_{\lambda_0}} \pi_0 \iota_{eq} \pi_0 w, \
\hat{u}_4 \textcolor{olive}{\theta_{\gamma_0} } \pi_1 \pi_0,\
\hat{u}_{4;5} \textcolor{purple}{\sigma_\gamma} \pi_1 )c \big) c\\
&=(\textcolor{cyan}{\omega_0} , \
\hat{u}_{0;4} \textcolor{olive}{\theta_{\gamma_0} } \pi_1 \pi_0\ ,  \
\hat{u} \textcolor{purple}{\sigma_\gamma} \pi_1
\end{align*}

There is a unique map $\textcolor{violet}{\sigma_{1 , \gamma}} : \hat{U} \to \spn $ determined by

\begin{align*}
\textcolor{violet}{\sigma_{1 , \gamma}} \pi_0
&= \textcolor{violet}{\omega_{1,0}} \pi_1 \\
\textcolor{violet}{\sigma_{1, \gamma}} \pi_1
&= ( \textcolor{violet}{\omega_1} ,\
\hat{u}_{0;4} \textcolor{brown}{\omega_{\gamma_1} } \pi_0 \pi_0 ,\
\hat{u} \textcolor{teal}{\sigma_1}\pi_1 )c \\
\big(
\textcolor{violet}{\omega_{1}} , \
\hat{u}_{0;4} \textcolor{brown}{\omega_{\gamma_1} } \pi_1 \pi_0 , \
\hat{u}\textcolor{purple}{\sigma_\gamma} \pi_1
\big)c
\end{align*}

where $\textcolor{violet}{\omega_1} : \hat{U} \to W_\circ$ is defined by

\[\textcolor{violet}{\omega_1} = ( \textcolor{violet}{\omega_{1,0}} \pi_0 \pi_0 , \
\hat{u}_0 \textcolor{violet}{\omega_{1,1}} \pi_0 \pi_0, \
\hat{u}_{0;1} \textcolor{violet}{\omega_{1,2}} \pi_1 ) c \]

Similarly define

\[ \textcolor{violet}{\omega_{1}'} = (\textcolor{violet}{\omega_{1,0}} \pi_0 \pi_0  , \
\hat{u}_0 \textcolor{violet}{\omega_{1,1}} \pi_0 \pi_0 ,\
\hat{u}_{0;1} \textcolor{violet}{\omega_{1,2}} \pi_0 \pi_0)c \]

and we have:

\begin{align*}
\textcolor{violet}{\omega_1}
&= ( \textcolor{violet}{\omega_{1,0}} \pi_0 \pi_0 , \
\hat{u}_0 \textcolor{violet}{\omega_{1,1}} \pi_0 \pi_0, \
\hat{u}_{0;1} \textcolor{violet}{\omega_{1,2}} \pi_1 ) c \\
( \textcolor{violet}{\omega_{1,0}} \pi_0 \pi_0  , \
\hat{u}_0 \textcolor{violet}{\omega_{1,1}} \pi_0 \pi_0 ,\
\hat{u}_{0;1} \textcolor{violet}{\omega_{1,2}} \pi_0 \pi_0 ,\
\hat{u}_{0;2} \textcolor{violet}{\delta_{\rho_1}} \pi_0 \iota_{eq} \pi_0 ,\
\hat{u}_{0;3} \textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 ) c\\
\big( \textcolor{violet}{\omega_{1}'} ,\
\hat{u}_{0;2} (\textcolor{violet}{\delta_{\rho_1}} \pi_0 \iota_{eq} \pi_0 ,\
\hat{u}_{3} \textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 ) c \big)c.
\end{align*}

By definition of $\sigma_1$ and $\rho_1'$$\pi_0 \pi_1 $:

\begin{align}\label{appendix eq sigma_{1,gamma} side-calc sigma_1}
\begin{split}
& \ \ \ \ ( \textcolor{violet}{\rho_1'} \pi_0 \pi_1 ,
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_1)c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w ,\
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_0 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_1 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_0
)c ,\\
& \ \ \ \
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_1
\big) c\\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w ,\
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_0 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_1 \pi_0 ,\\
& \ \ \ \
(\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_1 )c
\big) c\\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w ,\
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_0 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_1 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \bar{u} p_1^2 \pi_1 \pi_1
\big) c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w ,\
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_0 \pi_0 ,\\
& \ \ \ \
\hat{u}_{4;5} (\tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0 ,\
\tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_1 \pi_0 ,\
\tilde{u} \pi_1 \pi_0 p_1^2 \pi_1 \pi_1 )c
\big) c \\
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w ,\
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_0 \pi_0 ,\\
& \ \ \ \
\hat{u}_{4;5} (\tilde{u} \textcolor{teal}{\pi_1 \pi_1 \omega} \pi_0 \pi_0 ,\
\tilde{u} \textcolor{teal}{\pi_1 \pi_1 u_0 \theta} \pi_1 \pi_0 ,\
\tilde{u} \pi_1 \pi_1 u \pi_1 \pi_1 )c
\big) c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 w ,\
\hat{u}_4 \textcolor{brown}{\theta_{\gamma_1} } \pi_0 \pi_0 ,\
\hat{u}_{4;5} \textcolor{teal}{\sigma_1}\pi_1
\big) c
\end{split}
\end{align}

Similarly by definition of $\textcolor{purple}{\sigma_\gamma}$ and $\textcolor{violet}{\rho_1'} \pi_0 \pi_0$:

\begin{align}\label{appendix eq sigma_{1,gamma} side-calc sigma_gamma}
\begin{split}
& \ \ \ \ ( \textcolor{violet}{\rho_1'} \pi_0 \pi_0 , \hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_1) c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0w , \
\hat{u}_4 \textcolor{brown}{\omega_{\gamma_1} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_0
)c ,\\
& \ \ \ \
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_1
\big)c\\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0w , \
\hat{u}_4 \textcolor{brown}{\omega_{\gamma_1} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0 ,\\
& \ \ \ \
(\hat{u}_{4;5} \tilde{u} \bar{u} \pi_1 \pi_0 \pi_0 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_1 )c
\big)c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0w , \
\hat{u}_4 \textcolor{brown}{\omega_{\gamma_1} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 , \
\hat{u}_{4;5} \tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0 ,\
\hat{u}_{4;5} \tilde{u} \bar{u} p_1^2 \pi_1 \pi_1
\big)c\\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0w , \
\hat{u}_4 \textcolor{brown}{\omega_{\gamma_1} } \pi_1 \pi_0 , \\
& \ \ \ \
\hat{u}_{4;5} (\textcolor{purple}{\omega_\gamma} \pi_0 \pi_0 , \
\tilde{u}' \textcolor{purple}{\theta_\gamma} \pi_1 \pi_0 ,\
\tilde{u} \bar{u} p_1^2 \pi_1 \pi_1)c
\big)c \\
\big(
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0w , \
\hat{u}_4 \textcolor{brown}{\omega_{\gamma_1} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\sigma_\gamma} \pi_1
\big)c
\end{split}
\end{align}

Since $\cP(\mC)$ is a pullback of $\cP_{eq}(\mC)$ and $\cP_{cq}(\mC)$ over the object of parallel pairs in $\mC$, $P(\mC)$,

\begin{align*}
\textcolor{violet}{\delta_{\rho_1}} \pi_0 \iota_{eq} \pi_0
&= \textcolor{violet}{\delta_{\rho_1}} \pi_1 \iota_{ceq} \pi_0\\
&= \hat{u}_3 \textcolor{violet}{\rho_1} \iota_{ceq} \pi_0 \\
&= \hat{u}_3 \textcolor{violet}{\rho_1'} \pi_0
\end{align*}

By definition of $\cP_{eq}(\mC)$ the composable pairs

\begin{align*}
\textcolor{violet} {\delta_{\rho_1}} \pi_0 \iota_{eq} (\pi_0 , \pi_1 \pi_0)
(\textcolor{violet} {\delta_{\rho_1}} \pi_0 \iota_{eq} \pi_0 ,
\textcolor{violet} {\delta_{\rho_1}} \pi_0 \iota_{eq} \pi_1 \pi_0 )
(\textcolor{violet} {\delta_{\rho_1}} \pi_0 \iota_{eq} \pi_0,
\hat{u}_3 \textcolor{violet} {\rho_1'} \pi_0 \pi_0 )
\end{align*}

\begin{align*}
\textcolor{violet} {\delta_{\rho_1}} \pi_0 \iota_{eq} (\pi_0 , \pi_1 \pi_1)
(\textcolor{violet} {\delta_{\rho_1}} \pi_0 \iota_{eq} \pi_0 ,
\textcolor{violet} {\delta_{\rho_1}} \pi_0 \iota_{eq} \pi_1 \pi_1 )
= (\textcolor{violet} {\delta_{\rho_1}} \pi_0 \iota_{eq} \pi_0,
\hat{u}_3 \textcolor{violet} {\rho_1'} \pi_0 \pi_1 ) .
\end{align*}

are coequalized (in $\cE$) by the composition structure map of $\mC$. This implies

\begin{align}\label{appendix eq final helper lemma for sigma_{1,gamma}}
\begin{split}
(\textcolor{violet} {\delta_{\rho_1}} \pi_0 \iota_{eq} \pi_0,
\hat{u}_3 \textcolor{violet} {\rho_1'} \pi_0 \pi_0 ) c = (\textcolor{violet} {\delta_{\rho_1}} \pi_0 \iota_{eq} \pi_0,
\hat{u}_3 \textcolor{violet} {\rho_1'} \pi_0 \pi_1 ) c
\end{split}
\end{align}

Now the span

\[ \textcolor{violet}{\sigma_{1 , \gamma}} = (\textcolor{violet}{\omega_{0,1}} \pi_1 ,\ \textcolor{violet}{\sigma_{1,\gamma}} \pi_1) \]

is well-defined because

\[ \textcolor{violet}{\omega_{1,0}} \pi_1 w s = \textcolor{violet}{\omega_{1,0}} \pi_0 \pi_0 s \]

where the right leg, $\textcolor{violet}{\sigma_{1,\gamma}} \pi_1$, is given by the composite

\begin{align*}
( \textcolor{violet}{\omega_1} ,\
\hat{u}_{0;4} \textcolor{brown}{\omega_{\gamma_1} } \pi_0 \pi_0 ,\
\hat{u} \textcolor{teal}{\sigma_1}\pi_1 )c
\big(
\textcolor{violet}{\omega_{1}'} ,\
\hat{u}_{0;2} \textcolor{violet}{\delta_{\rho_1}} \pi_0 \iota_{eq} \pi_0 ,\\
& \ \ \ \
\hat{u}_{0;3} (\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0 ,\
\hat{u}_{4} \textcolor{brown}{\omega_{\gamma_1} } \pi_0 \pi_0 ,\
\hat{u}_{4;5} \textcolor{teal}{\sigma_1}\pi_1)c \big)c \\
\big(
\textcolor{violet}{\omega_{1}'} ,\
\hat{u}_{0;2} \textcolor{violet}{\delta_{\rho_1}} \pi_0 \iota_{eq} \pi_0 ,\\
& \ \ \ \
\hat{u}_{0;3} ( \textcolor{violet}{\rho_1'} \pi_0 \pi_1,\
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_1)c
\big)c\\
\big(
\textcolor{violet}{\omega_{1}'} ,\\
& \ \ \ \
\hat{u}_{0;2} (\textcolor{violet}{\delta_{\rho_1}} \pi_0 \iota_{eq} \pi_0 ,\
\hat{u}_3 \textcolor{violet}{\rho_1'} \pi_0 \pi_1)c ,\\
& \ \ \ \
\hat{u}_{0;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_1
\big)c\\
\big(
\textcolor{violet}{\omega_{1}'} ,\\
& \ \ \ \
\hat{u}_{0;2} (\textcolor{violet}{\delta_{\rho_1}} \pi_0 \iota_{eq} \pi_0 ,\
\hat{u}_3 \textcolor{violet}{\rho_1'} \pi_0 \pi_0)c ,\\
& \ \ \ \
\hat{u}_{0;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_1
\big)c\\
\big(
\textcolor{violet}{\omega_{1}'} ,\
\hat{u}_{0;2} \textcolor{violet}{\delta_{\rho_1}} \pi_0 \iota_{eq} \pi_0 ,\\
& \ \ \ \
\hat{u}_{0;3} (\textcolor{violet}{\rho_1'} \pi_0 \pi_0,\
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_1 )c
\big)c\\
\big(
\textcolor{violet}{\omega_{1}'} ,\
\hat{u}_{0;2} \textcolor{violet}{\delta_{\rho_1}} \pi_0 \iota_{eq} \pi_0 ,\\
& \ \ \ \
\hat{u}_{0;3} (\textcolor{violet}{\rho_1'} \pi_0 \pi_0,\
\hat{u}_{4;5} \tilde{u} \bar{u} p_0^2 \pi_1 \pi_1 )c
\big)c\\
\big(
\textcolor{violet}{\omega_{1}'} ,\
\hat{u}_{0;2} \textcolor{violet}{\delta_{\rho_1}} \pi_0 \iota_{eq} \pi_0 ,\\
& \ \ \ \
\hat{u}_{0;3} (
\textcolor{violet}{\delta_{\lambda_1}} \pi_0 \iota_{eq} \pi_0w , \
\hat{u}_4 \textcolor{brown}{\omega_{\gamma_1} } \pi_1 \pi_0 , \
\hat{u}_{4;5} \textcolor{purple}{\sigma_\gamma} \pi_1)c
\big)c\\
\big(
\textcolor{violet}{\omega_{1}} , \
\hat{u}_{0;4} \textcolor{brown}{\omega_{\gamma_1} } \pi_1 \pi_0 , \
\hat{u}\textcolor{purple}{\sigma_\gamma} \pi_1
\big)c\\
\end{align*}

There exists a sailboat $\varphi_0 : \hat{U} \to \slb$, uniquely determined by the pairing map

\begin{align*}
\varphi_0
\big(
\mu_0 , \
\hat{u} \textcolor{orange}{\sigma_0} \pi_0
) , \
\textcolor{cyan}{\omega_{0,0}} \pi_1
) , \
\hat{u} \textcolor{orange}{\sigma_0} \pi_1
\big)
\end{align*}

\[ \mu_0 =(\textcolor{cyan}{\omega_0} ,\
\hat{u}_{0;4} \textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0

such that

\begin{align*}
\varphi_0 p_0 &= \hat{u} \textcolor{orange}{\sigma_0} \\
\varphi_0 p_1 &= \textcolor{cyan}{\sigma_{0,\gamma}} .
\end{align*}

Recall that $\slb = W_\triangle \tensor[_{\pi_0 \pi_0 \pi_1 s}]{\times}{_s} \mC_1$, where $W_\triangle = (\mC_1 \tensor[_t]{\times}{_{ws}} W) \tensor[_c]{\times}{_w} W$ so to see $\varphi_0 : \hat{U} \to \slb$ is well-defined we need to show that

\[ (
\mu_0 , \
\hat{u} \textcolor{orange}{\sigma_0} \pi_0
) , \
\textcolor{cyan}{\omega_{0,0}} \pi_1
) : \hat{U} \to W_\triangle \]

is well-defined and that

\[ \hat{u} \textcolor{orange}{\sigma_0} \pi_1 s = \mu_0 t = \hat{u} \textcolor{orange}{\sigma_0} \pi_0 s.\]

By definition of $\mu_0$ and the lift $\textcolor{olive}{\theta_{\gamma_0}} : \hat{U}_5 \to W_\square$ we have

\begin{align*}
\mu_0 t
= \hat{u}_{0;4} \textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0 w t
= \hat{u} \textcolor{orange}{\sigma_0} \pi_0 w s
= \hat{u} \textcolor{orange}{\sigma_0} \pi_1 s
\end{align*}

showing that $(\mu_0 , \hat{u} \textcolor{orange}{\sigma_0} \pi_0) : \hat{U} \to \mC_1 \tensor[_t]{\times}{_{ws}} W$ are composable with respect to the internal composition structure of $\mC$ (after appliying $w : W \to \mC_1$ in the right-hand component) and that $\hat{u} \textcolor{orange}{\sigma_0} \pi_1$ is well-defined in the right-most component. It remains to see that the $\varphi_0 p_0 : \hat{U} \to W_\triangle$ is well-defined. For this we use the definitions of $\mu_0$ and the lifts in Diagrams (<ref>) and (<ref>) along with associativity of composition in $\mC$ to compute

\begin{align*}
\mu_0 , \
\hat{u} \textcolor{orange}{\sigma_0} \pi_0
) , \
\textcolor{cyan}{\omega_{0,0}} \pi_1
) \pi_1
&= \textcolor{cyan}{\omega_{0,0}} \pi_1 \\
&= (\textcolor{cyan}{\omega_{0,0}} \pi_0 \pi_0 , \textcolor{cyan}{\omega_{0,0}} \pi_0 \pi_1 , \textcolor{cyan}{\omega_{0,0}} \pi_0 \pi_2 ) c \\
&= (\textcolor{cyan}{\omega_{0,0}} \pi_0 \pi_0 , \hat{u}_0 \textcolor{cyan}{\omega_{0,1}} \pi_1 , \hat{u} \textcolor{orange}{\sigma_0} \pi_0) c \\
&= \big(\textcolor{cyan}{\omega_{0,0}} \pi_0 \pi_0 , \\
& \ \ \ \
\hat{u}_0 (\textcolor{cyan}{\omega_{0,1}} \pi_0 \pi_0 ,
\textcolor{cyan}{\omega_{0,1}} \pi_0 \pi_1 ,
\textcolor{cyan}{\omega_{0,1}} \pi_0 \pi_2 ) c , \\
& \ \ \ \  \hat{u} \textcolor{orange}{\sigma_0} \pi_0 \big) c \\
&= \big(\textcolor{cyan}{\omega_{0,0}} \pi_0 \pi_0 , \
\hat{u}_0 \textcolor{cyan}{\omega_{0,1}} \pi_0 \pi_0 , \
\hat{u}_0 \textcolor{cyan}{\omega_{0,1}} \pi_0 \pi_1 ,\
\hat{u}_0\textcolor{cyan}{\omega_{0,1}} \pi_0 \pi_2 , \
\hat{u} \textcolor{orange}{\sigma_0} \pi_0 \big) c \\
&= \big(\textcolor{cyan}{\omega_{0,0}} \pi_0 \pi_0 , \
\hat{u}_0 \textcolor{cyan}{\omega_{0,1}} \pi_0 \pi_0 , \
\hat{u}_{0;1} \textcolor{cyan}{\omega_{0,2}} \pi_1 ,\
\hat{u}_{0;4} \textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0 , \
\hat{u} \textcolor{orange}{\sigma_0} \pi_0 \big) c \\
&= \big(
(\textcolor{cyan}{\omega_{0,0}} \pi_0 \pi_0 , \
\hat{u}_0 \textcolor{cyan}{\omega_{0,1}} \pi_0 \pi_0 , \
\hat{u}_{0;1} \textcolor{cyan}{\omega_{0,2}} \pi_1
)c ,\\
& \ \ \ \
\hat{u}_{0;4} \textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0 , \
\hat{u} \textcolor{orange}{\sigma_0} \pi_0 \big) c \\
&= \big( \textcolor{cyan}{\omega_0} ,\
\hat{u}_{0;4} \textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0 , \
\hat{u} \textcolor{orange}{\sigma_0} \pi_0 \big) c \\
&= \big( (\textcolor{cyan}{\omega_0} ,\
\hat{u}_{0;4} \textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0
)c, \
\hat{u} \textcolor{orange}{\sigma_0} \pi_0 \big) c \\
&= ( \mu_0 , \hat{u} \textcolor{orange}{\sigma_0} \pi_0)c\\
&= (
\mu_0 , \
\hat{u} \textcolor{orange}{\sigma_0} \pi_0
) , \
\textcolor{cyan}{\omega_{0,0}} \pi_1
) (\pi_0 \pi_0 , \pi_0 \pi_1) c.
\end{align*}

This gives that

\[ \varphi_0 p_0 = (
\mu_0 , \
\hat{u} \textcolor{orange}{\sigma_0} \pi_0
) , \
\textcolor{cyan}{\omega_{0,0}} \pi_1
) : \hat{U} \to W_\triangle \]

is well-defined. Similar techniques allow us to see

\begin{align*}
( \mu_0 , \hat{u} \textcolor{orange}{\sigma_0} \pi_1)c
&= \big( (\textcolor{cyan}{\omega_0} ,\
\hat{u}_{0;4} \textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0
)c, \
\hat{u} \textcolor{orange}{\sigma_0} \pi_1 \big)c \\
&= (\textcolor{cyan}{\omega_0} ,\
\hat{u}_{0;4} \textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0 ,\
\hat{u} \textcolor{orange}{\sigma_0} \pi_1)c \\
&= \textcolor{cyan}{\sigma_{0,\gamma}} \pi_1 .
\end{align*}

which shows

\begin{align*}
\varphi_0 p_0
&= \varphi_0 (\pi_0 \pi_0 \pi_1 , \pi_1)
& \varphi_0 p_1
&= \varphi_0 \big( \pi_0 \pi_1 , ( \pi_0 \pi_0 \pi_0 , \pi_1)c \big) \\
&= (\hat{u} \textcolor{orange}{\sigma_0} \pi_0 , \hat{u} \textcolor{orange}{\sigma_0} \pi_1)
&= \big( \textcolor{cyan}{\omega_{0,0}} \pi_1 , (\mu_0 , \hat{u} \textcolor{orange}{\sigma_0} \pi_1) c \big) \\
&= \hat{u} \textcolor{orange}{\sigma_0}
&= ( \textcolor{cyan}{\omega_{0,0}} \pi_1 , \textcolor{cyan}{\sigma_{0,\gamma}} \pi_1 )\\
&= \textcolor{cyan}{\sigma_{0,\gamma}} .
\end{align*}

There exists a sailboat $\varphi_{0,\gamma} : \hat{U} \to \slb$, uniquely determined by the pairing map

\begin{align*}
\varphi_{0 , \gamma} =
\big(
( \mu_{0, \gamma} , \
\hat{u} \textcolor{purple}{\sigma_\gamma} \pi_0
) , \
\textcolor{cyan}{\omega_{0,0}} \pi_1 ) , \
\hat{u} \textcolor{purple}{\sigma_\gamma} \pi_1
\big)
\end{align*}

\[ \mu_{0, \gamma} = (\textcolor{cyan}{\omega_0} ,\
\hat{u}_{0;4} \textcolor{olive}{\theta_{\gamma_0}} \pi_1 \pi_0 )c \]

such that

\begin{align*}
\varphi_{0,\gamma} p_0 &= \hat{u} \textcolor{purple}{\sigma_\gamma} \\
\varphi_{0,\gamma} p_1 &= \textcolor{cyan}{\sigma_{0,\gamma}}
\end{align*}

First note that the components of the pairing map defining $\varphi_{0, \gamma} : \hat{U} \to \slb$ are appropriately composable with respect to the internal composition structure of $\mC$:

\begin{align*}
\mu_{0, \gamma} t
= \hat{u}_{0;4} \textcolor{olive}{\theta_{\gamma_0}} \pi_1 \pi_0 t
= \hat{u} \textcolor{purple}{\sigma_\gamma} \pi_0 w s
= \hat{u} \textcolor{purple}{\sigma_\gamma} \pi_1 s.
\end{align*}

By Definition of $\mu_{0, \gamma}$ and the lifts, $\textcolor{cyan}{\omega_{0,0}} : \hat{U} \to W_\circ$ and $\textcolor{olive}{\theta_{\gamma_0}} : \hat{U}_5 \to W_\square$, we have

\begin{align*}
\textcolor{cyan}{\omega_{0,0}} \pi_1
&= \big( \textcolor{cyan}{\omega_0} ,\
\hat{u}_{0;4} \textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0 w , \
\hat{u} \textcolor{orange}{\sigma_0} \pi_0 w \big) c \\
&= \big( \textcolor{cyan}{\omega_0} ,\
(\hat{u}_{0;4} \textcolor{olive}{\theta_{\gamma_0}} \pi_0 \pi_0 w, \
\hat{u} \textcolor{orange}{\sigma_0} \pi_0 w)c \big) c \\
&= \big( \textcolor{cyan}{\omega_0} ,\
(\hat{u}_{0;4} \textcolor{olive}{\theta_{\gamma_0}} \pi_1 \pi_0 , \
\hat{u} \textcolor{purple}{\sigma_\gamma} \pi_0 w)c \big) c \\
&= \big( (\textcolor{cyan}{\omega_0} ,\
\hat{u}_{0;4} \textcolor{olive}{\theta_{\gamma_0}} \pi_1 \pi_0 )c , \
\hat{u} \textcolor{purple}{\sigma_\gamma} \pi_0 w \big) c \\
&= (\mu_{0, \gamma} , \hat{u} \textcolor{purple}{\sigma_\gamma} \pi_0 w)c .
\end{align*}

showing that the map

\[ \varphi_{0,\gamma} \pi_0 = (
( \mu_{0, \gamma} , \
\hat{u} \textcolor{purple}{\sigma_\gamma} \pi_0
) , \
\textcolor{cyan}{\omega_{0,0}} \pi_1 )
: \hat{U} \to W_\triangle\]

is well-defined. Then by associativity of composition in $\mC$ and the definitions of $\mu_{0,\gamma}$ and $\textcolor{cyan}{\sigma_{0,\gamma}}$ we get

\begin{align*}
( \mu_{0, \gamma} , \hat{u} \textcolor{purple}{\sigma_\gamma} \pi_1 ) c
&= \big( (\textcolor{cyan}{\omega_0} ,\
\hat{u}_{0;4} \textcolor{olive}{\theta_{\gamma_0}} \pi_1 \pi_0 )c , \
\hat{u} \textcolor{purple}{\sigma_\gamma} \pi_1 \big) c\\
&= \big( \textcolor{cyan}{\omega_0} ,\
\hat{u}_{0;4} \textcolor{olive}{\theta_{\gamma_0}} \pi_1 \pi_0 , \
\hat{u} \textcolor{purple}{\sigma_\gamma} \pi_1 \big) c \\
&= \textcolor{cyan}{\sigma_{0,\gamma}} \pi_1 .
\end{align*}

The previous equation implies the unique pairing, $\hat{U} \to \slb$, given by

\[ \varphi_{0 , \gamma} =
\big(
( \mu_{0, \gamma} , \
\hat{u} \textcolor{purple}{\sigma_\gamma} \pi_0
) , \
\textcolor{cyan}{\omega_{0,0}} \pi_1 ) , \
\hat{u} \textcolor{purple}{\sigma_\gamma} \pi_1
\big)
\]

is well-defined. From here it is straightforward to calculate

\begin{align*}
\varphi_{0,\gamma} p_0
&= \varphi_{0 , \gamma} (\pi_0 \pi_0 \pi_1, \pi_1)
& \varphi_{0,\gamma} p_1
&=\varphi_{0 , \gamma} \big( \pi_0 \pi_1 , (\pi_0 \pi_0 \pi_0 , \pi_1)c \big) \\
&= (\hat{u} \textcolor{purple}{\sigma_\gamma} \pi_0 , \hat{u} \textcolor{purple}{\sigma_\gamma} \pi_1 )
&= \big( \textcolor{cyan}{\omega_{0,0}} \pi_1 ,
( \mu_{0, \gamma} , \hat{u} \textcolor{purple}{\sigma_\gamma} \pi_1 ) c \big)\\
&= \hat{u} \textcolor{purple}{\sigma_\gamma}
&=(\textcolor{cyan}{\omega_{0,0}} \pi_1 , \textcolor{cyan}{\sigma_{0,\gamma}} \pi_1 )\\
&&&= \textcolor{cyan}{\sigma_{0,\gamma}}.
\end{align*}

The sailboat, $\varphi_1 : \hat{U} \to \slb$, defined by

\begin{align*}
\varphi_1
\big(
\mu_1 , \
\hat{u} \textcolor{teal}{\sigma_1} \pi_0
) , \
\textcolor{violet}{\omega_{1,0}} \pi_1
) , \
\hat{u} \textcolor{teal}{\sigma_1} \pi_1
\big)
\end{align*}

\[ \mu_1 = (\textcolor{violet}{\omega_1} , \hat{u}_{0;4}\textcolor{brown}{\gamma_1} \pi_0 \pi_0) c \]

is well-defined and relates the spans $\textcolor{teal}{\sigma_1}, \textcolor{violet}{\sigma_{1,\gamma}} : \hat{U} \to \spn$ in the sense that

\begin{align*}
\varphi_1 p_0 &= \hat{u}\textcolor{teal}{\sigma_1}
& \varphi_1 p_1 &= \textcolor{violet}{\sigma_{1,\gamma}}
\end{align*}

First notice that the components defining $\varphi_1$ are apporpriately composable by checking

\begin{align*}
\mu_1 t
= \hat{u}_{0;4}\textcolor{brown}{\gamma_1} \pi_0 \pi_0 w t
=\hat{u} \textcolor{teal}{\sigma_1} \pi_1 s
= \hat{u} \textcolor{teal}{\sigma_1} \pi_0 w s.
\end{align*}

Now to see that the component

\[ \varphi_1 p_0 = (
\mu_1 , \
\hat{u} \textcolor{teal}{\sigma_1} \pi_0
) , \
\textcolor{violet}{\omega_{1,0}} \pi_1
) : \hat{U} \to W_\triangle\]

is well-defined we use the definitions of the lifts $\textcolor{violet}{\omega_{1,0}} : \hat{U} \to W_\circ$ and $\textcolor{brown}{\theta_{\gamma_1}} : \hat{U}_5 \to W_\square$ to see

\begin{align*}
\textcolor{violet}{\omega_{1,0}} \pi_1
(\textcolor{violet}{\omega_{1,0}} \pi_0 \pi_0 ,
\textcolor{violet}{\omega_{1,0}} \pi_0 \pi_1 ,
\textcolor{violet}{\omega_{1,0}} \pi_0 \pi_2 ) c \\
(\textcolor{violet}{\omega_{1,0}} \pi_0 \pi_0 ,
\hat{u}_0 \textcolor{violet}{\omega_{1,1}} \pi_1 ,
\hat{u} \textcolor{teal}{\sigma_1} \pi_0) c \\
&= \big(\textcolor{violet}{\omega_{1,0}} \pi_0 \pi_0 , \\
& \ \ \ \
\hat{u}_0 (\textcolor{violet}{\omega_{1,1}} \pi_0 \pi_0 ,
\textcolor{violet}{\omega_{1,1}} \pi_0 \pi_1 ,
\textcolor{violet}{\omega_{1,1}} \pi_0 \pi_2 ) c, \\
& \ \ \ \
\hat{u} \textcolor{teal}{\sigma_1} \pi_0 \big) c \\
&= \big(\textcolor{violet}{\omega_{1,0}} \pi_0 \pi_0 , \
\hat{u}_0 \textcolor{violet}{\omega_{1,1}} \pi_0 \pi_0 , \
\hat{u}_0 \textcolor{violet}{\omega_{1,1}} \pi_0 \pi_1 ,\
\hat{u}_0\textcolor{violet}{\omega_{1,1}} \pi_0 \pi_2 , \
\hat{u} \textcolor{teal}{\sigma_1} \pi_0 \big) c \\
&= \big(\textcolor{violet}{\omega_{1,0}} \pi_0 \pi_0 , \
\hat{u}_0 \textcolor{violet}{\omega_{1,1}} \pi_0 \pi_0 , \
\hat{u}_{0;1} \textcolor{violet}{\omega_{1,2}} \pi_1 ,\
\hat{u}_{0;4} \textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 , \
\hat{u} \textcolor{teal}{\sigma_1} \pi_0 \big) c \\
&= \big(
(\textcolor{violet}{\omega_{1,0}} \pi_0 \pi_0 , \
\hat{u}_0 \textcolor{violet}{\omega_{1,1}} \pi_0 \pi_0 , \
\hat{u}_{0;1} \textcolor{violet}{\omega_{1,2}} \pi_1
)c ,\\
& \ \ \ \
\hat{u}_{0;4} \textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 , \
\hat{u} \textcolor{teal}{\sigma_1} \pi_0 \big) c \\
&= \big( \textcolor{violet}{\omega_1} ,\
\hat{u}_{0;4} \textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 , \
\hat{u} \textcolor{teal}{\sigma_1} \pi_0 \big) c \\
&= \big( (\textcolor{violet}{\omega_1} ,\
\hat{u}_{0;4} \textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0
)c, \
\hat{u} \textcolor{teal}{\sigma_1} \pi_0 \big) c \\
&= ( \mu_1 , \hat{u} \textcolor{teal}{\sigma_1} \pi_0)c.
\end{align*}

This shows $\varphi_1 : \hat{U} \to \slb$ is well-defined. By definition of $\mu_1$ and $\textcolor{violet}{\sigma_{1,\gamma}}$ in Lemma <ref> we have

\begin{align*}
( \mu_1 , \hat{u} \textcolor{teal}{\sigma_1} \pi_1)c
&= \big( (\textcolor{violet}{\omega_1} ,\
\hat{u}_{0;4} \textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0
)c, \
\hat{u} \textcolor{teal}{\sigma_1} \pi_1 \big)c \\
&= (\textcolor{violet}{\omega_1} ,\
\hat{u}_{0;4} \textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 ,\
\hat{u} \textcolor{teal}{\sigma_1} \pi_1)c \\
&= \textcolor{violet}{\sigma_{1,\gamma}} \pi_1
\end{align*}

which implies

\begin{align*}
\varphi_1 p_0
&= \varphi_1 (\pi_0 \pi_0 \pi_1 , \pi_1)
& \varphi_1 p_1
&= \varphi_1 (\pi_0 \pi_1 , (\pi_0 \pi_0 \pi_0 , \pi_1)c) \\
&= (\hat{u} \textcolor{teal}{\sigma_1} \pi_0 , \hat{u} \textcolor{teal}{\sigma_1} \pi_1 ) c
&= ( \mu_1 , \hat{u} \textcolor{teal}{\sigma_1} \pi_1)c \\
&= \hat{u} \textcolor{teal}{\sigma_1}
&= ( \textcolor{violet}{\omega_{1,0}} \pi_1 , \textcolor{violet}{\sigma_{1,\gamma}} \pi_1 ) \\
&= \textcolor{violet}{\sigma_{1,\gamma}}
\end{align*}

The sailboat, $\varphi_{1,\gamma} : \hat{U} \to \slb$, defined by

\[ \varphi_{1 , \gamma} =
\big(
( \mu_{1, \gamma} , \
\hat{u} \textcolor{purple}{\sigma_\gamma} \pi_0
) , \
\textcolor{violet}{\omega_{1,0}} \pi_1 ) , \
\hat{u} \textcolor{purple}{\sigma_\gamma} \pi_1
\big)
\]

\[ \mu_{1, \gamma} = (\textcolor{violet}{\omega_1} ,\
\hat{u}_{0;4} \textcolor{brown}{\theta_{\gamma_1}} \pi_1 \pi_0 )c \]

relates the spans $\textcolor{purple}{\sigma_\gamma} , \textcolor{violet}{\sigma_{1,\gamma}} : \hat{U} \to \spn$ in the sense that

\begin{align*}
\varphi_{1,\gamma} p_0 &= \hat{u} \textcolor{purple}{\sigma_\gamma}
& \varphi_{1,\gamma} p_1 &= \textcolor{violet}{\sigma_{1,\gamma}}.
\end{align*}

First use the definition of $\mu_{01}$, the lift $\textcolor{brown}{\theta_{\gamma_1}} : \hat{U}_5 \to W_\square$, and the span $\textcolor{purple}{\sigma_\gamma}$ to see that the components of $\varphi_{1,\gamma}$ are appropriately composable in $\mC$:

\begin{align*}
\mu_{1,\gamma} t
= \hat{u}_{0;4} \textcolor{brown}{\theta_{\gamma_1}} \pi_1 \pi_0 t
= \hat{u} \textcolor{purple}{\sigma_\gamma} \pi_0 w s
= \hat{u} \textcolor{purple}{\sigma_\gamma} \pi_1 s .
\end{align*}

Now use those definitions to compute

\begin{align*}
\textcolor{violet}{\omega_{1,0}} \pi_1
&= \big( \textcolor{violet}{\omega_1} ,\
\hat{u}_{0;4} \textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 w , \
\hat{u} \textcolor{teal}{\sigma_1} \pi_0 w \big) c \\
&= \big( \textcolor{violet}{\omega_1} ,\
(\hat{u}_{0;4} \textcolor{brown}{\theta_{\gamma_1}} \pi_0 \pi_0 w, \
\hat{u} \textcolor{teal}{\sigma_1} \pi_0 w)c \big) c \\
&= \big( \textcolor{violet}{\omega_1} ,\
(\hat{u}_{0;4} \textcolor{brown}{\theta_{\gamma_1}} \pi_1 \pi_0 , \
\hat{u} \textcolor{purple}{\sigma_\gamma} \pi_0 w)c \big) c \\
&= \big( (\textcolor{violet}{\omega_1} ,\
\hat{u}_{0;4} \textcolor{brown}{\theta_{\gamma_1}} \pi_1 \pi_0 )c , \
\hat{u} \textcolor{purple}{\sigma_\gamma} \pi_0 w \big) c \\
&= (\mu_{1, \gamma} , \hat{u} \textcolor{purple}{\sigma_\gamma} \pi_0 w)c .
\end{align*}

This shows that the component

\[ \varphi_{1, \gamma} \pi_0 = (
( \mu_{1, \gamma} , \
\hat{u} \textcolor{purple}{\sigma_\gamma} \pi_0
) , \
\textcolor{violet}{\omega_{1,0}} \pi_1 )
: \hat{U} \to W_\triangle\]

is well-defined. Similarly,

\begin{align*}
( \mu_{1, \gamma} , \hat{u} \textcolor{purple}{\sigma_\gamma} \pi_1 ) c
&= \big( (\textcolor{violet}{\omega_1} ,\
\hat{u}_{0;4} \textcolor{brown}{\theta_{\gamma_1}} \pi_1 \pi_0 )c , \
\hat{u} \textcolor{purple}{\sigma_\gamma} \pi_1 \big) c\\
&= \big( \textcolor{violet}{\omega_1} ,\
\hat{u}_{0;4} \textcolor{brown}{\theta_{\gamma_1}} \pi_1 \pi_0 , \
\hat{u} \textcolor{purple}{\sigma_\gamma} \pi_1 \big) c \\
&= \textcolor{violet}{\sigma_{1,\gamma}} \pi_1 .
\end{align*}

\begin{align*}
\varphi_{1,\gamma} p_0
&= \varphi_{1 , \gamma} (\pi_0 \pi_0 \pi_1, \pi_1)
& \varphi_{1,\gamma} p_1
&= \varphi_{1 , \gamma} \big( \pi_0 \pi_1 , (\pi_0 \pi_0 \pi_0 , \pi_1)c \big) \\
&= (\hat{u} \textcolor{purple}{\sigma_\gamma} \pi_0 , \hat{u} \textcolor{purple}{\sigma_\gamma} \pi_1 )
&= \big(\textcolor{violet}{\omega_{1,0}} \pi_1 , ( \mu_{1, \gamma} , \hat{u} \textcolor{purple}{\sigma_\gamma} \pi_1 ) c  \big) \\
& = \hat{u} \textcolor{purple}{\sigma_\gamma}
&= (\textcolor{violet}{\omega_{1,0}} \pi_1 , \textcolor{violet}{\sigma_{1,\gamma}} \pi_1 ) \\
&= \textcolor{violet}{\sigma_{1,\gamma}}.
\end{align*}

[1]
M. Artin, A. Grothendieck, and J.-L. Verdier.
SGA 4: Theorie de Topos et Cohomologie Etale des Schemas I, II, III, volume 269, 270, 305 of Lecture Notes in Mathematics.
Springer, 1971.

[2]
M. Barr and C. Wells.
Toposes, Triples and Theories.
Repr. Theory Appl. Categ., (12):x+288, 2005.
Corrected reprint of the 1985 original [MR0771116].

[3]
J. Beardsley and L. Z. Wong.
The Enriched Grothendieck Construction.
Adv. Math., 344:234–261, 2019.

[4]
M. Buckley.
Fibred 2-Categories and Bicategories.
J. Pure Appl. Algebra, 218(6):1034–1074, 2014.

[5]
P. Gabriel and M. Zisman.
Calculus of Fractions and Homotopy Theory.
Ergebnisse der Mathematik und ihrer Grenzgebiete, Band 35. Springer-Verlag New York, Inc., New York, 1967.

[6]
D. Gepner, R. Haugseng, and T. Nikolaus.
Lax Colimits and Free Fibrations in $\infty$-Categories.
Documenta Mathematica, 22:1225–1266, 2017.

[7]
P.T. Johnstone.
Sketches of an Elephant: a Topos Theory Compendium. Vol. 1, volume 43 of Oxford Logic Guides.
The Clarendon Press, Oxford University Press, New York, 2002.

[8]
Saunders Mac Lane.
Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics.
Springer-Verlag, New York, second edition, 1998.

[9]
J. Moeller and C. Vasilakopoulou.
Monoidal Grothendieck Construction.
Theory Appl. Categ., 35:Paper No. 31, 1159–1207, 2020.

[10]
A. Sharma.
CoCartesian Fibrations and Homotopy Colimits.
https://arxiv.org/abs/2205.13686, 2022.

[11]
A. Sibih.
Orbifold Atlas Groupoids.
Dalhousie University, 2013.
Thesis (M.Sc.)–Dalhousie University.

[12]
R. W. Thomason.
Homotopy Colimits in the Category of Small Categories.
Math. Proc. Cambridge Philos. Soc., 85(1):91–109, 1979.

[13]
T. tom Dieck.
Transformation Groups, volume 8 of De Gruyter Studies in Mathematics.
Walter de Gruyter & Co., Berlin, 1987.

[14]
P. Bustillo Vazquez, D. Pronk, and M. Szyld.
The Three F's for Bicategories I: Localization by Fractions is Exact.
https://arxiv.org/abs/2112.00205, 2021.

[15]
P. Bustillo Vazquez, D. Pronk, and M. Szyld.
The Three F's for Bicategories II: Minimal Fractions and Tricolimits of Bicategories.
Preprint forthcoming, 2022.