\begin{align}\label{eq assoc proof sidecalc final components of theta_a pi_0 pi_1 and theta_a pi_1 pi_1 coincide}
\begin{split}
\hat{u}_7 \pi_0 \bar{u}_0 \pi_0 \tilde{\pi}_{01} u \pi_0 \pi_0 w
&= \hat{u}_7 \pi_1 \bar{u}_1 \pi_0 \tilde{\pi}_{01} u \pi_0 \pi_0 w \\
%&= \hat{u}_7 \pi_0 \bar{u}_0 \pi_0 \tilde{u}_0 \pi_{01} \pi_0 \pi_0 w \\
%&= \hat{u}_7 \pi_0 \bar{u}_0 \pi_0 \tilde{u}_0 \pi_0 \pi_0 w \\
%&= \hat{u}_7 \bar{u} \tilde{u} \pi_0 \pi_0 w \\
%&= \hat{u}_7 \bar{u} (1 \times \sigma_c) \pi_0 \pi_0 w \\
&= \hat{u}_7 \pi_1 \bar{u}_1 (1 \times \sigma_c) \pi_0 \pi_0 w.
\end{split}
\end{align}

With these calculations and the commuting diagrams defining the covers above we can see there exists a map $\delta_0'' : \hat{U}_6 \to P(\mC) \prescript{}{wt}{\times_{ws}} W $, uniquely determined by the maps

\begin{align*}
\delta_0'' \pi_1
%= \hat{u}_7 \bar{u} \pi_0 \tilde{\pi}_{01} u \pi_0 \pi_0
= \hat{u}_7 \bar{u} (1 \times \sigma_c) \pi_0 \pi_0 ,
\end{align*}

\begin{align*}
\delta_0'' \pi_0 \pi_0
= \big(
\theta_a \pi_1 \pi_0 , \
\bar{u}_7 \pi_1
\bar{\pi}_{12} \omega \pi_0 \pi_0 , \
\bar{u}_{0:1} \bar{\pi}_{0:12} \theta \pi_0 \pi_0 w
\big)c ,
\end{align*}

\begin{align*}
\delta_0'' \pi_0 \pi_1
&= \big(
\theta_a \pi_0 \pi_0 , \\
& \ \ \ \
\bar{u}_7 \pi_0
( \bar{\pi}_{01} \omega \pi_0 \pi_0 , \
\bar{u}_{0:0} \bar{\pi}_{0:01} \theta \pi_0 \pi_0 w , \\
& \ \ \ \
\bar{u}_{0}
( \pi_0 \tilde{\pi}_{01} ( \omega \pi_0 \pi_0 ,
u_0 \theta \pi_0 \pi_0 w
)c \
%(\sigma_c \times 1) \pi_0 \pi_0 w
)c \
\big) c \\
&= \big(
\theta_a \pi_0 \pi_0 , \\
& \ \ \ \ \bar{u}_7 \pi_0
\bar{\pi}_{01} \omega \pi_0 \pi_0 , \
\bar{u}_{0:0} \bar{\pi}_{0:01} \theta \pi_0 \pi_0 w , \
\bar{u}_{0} (\sigma_c \times 1) \pi_0 \pi_0 w
) c \big).
\end{align*}

Moreover, the equations five equations above imply

\begin{align}\label{eq assoc proof sidecalc delta_0'' inducing delta_0'}
\begin{split}
\delta_0'' (\pi_0 \pi_0 , \pi_1 ) c
&= \big( \theta_a \pi_1 \pi_0 , \\
& \ \ \ \
\bar{u}_7 \pi_1
\bar{\pi}_{12} \omega \pi_0 \pi_0 , \
\bar{u}_{0:1} \bar{\pi}_{0:12} \theta \pi_0 \pi_0 w
)c , \\
& \ \ \ \
\hat{u}_7 \bar{u} (1 \times \sigma_c) \pi_0 \pi_0
\big) c \\
&= ( \theta_a \pi_1 \pi_0 , \theta_a \pi_1 \pi_1 )c \\
&= ( \theta_a \pi_0 \pi_0 , \theta_a \pi_0 \pi_1 )c \\
&= \big( \theta_a \pi_0 \pi_0 , \\
& \ \ \ \ \bar{u}_7 \pi_0
\bar{\pi}_{01} \omega \pi_0 \pi_0 , \
\bar{u}_{0:0} \bar{\pi}_{0:01} \theta \pi_0 \pi_0 w , \
\bar{u}_{0} (\sigma_c \times 1) \pi_0 \pi_0 w
) c
\big)c \\
%&= \big(
%\theta_a \pi_0 \pi_0 , \\
%& \ \ \ \
%\bar{u}_7 \pi_0
%( \bar{\pi}_{01} \omega \pi_0 \pi_0 , \
%\bar{u}_{0:0} \bar{\pi}_{0:01} \theta \pi_0 \pi_0 w , \\
%& \ \ \ \ \ \ \ \
%( \pi_0 \tilde{\pi}_{01} ( \omega \pi_0 \pi_0 ,
% u_0 \theta \pi_0 \pi_0 w
%)c \
%(\sigma_c \times 1) \pi_0 \pi_0 w
%)c , \\
%& \ \ \ \
%\hat{u}_7 \bar{u} (1 \times \sigma_c) \pi_0 \pi_0
%\big) c \\
&= \delta_0 '' (\pi_0 \pi_1 , \pi_1) c .
\end{split}
\end{align}

By the universal property of the equalizer,$\cP_{cq}(\mC)$, equation (<ref>) induces a unique map $\delta_0' : \hat{U}_6 \to \cP_{cq}(\mC)$ such that the diagram

_cq() ["ι_cq", tail]    P() t×_ws W

Û_6 [ur, "δ_0”"'] [dotted, "δ_0'"]

commutes in $\cE$. Next, to define the map $\delta_1' : \hat{U}_5 \to \cP_{cq}(\mC)$, we start by considering the definition of the pullback, $\cP ( \mC)$, that says

\[ \delta_0 \pi_0 \iota_{eq} (\pi_0 , \pi_1 \pi_0 )c = \delta_0 \pi_0 \iota_{eq} (\pi_0 , \pi_1 \pi_1 )c : \hat{U}_5 \to \mC_1 \]

are equal in $\cE$ and represent that same family of arrows in $\mC$. We can post-compose these internally to $\mC$ with the family of arrows

\[ \hat{u}_{6;7} \bar{u} \tilde{u} \pi_0 \pi_1 : \hat{U}_5 \to \mC_1\]

and after re-associating the internal composition to find each of the two Ore-squares arising at the two different covers in the following diagram.

\[\label{dgm assoc picking ore squares through covers}
\begin{tikzcd}[]
\rar[r, "/" marking, "\tilde{u}_{0:0}" near start]
& \tilde{U}_{0:0}
%\dar["/" marking, "\tilde{u}_{0:1}" near start]
\rar[r,"\tilde{\pi}_{0:01}"]
& U_0
\dar["/" marking, "u_1" near start]
\ar[r, "\theta"]
%\rar[rr, bend right, "u_1 \pi_0 \pi_1"']
& W_\square \dar["\pi_0 \pi_1"] \\
\hat{U}_5
\ar[drrrrr, bend right = 50, orange, "\square_{0,1}"']
\ar[urrrrr, bend left = 40, teal, "\square_{1,0}"]
\rar["/" marking, "\hat{u}_{6;7}" near start]
& \bar{U}
\dar["\pi_1"', orange]
\rar["/" marking, "\bar{u}" near start]
& \tilde{U}
\ar[u, "\pi_0", teal]
%\rar[r,shift left, "1 \times \sigma_c"]
%\rar[r,shift right, "\sigma_c \times 1"']
& \spn^2 \rar["/" marking, "\pi_0 \pi_1" near start]
& \mC_1 \\
& \bar{U}_1
%\ar[urr, "/" marking, "\bar{u}_1" near start]
\rar[rr,"/" marking, "\bar{u}_{0:1}"' near end]
\rar["\bar{\pi}_{0:12}"']
%\ar[u, "/" marking, "\bar{u}_{1:1}" near start]
& U_0
\uar["/" marking, "u_1" near start]
\ar[r, "\theta"']
%\rar[rr, bend right, "u_1 \pi_0 \pi_1"']
& W_\square \uar["\pi_0 \pi_1"']
\end{tikzcd}\tag{$\blacksquare$}\]

This diagram commutes in the sense that the two maps on the outside, $\hat{U}_5 \to \mC_1,$ are equal. In the figure above this corresponds to the statement that the two left-most Ore-squares on the top and bottom agree on the projection, $\pi_0 \pi_1 : W_\square \to \mC_1$. Notice $\textcolor{teal}{\square_{1,0}}$ represents one of the two Ore-squares in Diagram <ref> of the triple composition construction on the top (in teal) while $\textcolor{orange}{\square_{0,1}}$ represents the second of two Ore-squares in the triple composition construction on the bottom (in orange). Now compute the projection

\begin{align*}
\textcolor{orange}{\square_{0,1}} \pi_1 \pi_1
&= \hat{u}_{6;7} \textcolor{orange}{\pi_1} \bar{u}_{0:1} \bar{\pi}_{0:12} \theta \pi_1 \pi_1 \\
&= \hat{u}_{6;7} \textcolor{orange}{\pi_1} \bar{u}_{0:1} \bar{\pi}_{0:12} u_1 \pi_1 \pi_0 \\
&= \hat{u}_{6;7} \textcolor{orange}{\pi_1} \bar{\pi}_{12} u_{0} u_1 \pi_1 \\
&= \hat{u}_{6;7} \textcolor{orange}{\pi_1} \bar{\pi}_{12} u \pi_1 \pi_0\\
&= \hat{u}_{6;7} \textcolor{orange}{\pi_1} \bar{u}_{1} (1 \times \sigma_c) \pi_1 \pi_0\\
&= \hat{u}_{6;7} \bar{u} (1 \times \sigma_c) \pi_1 \pi_0 \\
&= \hat{u}_{6;7} \bar{u} \pi_1 \tilde{\pi}_{12} \sigma_c \pi_0 \\
&= \hat{u}_{6;7} \bar{u} \pi_1 \tilde{\pi}_{12} \omega \pi_1.
\end{align*}

Since $\omega \pi_1 = (\omega \pi_0 \pi_0 , \omega \pi_0 \pi_1 , \omega \pi_0 \pi_2) c$ with $\omega \pi_0 \pi_2 = u \pi_0 \pi_0$ by definition of $\omega : U \to W_\circ$ we can expand and notice that the final map,

\[ \hat{u}_{6;7} \bar{u} \pi_1 \tilde{\pi}_{12} \omega \pi_0 \pi_2 : \hat{U}_5 \to W \]

is equal to

\[ \hat{u}_{6;7} \bar{u} \pi_1 \tilde{\pi}_{12} u \pi_0 \pi_0 = \textcolor{teal}{\square_{1,0}} \pi_1 \pi_1 : \hat{U}_5 \to W. \]

This induces a unique map $\delta_1'' : \hat{U}_5 \to P(\mC) \prescript{}{t}{\times_{ws}} W$ determined by the map $\hat{U}_5 \to W$ given by

\begin{align*}
\delta_1'' \pi_1
= \textcolor{teal}{\square_{1,0}} \pi_1 \pi_1 ,
\end{align*}

and the map $\delta_1'' \pi_0 : \hat{U}_5 \to P(\mC) $ whose left projection, $\delta_1'' \pi_0\pi_0$, is the pairing map

\begin{align*}
\big(
&\delta_0 \iota_{eq} \pi_0 w ,\\
\hat{u}_6 \theta_a \pi_1 \pi_0 , \\
&\hat{u}_{6;7} \textcolor{orange}{\pi_1} \bar{\pi}_{12} \omega \pi_0 \pi_0 , \\
&\hat{u}_{6;7} \textcolor{orange}{\pi_1} \bar{\pi}_{12} u_0 \theta \pi_1 \pi_0 ,\\
&\hat{u}_{6;7} \bar{u} \textcolor{orange}{\pi_1} \tilde{\pi}_{12} \omega \pi_0 \pi_0 ,\\
&\hat{u}_{6;7} \bar{u} \textcolor{orange}{\pi_1} \tilde{\pi}_{12} u_0 \theta \pi_0 \pi_0 w
\big) c
\end{align*}

and whose right projection, $\delta_1'' \pi_0 \pi_1$, is the pairing map

\begin{align*}
\big(
&\delta_0 \iota_{eq} \pi_0 w ,\\
&\hat{u}_6 \theta_a \pi_0 \pi_0 w , \\
&\hat{u}_{6;7} \textcolor{teal}{\pi}_0 \bar{\pi}_{01} \omega \pi_0 \pi_0 , \\
&\hat{u}_{6;7} \textcolor{teal}{\pi}_0 \bar{\pi}_{01} u_0 \theta \pi_0 \pi_0 w ,\\
&\hat{u}_{6;7} \bar{u} \textcolor{teal}{\pi}_1 \tilde{\pi}_{01} \omega \pi_0 \pi_0 ,\\
&\hat{u}_{6;7} \bar{u} \textcolor{teal}{\pi}_0 \tilde{\pi}_{01} u_0 \theta \pi_1 \pi_0
\big) c .
\end{align*}

The fact that $\delta_1''$ satisfies the equalizer condition for $\cP_{cq}(\mC)$, namely

\[\delta_1'' (\pi_0 \pi_0 , \pi_1) c = \delta_1'' (\pi_0 \pi_1 , \pi_1) c,\]

follows from the calculations above. This induces the unique map $\delta_1'$ that makes the following diagram commute:

_cq() ["ι_cq" ]     P() t×_ws W

Û_5 [ur, "δ_1”"'] [dotted, "δ_1'"]

Finally, the map $\delta_2' : \hat{U}_4 \to \cP_{cq}(\mC)$ is similarly induced by a map $\delta_2'' : \hat{U}_4 \to P(\mC) \prescript{}{t}{\times_{ws}} W$ which can be deduced expanding the right and left-hand sides of the equation

\[ \delta_1 \iota_{eq} (\pi_0 , \pi_1 \pi_0) c = \delta_1 \iota_{eq} (\pi_0 \pi_1 \pi_1) c \]

whose common target is the middle object of the original composable triple of spans, post-composing with the arrow

\[ \hat{u}_{5;6} \bar{u} \tilde{u} \pi_1 \pi_1 : \hat{U}_4 \to \mC_1, \]

which is final map given by applying the projection $\pi_0 \pi_1 : W_\square \to \mC_1$ of the Ore-squares

\[
\begin{tikzcd}[]
\rar[rr, "/" marking, "\tilde{u}_{0:0}" near start]
& \tilde{U}_{0:0}
\rar[r,"\tilde{\pi}_{0:01}"]
& U_0
\dar["/" marking, "u_1" near start]
\ar[r, "\theta"]
& W_\square \dar["\pi_1 \pi_1"]
\\
\hat{U}_4
\ar[drrrrr, bend right = 40, orange, "\square_{0,0}"']
\ar[urrrrr, bend left = 50, teal, "\square_{1,1}"]
\rar["/" marking, "\hat{u}_{4;7}" near start]
& \bar{U}
\ar[u, "\pi_0", teal]
\rar["/" marking, "\bar{u}" near start]
& \tilde{U}
\dar["\pi_1"', orange]
& \spn^2 \rar["/" marking, "\pi_1 \pi_0" near start]
& W
\\
& \bar{U}_1
\rar[r,"/" marking, "\bar{u}_{0:1}"' near end]
\rar["\bar{\pi}_{0:12}"']
& U_0
\uar["/" marking, "u_1" near start]
\ar[r, "\theta"']
& W_\square \uar["\pi_1 \pi_1"']
\\
\end{tikzcd}.\tag{$\blacksquare \blacksquare$}\]

Picking out the composable pairs in $W$ to get a cover witnessing a family of spans whose left leg is in $W$ is done in order from right to left in the diagram before. This is identical to how it was done in the proof of Lemma <ref> from Section <ref>, except this time an extra zippering step leads to an extra composable pair in $W$. The chain of covers and lifts are given by applying In.Frc(2) four times as seen in diagrams

\[\label{dgm assoc covers weak comp}
\begin{tikzcd}[column sep = large]
W_\circ \rar["(\pi_0 \pi_1 {,} \pi_0 \pi_2)"]
&W \prescript{}{wt}{\times_{ws}} W
\\
\hat{U}_1 \rar["/" marking, "\hat{u}_2" near start]
\uar[dotted, "\omega_1"]
\hat{U}_2
\rar["/" marking, "\hat{u}_3" near start]
\dar[dotted, "\omega_0"']
\uar["(\omega_0 \pi_1 {,} \hat{u}_{3;5} \delta_0 \iota_{eq} \pi_0) "']
\hat{U}_3 \dar["( \delta_2 \iota_{eq} \pi_0 {,} \hat{u}_4 \delta_1 \iota_{eq} \pi_0 )"]
\\
& W_\circ \rar["(\pi_0 \pi_1 {,} \pi_0 \pi_2)"']
&W \prescript{}{wt}{\times_{ws}} W
\end{tikzcd} \tag{$\star \star$} \]

\[ \label{dgm assoc covers weak comp 2}
\begin{tikzcd}
W_\circ \rar["(\pi_0 \pi_1 {,} \pi_0 \pi_2)"]
&W \prescript{}{wt}{\times_{ws}} W
& \\
\hat{U}
\uar[dotted, "\omega_3"]
\rar["/" marking, "\hat{u}_0" near start]
\hat{U}_0
\rar["/" marking, "\hat{u}_1" near start]
\dar[dotted, "\omega_2"']
\uar["(\omega_2 \pi_1 {,} \hat{u}_{1;7} \sigma_0 \pi_0)"']
\hat{U}_1
\dar["(\omega_1 \pi_1 {,} \hat{u}_{2;6} \theta_a \pi_0 \pi_0 )"]
\\
&W_\circ \rar["(\pi_0 \pi_1 {,} \pi_0 \pi_2)"']
&W \prescript{}{wt}{\times_{ws}} W
\end{tikzcd}. \tag{$\star \star \star$}\]

At this point we can define two sailboats, $\varphi_0 , \varphi_1 : \hat{U} \to \slb$, whose deck-projections give the two composite representatives we care for,

\[ \varphi_0 p_0 = \hat{u} \sigma_0 \quad , \quad \varphi_1 p_0 = \hat{u} \sigma_1\]

and whose sail-projections agree,

\[ \varphi_0 p_1 = \varphi_1 p_1\]

by virtue of zippering. To define these explicitly we first expand both sides of the equation

\[ \hat{u}_{0; 3} \delta_2 \iota_{eq} (\pi_0 , \pi_1 \pi_0) c = \hat{u}_{0; 3} \delta_2 \iota_{eq} (\pi_0 , \pi_1 \pi_1) c\]

into composites and post-compose both sides with the map represented by

\[ \hat{u} \bar{u} \tilde{u} \pi_2 \pi_1 : \hat{U} \to \mC_1.\]

This gives two equal representations of the right leg of the intermediate span,

\[ \varphi_0 p_1 \pi_1 = \varphi_1 p_1 \pi_1, \]

and by re-associating the composites in both representations we can get

\[ \varphi_0 p_1 \pi_1 = ( \mu_0 , \hat{u} \sigma_0 \pi_1) c \]

\[ \varphi_1 p_1 \pi_1 = (\mu_1 , \hat{u} \sigma_1 \pi_1) c\]

for two maps, $\mu_0 , \mu_1 : \hat{U} \to \mC_1$, which represent the masts of the sailboats being picked out. This gives the maps $\hat{U} \to \slb$ defined by the pairing maps

\[ \varphi_0 = \big( ( ( \mu_0 , \hat{u} \sigma_0) , \ \omega_2 \pi_1 ) , \ \hat{u} \sigma_0 \pi_1 \big) \]

\[ \varphi_1 = \big( ( ( \mu_1 , \hat{u} \sigma_1) , \ \omega_2 \pi_1 ) , \ \hat{u} \sigma_1 \pi_1 \big) . \]

It follows that

\[ \hat{u} \sigma_0 q = \varphi_0 p_0q = \varphi_0 p_1 q = \varphi_1 p_1 q = \varphi _1 p_0 q = \hat{u} \sigma_1 q \]

and since $\hat{u}$ is epic,

\[ \sigma_0 q = \sigma_1 q.\]

§.§.§ Identity Laws

The only conditions left to check in order to see that $\mCW$ is an internal category are the left and right identity laws for composition. This rest of this section is dedicated precisely to this. The identity laws are typically proven, when $\cE = \Set$, by looking at the composites

\[\begin{tikzcd}
&& \cdot \\
&& \cdot \\
& \cdot && \cdot \\
\cdot && \cdot && \cdot
\arrow[from=3-2, to=4-1, "\circ" marking, "x"']
\arrow[from=3-2, to=4-3, "x"]
\arrow[from=3-4, to=4-3, "\circ" marking, "f"']
\arrow[from=3-4, to=4-5, "g"]
\arrow[from=2-3, to=3-2, "\circ" marking, "v"']
\arrow[from=2-3, to=3-4, "h"]
\arrow[from=1-3, to=2-3, "u"]
\arrow[curve={height=30pt}, from=1-3, to=4-1,"\circ" marking, "y"']
\end{tikzcd}\]

\[
\begin{tikzcd}
&& \cdot \\
&& \cdot \\
& \cdot && \cdot \\
\cdot && \cdot && \cdot
\arrow[from=3-2, to=4-1, "\circ" marking, "f"']
\arrow[from=3-2, to=4-3, "g"]
\arrow[from=3-4, to=4-3, "\circ" marking, "x"']
\arrow[from=3-4, to=4-5, "x"]
\arrow[from=2-3, to=3-2, "\circ" marking, "v"']
\arrow[from=2-3, to=3-4, "h"]
\arrow[from=1-3, to=2-3, "u"]
\arrow[curve={height=30pt}, from=1-3, to=4-1, "\circ" marking, "y"']
\end{tikzcd}\]

and producing the sailboats

\[\begin{tikzcd}[column sep = large, row sep = large]
& \cdot & \\
\cdot & \cdot & \cdot
\arrow[from=1-2, to=2-2, "uh"]
\arrow[from=1-2, to=2-1, "\circ" marking, "y"']
\arrow[from=2-2, to=2-1, "\circ" marking, "f"near start]
\arrow[from=2-2, to=2-3, "g"' near start]
\end{tikzcd}\qquad \qquad
\begin{tikzcd}[column sep = large, row sep = large]
& \cdot & \\
\cdot & \cdot & \cdot
\arrow[from=1-2, to=2-2, "uv"]
\arrow[from=1-2, to=2-1, "\circ" marking, "y"']
\arrow[from=2-2, to=2-1, "\circ" marking, "f"near start]
\arrow[from=2-2, to=2-3, "g"' near start]
\end{tikzcd}\]

that relate each composite to the span $(f,g)$ respectively. Since proving the identity laws requires a lot of source and target maps for different objects and we have been overloading their notation, for the rest of this section we rename the source and target maps for spans and sailboats to keep our calculations somewhat more legible. Let $s', t' : \spn \to \mC_0$ denote the source and target maps for spans, given by the pairing maps $s' = \pi_0 w t$ and $t' = \pi_1 t$ respectively. Also let $s'' , t'' : \slb \to \mC_0$ denote the source and target maps for sailboats given by the pairing maps $s'' = \pi_0 \pi_1 t = \pi_0 \pi_0 \pi_1 t$ and $t'' = \pi_1 t $. Internalizing this will require covers that witness composition of spans along with the canonical left and right identity inclusions,

\[
\begin{tikzcd}[]
\spn \rar["( s' \sigma_\alpha {,} 1)"] & \spn \tensor[_{t'}]{\times}{_{s'}} \spn
\end{tikzcd}\qquad \qquad
\begin{tikzcd}[]
\spn \rar["( 1 {,} t' \sigma_\alpha)"] & \spn \tensor[_{t'}]{\times}{_{s'}} \spn
\end{tikzcd}
\]

\[
\begin{tikzcd}[]
\slb \rar["( s'' \varphi_\alpha {,} 1)"] & \slb \tensor[_{t''}]{\times}{_{s''}} \slb
\end{tikzcd}\qquad \qquad
\begin{tikzcd}[]
\slb \rar["( 1 {,} t'' \varphi_\alpha)"] & \slb \tensor[_{t''}]{\times}{_{s''}} \slb
\end{tikzcd},
\]

induced by $\sigma_\alpha = (\alpha, \alpha w)$, $\varphi_\alpha = \big( ( ( \alpha s w e , \alpha), \alpha ) , \alpha w \big)$, and the fact that $\alpha$ is a section of $w t$. The following lemma is used to define the identity inclusions $\mCW_1 \to \mCW_1 \tensor[_t]{\times}{_s} \mCW_1$ used in the identity law statement.

The diagrams

["(s” φ_α, 1)"'] [shift left, "p_0"] [shift right, "p_1"']     ["(s' σ_α, 1)"] [two heads, "q"]     _1 [dotted, "(s e , 1)"]

[_t”]×_s”[shift left, "p_0^2"] [shift right, "p_1^2"']     [_t']×_s' ["q^2"']     _1 [_t]×_s _1

["( 1 , t” φ_α)"'] [shift left, "p_0"] [shift right, "p_1"']     ["(1 , t' σ_α)"] [two heads, "q"]     _1 [dotted, "(1 , t e)"]

[_t”]×_s”[shift left, "p_0^2"] [shift right, "p_1^2"']     [_t']×_s' ["q^2"']     _1 [_t]×_s _1

commute in the sense that for $i = 0,1$

\[(s'' \varphi_\alpha , 1) p_i^2 = p_i (s' \sigma_\alpha , 1) \qquad , \qquad (t'' \varphi_\alpha , 1) p_i^2 = p_i (t' \sigma_\alpha , 1), \]

which uniquely determines

\[(s e , 1) \qquad \text{ and } \qquad (1,te)\]

To see the squares on the left commute first notice that

\[ p_0 s' = p_0 \pi_0 w t = \pi_0 \pi_0 \pi_1 w t = s'' = \pi_0 \pi_1 w t = p_1 \pi_0 w t = p_1 s' \]

\[ p_0 t' = p_0 \pi_1 t = \pi_1 t = t'' = p_1 \pi_1 t = p_1 t'.\]

Now for $i = 0,1$ we have

\begin{align*}
(s'' \varphi_\alpha , 1)p_i^2
&= (s'' \varphi_\alpha , 1)(\pi_0 p_i , \pi_1 p_i) \\
&= \big((s'' \varphi_\alpha , 1)\pi_0 p_i ,  \ (s'' \varphi_\alpha , 1) \pi_1 p_i \big) \\
&= \big(s'' \varphi_\alpha p_i , \ p_i \big) \\
&= \big(s'' (\alpha , \alpha w) , \ p_i \big) \\
&= \big(s'' \sigma_\alpha , \ p_i \big) \\
&= \big(p_i s' \sigma_\alpha , \ p_i \big) \\
&= p_i (s' \sigma_\alpha , 1)
\end{align*}

and similarly

\begin{align*}
(t'' \varphi_\alpha , 1)p_i^2
&= p_i (t' \sigma_\alpha , 1)
\end{align*}

showing that the squares on the left commute as described. Then since $p_0^2 q_2 = p_1^2 q_2$ we get

\[ p_0 (s' \sigma_\alpha , 1) q^2 = p_1 (s' \sigma_\alpha , 1) q^2 \]

\[ p_0 ( 1, t' \sigma_\alpha ) q^2 = p_1 (1, t' \sigma_\alpha ) q^2 \]

inducing the unique vertical maps on the right in the lemma's diagrams by the universal property of the coequalizer $\mCW_1$. Now we show these are precisely $(se, 1), (1, te) : \mCW_1 \to \mCW_1 \tensor[_t]{\times}{_s} \mCW_1$. Notice the outer squares of the following pullback diagrams

[ddr, bend right, "s' e"'] [drr, bend left, "q"] [dr, dotted, "(s' σ_α, 1) q^2"]

_1 [_t]×_s _1 [dr, phantom, "" , very near start, color=black] ["π_0^2"'] ["π_1^2"]     _1 ["s"]

_1 ["t"']     _0
[ddr, bend right, "q"'] [drr, bend left, "t'e"] [dr, dotted, "(1 , t' σ_α) q^2"]

_1 [_t]×_s _1 [dr, phantom, "" , very near start, color=black] ["π_0^2"'] ["π_1^2"]     _1 ["s"]

_1 ["t"']     _0

commute because $s' = q s$ implies

\begin{align*}
e t
= \sigma_\alpha q t
= \sigma_\alpha t'
= \sigma_\alpha \pi_1 t
= (\alpha , \alpha w) \pi_1 t
= \alpha w t
= 1_{\mC_0}
\end{align*}

and similarly $t' = qt$ implies

\[ e s = \sigma_\alpha q s = \sigma_\alpha s' = \alpha w t = 1_{\mC_0}. \]

The triangles in the left diagram commute because

\[(s' \sigma_\alpha {,} 1) q^2 \pi_0^2
= (s' \sigma_\alpha {,} 1) \pi_0 q
= s' \sigma_\alpha q
= s' e \]

\[ (s' \sigma_\alpha {,} 1) q^2 \pi_1^2
= (s' \sigma_\alpha {,} 1) \pi_1 q

and a similar calculation shows the triangles on the right commute.
Then we have

\[(s' \sigma_\alpha , 1) q^2 = (s' e , q) = (qse , q) = q (se, 1) \]

\[( 1, t' \sigma_\alpha) q^2 = (q, t' e) = (q, qte) = q (1, te). \]

as required.

The diagram

[column sep = large, row sep = large]
["s' σ_α, 1)"] [dr, two heads, "q"']     [_t']×_s' ["c'"]     ["(1 , t' σ_α)"'] [dl, two heads,"q"]

commutes in $\cE$.

We show the left triangle commutes, the argument for the right triangle is similar. Pullback $u_1$ along $(s' \sigma_\alpha , 1)$ and then pullback along $u_0$ as shown in the diagram below to obtain a cover of $\spn$ that witnesses the entire composition process of an arbitary span and a pre-composable span representing the identity in $\mCW_1$. The following diagram commutes by definition.

[column sep = large ]
U^* [dr, phantom, "" , very near start, color=black][dd, bend right = 50, "/" marking, "u^*"' near end] ["/" marking, "u_0^*" near start] ["π_1"]
[dd, bend left = 50, "/" marking, "u" near start]
["/" marking, "u_0"'near end]

[dd, two heads, "q"]

[dr, phantom, "" , very near start, color=black]
["/" marking, "u_1^*"near start]

["/" marking, "u_1"'near end]

["(s' σ_α, 1)"']

[_t']×_s' ["c"']

By commutativity of the outer square above and since $u^*$ is epic, it suffices to show

\[ u^* \pi_1 \sigma_\circ q = u^* q. \]

This can be done by translating the usual proof of the left identity law for span composition and defining a sailboat $\varphi : U^* \to \slb$ such that

\[ \varphi p_0 = u^* \quad \text{ and } \quad \varphi p_1 = \pi_1 \sigma_\circ \]

to give

\[ u^* q =\varphi p_0 q = \varphi p_1 q = \pi_1 \sigma_\circ q. \]

First compute

\begin{align*}
\pi_1 \sigma_\circ
&= \pi_1 \big( \omega \pi_1 , \ (\omega \pi_0 \pi_1 , u_0 \theta \pi_1 \pi_0 , \ u \pi_1 \pi_1 )c \big)
\\
\big(
\pi_1 \omega \pi_1 , \
(\pi_1 \omega \pi_0 \pi_1 ,
\pi_1 u_0 \theta \pi_1 \pi_0 , \
\pi_1 u \pi_1 \pi_1
\big) \\
\big(
\pi_1 \omega \pi_1 , \
(\pi_1 \omega \pi_0 \pi_1 ,
u^*_0 \pi_1 \theta \pi_1 \pi_0 , \
u^* \pi_1
\big) .
\end{align*}

Now notice that

\begin{align*}
\pi_1 u \pi_0 \pi_0 w
&= u^* (s' \sigma_\alpha, 1) \pi_0 \pi_0 w \\
&= u^* (s' \sigma_\alpha, 1) \pi_0 \pi_0 w \\
&= u^* s' \sigma_\alpha \pi_0 w \\
&= u^* s' \alpha w \\
&= u^* s' \sigma_\alpha \pi_1 \\
&= u^*_0 u^*_1 (s' \sigma_\alpha , 1) \pi_0 \pi_1\\
&= u^*_0 \pi_1 u_1 \pi_0 \pi_1 \\
&= u^*_0 \pi_1 \theta \pi_0 \pi_1
\end{align*}

and use this in the third line of the following calculation along with the definition of $W_\square$ (the Ore-condition) in the fifth line.

\begin{align*}
\pi_1 \omega \pi_1
(\pi_1 \omega \pi_0 \pi_0 , \
\pi_1 \omega \pi_0 \pi_1 w, \
\pi_1 \omega \pi_0 \pi_2 w
)c \\
(\pi_1 \omega \pi_0 \pi_0 , \
\pi_1 u_0 \theta \pi_0 \pi_0 w, \
\pi_1 u \pi_0 \pi_0 w
)c \\
(\pi_1 \omega \pi_0 \pi_0 , \
u^*_0 \pi_1 \theta \pi_0 \pi_0 w, \
u^*_0 \pi_1 \theta \pi_0 \pi_1
)c \\
\big(
\pi_1 \omega \pi_0 \pi_0 , \
u^*_0 \pi_1
(\theta \pi_0 \pi_0 w, \
\theta \pi_0 \pi_1 )c
\big)c \\
\big(
\pi_1 \omega \pi_0 \pi_0 , \
u^*_0 \pi_1
(\theta \pi_1 \pi_0 , \
\theta \pi_1 \pi_1 w)c
\big)c \\
\pi_1 \omega \pi_0 \pi_0 , \
u^*_0 \pi_1 \theta \pi_1 \pi_0 , \
u^*_0 \pi_1 \theta \pi_1 \pi_1 w
)c \\
\pi_1 \omega \pi_0 \pi_0 , \
u^*_0 \pi_1 \theta \pi_1 \pi_0 , \
u^*_0 \pi_1 u_1 \pi_1 \pi_0 w
)c \\
\pi_1 \omega \pi_0 \pi_0 , \
u^*_0 \pi_1 \theta \pi_1 \pi_0 , \
u^* (s' \sigma_\alpha , 1) \pi_1 \pi_0 w
)c \\
\pi_1 \omega \pi_0 \pi_0 , \
u^*_0 \pi_1 \theta \pi_1 \pi_0 , \
u^* \pi_0 w
\end{align*}

The last calculation shows that the sailboat $\varphi : U^* \to \slb$ defined by

\[ \varphi =
\big(
(\pi_1 \omega \pi_0 \pi_0 , u_0^* \pi_1 \theta \pi_1 \pi_0 w ) c , \
u^* \pi_0 ) ,\
\pi_1 \omega \pi_1 ) ,\
u^* \pi_1 \big)
\]

is well-defined. Clearly we have

\[ \varphi p_0 = \varphi (\pi_0 \pi_0 \pi_1 , \pi_1 ) = (u^* \pi_o , u^* \pi_1) = u^*\]

and the first calculation along with associativity of composition in the last equality below shows us that

\begin{align*}
\varphi p_1
&= \varphi (\pi_0 \pi_1 , \ (\pi_0 \pi_0 \pi_0 , \pi_1)c) \\
&= \big( \pi_1 \omega \pi_1 , \ ( (\pi_1 \omega \pi_0 \pi_0 , u^*_0 \pi_1 \theta \pi_1 \pi_0) c , u^* \pi_1\big)\\
&= \pi_1 \sigma_\circ .
\end{align*}

The diagram

_1 ["(se, 1)"] [dr, equals]    _1 [_t]×_s _1 ["c"]     ["(1, te)"'] _1 [dl, equals]

commutes in $\cE$.

By Lemma <ref>, the diagrams

\[
\begin{tikzcd}[]
\spn \dar["(s' \sigma_\alpha {,} 1)"'] \rar[two heads, "q"] & \mCW_1 \dar[dotted, "(s e {,} 1)"] & \\
\spn \tensor[_{t'}]{\times}{_{s'}} \spn \rar["q^2"'] \ar[dr, "c'"'] & \mCW_1 \tensor[_t]{\times}{_s} \mCW_1 \dar[dotted, "c"] \\
& \mCW_1
\end{tikzcd} \]

\[
\begin{tikzcd}[]
\spn \dar["(1 {,} t' \sigma_\alpha)"'] \rar[two heads, "q"] & \mCW_1 \dar[dotted, "(1 {,} t e)"] \\
\spn \tensor[_{t'}]{\times}{_{s'}} \spn \rar["q^2"'] \ar[dr, "c'"'] & \mCW_1 \tensor[_t]{\times}{_s} \mCW_1 \dar[dotted, "c"] \\
& \mCW_1
\end{tikzcd}
\]

commute and by Lemma <ref> the composites on the left sides are both equal to $q$. It follows that the right-hand sides are identities by uniqueness.

§.§ The Internal Localization Funtor

In this section we define the (internal) localization functor, $L : \mC \to \mCW$, prove it is an internal functor, define what it means for an internal functor to invert an arrow $w : W \to \mC_1$, and then show that $L$ inverts $w : W \to \mC_1$.

§.§.§ Defining the Internal Functor

The localizing internal functor, $L : \mC \to \mCW$, is defined on objects to be the identity map, $L_0 = 1_{\mC_0} $, because $\mCW_0 = \mC_0$. On arrows we use the section $\alpha : \mC_0 \to W$ along with the source map and the identity to get a (family of) span(s) which can be mapped to $\mCW_1$ as follows.

[column sep = large]
_1 [dr, "L_1"'] ["( s α, ( s αw , 1) c )"]     [two heads, "q"]

When $\cE = \Set$ this says $L_1$ maps an arrow $f : a \to b$ in $\mC_1$ to the equivalence class of spans represented by the span

\[ \begin{tikzcd}[]
a & \lar["\circ" marking, "\alpha(a)"'] a \rar[rr, bend left, "\alpha (a) f"] \rar["\circ" marking, "\alpha(a)"'] & a \rar["f"'] & b
\end{tikzcd}. \]

Identities are preserved since $e s = 1_{\mC_0}$ and by the identity law, $(1 , te) c = 1_{\mC_1}$, in $\mC$

\begin{align*}
e L_1
&= e \big( s \alpha {,} ( s \alpha w {,} 1) c \big) q \\
&= \big( e s \alpha {,} ( e s \alpha w {,} e ) c \big) q \\
&= \big( \alpha {,} ( \alpha w {,} e ) c \big) q \\
&= \big( \alpha {,} \alpha w ( 1 , t e ) c \big) q \\
&= ( \alpha {,} \alpha w ) q \\
\end{align*}

where the last line is the identity structure map, $e = ( \alpha {,} \alpha w ) q : \mCW_0 \to \mCW_1$, for the internal category $\mCW$. This shows the diagram

_0 ["e"'] [equals, "L_0"]     _0 ["e"]

_1 ["L_1"']     _1

commutes in $\cE$ so $L = (L_0, L_1)$ preserves the identity structure. Composition is preserved in a less obvious way. We need Lemma <ref> to see

\begin{align*}
c L_1
&= c \big( s \alpha {,} ( s \alpha w {,} 1) c \big) q \\
&= \big( c s \alpha {,} ( c s \alpha w {,} c ) c \big) q \\
&= \big( \pi_0 s \alpha {,} ( \pi_0 s \alpha w {,} c ) c \big) q \\
&= \big( \pi_0 ( s \alpha {,} ( s \alpha w {,} 1) c ), \pi_1 ( s \alpha {,} ( s \alpha w {,} 1) c ) \big) c' \\
&= \big( \pi_0 ( s \alpha {,} ( s \alpha w {,} 1) c ), \pi_1 ( s \alpha {,} ( s \alpha w {,} 1) c ) \big) (q \times q) c \\
&= \big( \pi_0 ( s \alpha {,} ( s \alpha w {,} 1) c ) q , \pi_1 ( s \alpha {,} ( s \alpha w {,} 1) c )q \big) c \\
&= (L_1 \times L_1) c
\end{align*}

and conclude that the diagram

_2 ["c"'] [ "L_1 ×L_1 "]     _1^2 ["c"]

_1 ["L_1"']     _1

commutes in $\cE$. It follows that $L = (L_0, L_1)$ is an internal functor.

The diagram

[column sep = huge, row sep = large]
["( π_0 s α, ( π_0 s αw , c ) c ) "']
[rr,"( π_0 ( s α, ( s αw , 1) c ),π_1 ( s α, ( s αw , 1) c ) )"]

[rr,two heads, "q"']

commutes in $\cE$.

Internalize the following figure

\begin{equation}\label{fig the big}
\begin{tikzcd}[column sep = scriptsize]
&&& \cdot \\
&&& \cdot \\
\\
a & \cdot & a & b & \cdot & b & c & \cdot & \cdot & \cdot \\
&& \cdot \\
&&& \cdot &&b & &&& \cdot \\
&&& \cdot \\
&& \cdot && a \\
\\
&&& \cdot &&&&&& \cdot \\
\\
\\
&&& \cdot
\arrow[from=4-2, to=4-1, "\circ" marking, "\alpha(a)"']
\arrow[from=4-2, to=4-3 ,"\alpha(a)"']
\arrow[from=4-3, to=4-4, "f"']
\arrow[curve={height=-12pt}, from=4-2, to=4-4, "\alpha(a) f"]
\arrow[from=4-5, to=4-4, "\circ" marking, "\alpha(b)"']
\arrow[from=4-5, to=4-6,"\alpha(b)"']
\arrow[from=4-6, to=4-7,"g"']
\arrow[curve={height=-12pt}, from=4-5, to=4-7, "\alpha(b) g"]
\arrow[curve={height=12pt}, from=2-4, to=4-2, "\circ" marking,, teal]
\arrow[curve={height=-12pt}, from=2-4, to=4-5, teal]
\arrow[from=1-4, to=2-4, teal]
\arrow[curve={height=25pt}, from=1-4, to=4-1, "\circ" marking, teal]
\arrow[from=8-3, to=4-1, "\circ" marking, orange, "\alpha(a)"']
\arrow[from=8-3, to=8-5, "\alpha(a)"' near end, orange]
\arrow[from=8-5, to=6-6, orange, "f"']
\arrow[from= 6-6, to=4-7, "g"', orange]
\arrow[from=5-3, to=4-2, olive]
\arrow[from=5-3, to=8-3, olive, "\circ" marking]
\arrow[from=6-4, to=5-3, olive, "\circ" marking]
\arrow[from=6-4, to=4-5, olive]
\arrow[from=7-4, to=6-4, violet]
\arrow[from=7-4, to=8-3, violet, "\circ" marking]
\arrow[from=10-4, to=7-4, violet, crossing over]
\arrow[curve={height=-24pt}, from=10-4, to=4-1, violet, "\circ" marking]
\arrow[curve={height=-30pt}, from=4-8, to=10-4, olive, "\circ" marking]
\arrow[curve={height=24pt}, from=4-8, to=1-4, olive]
\arrow[from=4-9, to=4-8, magenta, "\circ" marking]
\arrow[from=4-10, to=4-9,magenta, "\circ" marking]
\arrow[from=6-10, to=4-10, violet]
\arrow[from=6-10, to=4-8, violet, "\circ" marking]
\arrow[from=10-10, to=6-10,violet]
\arrow[from=10-10, to=10-4, "\circ" marking, violet]
\arrow[curve={height=30pt}, from=13-4, to=10-10, violet]
\arrow[curve={height=-30pt}, from=13-4, to=4-1,"\circ" marking, violet]
\end{tikzcd} \tag{A}
\end{equation}

where olive coloured arrows are fillers of Ore-squares, violet coloured arrows $W$-composition fillers, and magenta coloured arrows are zippering fillers. To do this internally, start by taking the pullback

\begin{equation}\label{pb comp + representatives for L_1}
\begin{tikzcd}[column sep = huge, row sep = large]
\tilde{U} \rar[rrr, "\pi"] \dar["/" marking, "\tilde{u}"' near end] \arrow[drrr, phantom, "\usebox\pullback" , very near start, color=black] &&& U \dar["/" marking, "u" near start] \\
\mC_2
\rar[rrr,"\big( \pi_0 ( s \alpha {,} ( s \alpha w {,} 1) c ){,}\pi_1 ( s \alpha {,} ( s \alpha w {,} 1) c ) \big)"']
&&& \spn^2
\end{tikzcd}\tag{0}
\end{equation}

to give a cover witnessing span-composition along with the representative spans for $L_1$. In Figure $(A)$, this gives access to the teal and black coloured arrows. We begin by internalizing the `inner' part of Figure <ref>

\begin{equation*}\label{fig inner part}
\begin{tikzcd}[row sep = scriptsize]
a & \cdot & a & b & \cdot & b & c \\
&& \cdot \\
&&& \cdot &&b & \\
&&& \cdot \\
&& \cdot && a \\
\\
&&& \cdot &&& \\
\\
\\
&&& \cdot
\arrow[from=1-2, to=1-1, "\circ" marking, "\alpha(a)"']
\arrow[from=1-2, to=1-3 ,"\alpha(a)"', near end]
\arrow[from=1-3, to=1-4, "f"']
\arrow[curve={height=-12pt}, from=1-2, to=1-4, "\alpha(a) f"]
\arrow[from=1-5, to=1-4, "\circ" marking, "\alpha(b)"']
\arrow[from=1-5, to=1-6,"\alpha(b)"']
\arrow[from=1-6, to=1-7,"g"']
\arrow[curve={height=-12pt}, from=1-5, to=1-7, "\alpha(b) g"]
%\arrow[curve={height=12pt}, from=2-4, to=4-2, "\circ" marking,, teal]
%\arrow[curve={height=-12pt}, from=2-4, to=4-5, teal]
%\arrow[from=1-4, to=2-4, teal]
%\arrow[curve={height=25pt}, from=1-4, to=-1, "\circ" marking, teal]
\arrow[from=5-3, to=1-1, "\circ" marking, orange, "\alpha(a)"']
\arrow[from=5-3, to=5-5, "\alpha(a)"' near end, orange]
\arrow[from=5-5, to=3-6, orange, "f"']
\arrow[from= 3-6, to=1-7, "g"', orange]
\arrow[from=2-3, to=1-2, olive]
\arrow[from=2-3, to=5-3, olive, "\circ" marking]
\arrow[from=3-4, to=2-3, olive, "\circ" marking]
\arrow[from=3-4, to=1-5, olive]
\arrow[from=4-4, to=3-4, violet]
\arrow[from=4-4, to=5-3, violet, "\circ" marking]
\arrow[from=7-4, to=4-4, violet, crossing over]
\arrow[curve={height=-24pt}, from=7-4, to=1-1, violet, "\circ" marking]
\begin{comment}
\arrow[curve={height=-30pt}, from=4-8, to=10-4, olive, "\circ" marking]
\arrow[curve={height=24pt}, from=4-8, to=1-4, olive]
\arrow[from=4-9, to=4-8, magenta, "\circ" marking]
\arrow[from=4-10, to=4-9,magenta, "\circ" marking]
\arrow[from=6-10, to=4-10, violet]
\arrow[from=6-10, to=4-8, violet, "\circ" marking]
\arrow[from=10-10, to=6-10,violet]
\arrow[from=10-10, to=10-4, "\circ" marking, violet]
\arrow[curve={height=30pt}, from=13-4, to=10-10, violet]
\arrow[curve={height=-30pt}, from=13-4, to=4-1,"\circ" marking, violet]
\end{comment}
\end{tikzcd}. \tag{B}
\end{equation*}

We can build diagram (<ref>) below by noticing

\[ \label{eq alpha(a)} \pi u \pi_0 \pi_0 = \tilde{u} \pi_0 s \alpha \tag{a}\]

which means there is a unique map $(\tilde{u} \pi_0 s \alpha w , \pi u \pi_0 \pi_0) : \tilde{U} \to \csp$. Applying the internal Ore condition, Int.Frc.(3), witnesses the first (family of) Ore-square(s), $\theta_0: \hat{U}_8 \to W_\square$, and using diagram (<ref>) and equation $(a)$ above we can rewrite

\[ \hat{u}_9\pi u \pi_0 \pi_1 = \hat{u}_9 \tilde{u} \pi_0 (s \alpha w , 1) c = (\hat{u}_9 \tilde{u} \pi_0 s \alpha w , \hat{u}_9 \tilde{u} \pi_0) c = (\theta_0 \pi_1 \pi_1 w , \hat{u}_9 \tilde{u} \pi_0) c \]

and see its source coincides with the target of $\theta_0 \pi_1 \pi_0 : \hat{U}_8 \to W$ by definition of $W_\square$. This induces the unique map

\[ (\theta_0 \pi_1 \pi_0 , \pi u \pi_0 \pi_1) : \hat{U}_8 \to \mC_2. \]

Now the target of $\pi u \pi_0 \pi_1 : \tilde{U} \to \mC_1$ is the target of $\pi u \pi_1 \pi_0 : \tilde{U} \to W$ by definition of $\spn^2$, and this gives rise to the map

\[\big( (\theta_0 \pi_1 \pi_0 , \pi u \pi_0 \pi_1)c , \pi u \pi_1 \pi_0 \big) : \hat{U}_8 \to \csp\]

in diagram (<ref>) below. Applying Int.Frc.(3) here witnesses the second (family of) Ore-square(s), $\theta_1 : \hat{U}_7 \to W_\square$. The map representing pairs of composable arrows in $W$, that induce the cover $\tilde{u}_f$ and the lift $\omega_0: \hat{U}_6 \to W_\circ$ by Int.Frc.(2) in diagram (<ref>) below, are pretty self-explanatory. The one inducing $\omega_1 : \hat{U}_5 \to W_\circ $ can be justified by chasing through the already established parts of diagram (<ref>) below. First notice that

\[ \hat{u}_{7;8} \theta_0 \pi_0 \pi_1 = \hat{u}_{7;9} \tilde{u} \pi_0 s \alpha w \]

\[ \omega_0 \pi_1 = (\omega_0 \pi_0 \pi_0 , \theta_1 \pi_0 \pi_0 , \hat{u}_8 \theta_0 \pi_0 \pi_0 ) c .\]

The target of this last composite is the target of the last arrow which is the source

\[ \omega_0 \pi_1 w t = \hat{u}_{7;8} \theta_0 \pi_0 \pi_0 w t = \hat{u}_{7;8} \theta_0 \pi_0 \pi_1 s = \hat{u}_{7;9} \tilde{u} \pi_0 s \alpha w s. \]

Applying Int.Frc.(3) induces the map $\omega_1 : \hat{u}_5 \to W_\circ$ and all together we get a commuting diagram of witnesses to the the inner part of Figure (<ref>).

\begin{equation}\label{cover dgm - `inner' part}
\begin{tikzcd}[column sep = large]
W_\square \rar["(\pi_0 \pi_1 {,} \pi_1 \pi_1)"]
& \csp
\hat{U}_7
\uar["\theta_1", olive]
\rar["/" marking, "\hat{u}_8" near start]
& \hat{U}_8
\uar["\big( ( \theta_0 \pi_1 \pi_0 {,} \hat{u}_9 \pi u \pi_0 \pi_1 )c {,} \hat{u}_9 \pi u \pi_1 \pi_0 \big) "']
\dar["\theta_0"', olive]
\rar["/" marking, "\hat{u}_9" near start]
& \tilde{U}
\dar["( \tilde{u} \pi_0 s \alpha w{,}\pi u \pi_0 \pi_0)"]
\\
& W_\square \rar["(\pi_0 \pi_1 {,} \pi_1 \pi_1)"']
& \csp \\
\\
W_\circ \rar["(\pi_0 \pi_1 {,} \pi_0 \pi_2)"]
& W \prescript{}{wt}{\times_{ws}} W
\\
\hat{U}_5
\uar["\omega_1" violet]
\rar["/" marking, "\hat{u}_6" near start]
\uar["(\omega_0 \pi_1 {,} \hat{u}_{7;9} \tilde{u} \pi_0 s \alpha)"']
\dar["\omega_0"', violet]
\rar["/" marking, "\hat{u}_7" near start]
& \hat{U}_7 \dar["(\theta_1 \pi_0 \pi_0 {,} \hat{u}_8 \theta_0 \pi_0 \pi_0)"']
\\
& W_\circ \rar["(\pi_0 \pi_1 {,} \pi_0 \pi_2)"']
& W \prescript{}{wt}{\times_{ws}} W
\end{tikzcd} \tag{1}
\end{equation}

Applying Int.Frc(3) once followed by Int.Frc(4) twice gives local witnesses to the existence of the outer Ore-square and zippering arrows in magenta from Figure (<ref>). Note that the first and second magenta arrows equalize the parallel pairs obtained by going around either side of the Ore-square and ending at the domains of $\alpha(a)$ and $\alpha(b)$ respectively.

\begin{equation}\label{fig outer part 1}
\begin{tikzcd}[row sep = scriptsize, column sep = scriptsize]
&&& \cdot \\
&&& \cdot \\
\\
a & \cdot & a & b & \cdot & b & c & \cdot & \cdot & \cdot \\
&& \cdot \\
&&& \cdot &&b & &&& \\
&&& \cdot \\
&& \cdot && a \\
\\
&&& \cdot &&&&&&
\arrow[from=4-2, to=4-1, "\circ" marking, "\alpha(a)"', magenta]
\arrow[from=4-2, to=4-3 ,"\alpha(a)"', near end]
\arrow[from=4-3, to=4-4, "f"']
\arrow[curve={height=-12pt}, from=4-2, to=4-4, "\alpha(a) f"]
\arrow[from=4-5, to=4-4, "\circ" marking, "\alpha(b)"', magenta]
\arrow[from=4-5, to=4-6,"\alpha(b)"']
\arrow[from=4-6, to=4-7,"g"']
\arrow[curve={height=-12pt}, from=4-5, to=4-7, "\alpha(b) g"]
\arrow[curve={height=12pt}, from=2-4, to=4-2, "\circ" marking,, teal]
\arrow[curve={height=-12pt}, from=2-4, to=4-5, teal]
\arrow[from=1-4, to=2-4, teal]
\arrow[curve={height=25pt}, from=1-4, to=4-1, "\circ" marking, teal]
\arrow[from=8-3, to=4-1, "\circ" marking, orange, "\alpha(a)"']
\arrow[from=8-3, to=8-5, "\alpha(a)"' near end, orange]
\arrow[from=8-5, to=6-6, orange, "f"']
\arrow[from= 6-6, to=4-7, "g"', orange]
\arrow[from=5-3, to=4-2, olive]
\arrow[from=5-3, to=8-3, olive, "\circ" marking]
\arrow[from=6-4, to=5-3, olive, "\circ" marking]
\arrow[from=6-4, to=4-5, olive]
\arrow[from=7-4, to=6-4, violet]
\arrow[from=7-4, to=8-3, violet, "\circ" marking]
\arrow[from=10-4, to=7-4, violet, crossing over]
\arrow[curve={height=-24pt}, from=10-4, to=4-1, violet, "\circ" marking]
\arrow[curve={height=-30pt}, from=4-8, to=10-4, olive, "\circ" marking]
\arrow[curve={height=24pt}, from=4-8, to=1-4, olive]
\arrow[from=4-9, to=4-8, magenta, "\circ" marking]
\arrow[from=4-10, to=4-9,magenta, "\circ" marking]
\begin{comment}
\arrow[from=6-10, to=4-10, violet]
\arrow[from=6-10, to=4-8, violet, "\circ" marking]
\arrow[from=10-10, to=6-10,violet]
\arrow[from=10-10, to=10-4, "\circ" marking, violet]
\arrow[curve={height=30pt}, from=13-4, to=10-10, violet]
\arrow[curve={height=-30pt}, from=13-4, to=4-1,"\circ" marking, violet]
\end{comment}
\end{tikzcd} \tag{C}
\end{equation}

For the additional Ore-square added in (<ref>) recall the construction of the cover $u : u \to \spn^2$ and notice that target of the left leg of the composite coincides with the target of $\omega_1 \pi_1 : \hat{U}_5 \to W$,

\begin{align*}
\hat{u}_{6;9} \pi \sigma_\circ \pi_0 w t
&= \hat{u}_{6;9} \pi \omega \pi_1 w t \\
&= \hat{u}_{6;9} \pi u \pi_0 \pi_0 w t\\
&= \hat{u}_{6;9} s \alpha w t\\
&= \omega_1 \pi_0 \pi_2 w t\\
&= \omega_1 \pi_1 w t .
\end{align*}

This induces a unique map $(\omega_1 \pi_1 , \hat{u}_{6;9} \pi \sigma_\circ \pi_0 ) : \hat{U}_5 \to \csp$ which in turn gives a witnessing map $\theta_2 : \hat{U}_4 \to W_\square$ in diagram (<ref>) below. The map $\lambda' : \hat{U}_4 \to \cP_{cq} (\mC)$ is induced by $\lambda'' : \hat{U} \to P(\mC) \prescript{}{\pi_0 t}{\times_s} W$, which itself is induced by the universal property of the pullback $P(\mC) \prescript{}{\pi_0 t}{\times_s} W$ and can be defined explicitly as a pairing map by expanding each side of the equality determined by commutativity of the last Ore-square. Internally this is captured by the definition of $W_\square$ and the lift $\theta_2$ from . On one side of the equality we have

\begin{align}
\label{eq a side of outer Ore square}
\begin{split}
& \ \ \ \
( \theta_2 \pi_0 \pi_0 , \theta_2 \pi_0 \pi_1) c \\
&= (\theta_2 \pi_0 \pi_0 , \hat{u}_5 \omega_1 \pi_1)c \\
&= \big( \theta_2 \pi_0 \pi_0 , \hat{u}_5 ( \omega_1 \pi_0 \pi_0 , \hat{u}_6 \omega_0 \pi_1 , \hat{u}_{6;9} \tilde{u} \pi_0 s \alpha w )c \big)c \\
&= \big( \theta_2 \pi_0 \pi_0 , \hat{u}_5 \omega_1 \pi_0 \pi_0 , \hat{u}_{5;6} \omega_0 \pi_1 , \hat{u}_{5;9} \tilde{u} \pi_0 s \alpha w  \big)c \\
&=  \big( \theta_2 \pi_0 \pi_0 , \hat{u}_5 \omega_1 \pi_0 \pi_0 , \hat{u}_{5;6} (\omega_0 \pi_0 \pi_0 , \hat{u}_7 \theta_1 \pi_0 \pi_0, \hat{u}_{7;8} \theta_0 \pi_0 \pi_0) c ,  \hat{u}_{5;9} \tilde{u} \pi_0 s \alpha w   \big)c \\
&= \big( \theta_2 \pi_0 \pi_0 ,
\hat{u}_5 \omega_1 \pi_0 \pi_0 ,
\hat{u}_{5;6} \omega_0 \pi_0 \pi_0 , \hat{u}_{5;7 } \theta_1 \pi_0 \pi_0, \hat{u}_{5;8} ( \theta_0 \pi_0 \pi_0 w ,
\hat{u}_{9} \tilde{u} \pi_0 s \alpha w )c   \big)c\\
&= \big( \theta_2 \pi_0 \pi_0 ,
\hat{u}_5 \omega_1 \pi_0 \pi_0 ,
\hat{u}_{5;6} \omega_0 \pi_0 \pi_0 , \hat{u}_{5;7 } \theta_1 \pi_0 \pi_0, \hat{u}_{5;8} \theta_0 \pi_1 \pi_0 ,
\hat{u}_{5;9} \tilde{u} \pi_0 s \alpha w   \big)c
\end{split}
\end{align}

and on the other we have

\begin{align}
\label{eq other side of outer Ore square}
\begin{split}
& \ \ \ \ ( \theta_2 \pi_1 \pi_0 , \theta_2 \pi_1 \pi_1 w ) c \\
&= (\theta_2 \pi_1 \pi_0 , \hat{u}_{5;9} \pi \sigma_\circ \pi_0 w )c \\
&= (\theta_2 \pi_1 \pi_0 , \hat{u}_{5;9} \pi \omega \pi_1 w )c \\
&= 	\big(\theta_2 \pi_1 \pi_0 ,
\hat{u}_{5;9} \pi ( \omega \pi_0 \pi_0 ,
u_0 \theta \pi_0 \pi_0 w ,
u \pi_0 w )c
\big)c \\
&= \big(\theta_2 \pi_1 \pi_0 ,
\hat{u}_{5;9} \pi \omega \pi_0 \pi_0 ,
\hat{u}_{5;9} \pi u_0 \theta \pi_0 \pi_0 w ,
\hat{u}_{5;9} \pi u \pi_0 w
\big)c \\
&= \big(\theta_2 \pi_1 \pi_0 ,
\hat{u}_{5;9} \pi \omega \pi_0 \pi_0 ,
\hat{u}_{5;9} \pi u_0 \theta \pi_0 \pi_0 w ,
\hat{u}_{5;9} \tilde{u} \pi_0 s \alpha w
\big)c
\end{split}.
\end{align}

Notice that the last coordinates of the internal compositions described in the last lines of equations (<ref>) and (<ref>) coincide. Then the map $\lambda'' : \hat{U}_4 \to P(\mC) \prescript{}{t}{\times_{ws}} W$ is determined by the projections

\begin{align*}
\lambda'' \pi_1 &= \hat{u}_{5;9} \tilde{u} \pi_0 s \alpha w\\
\lambda'' \pi_0 \pi_0 &= (\theta_2 \pi_0 \pi_0 w ,
\hat{u}_5 \omega_1 \pi_0 \pi_0 ,
\hat{u}_{5;6} \omega_0 \pi_0 \pi_0 , \hat{u}_{5;7 } \theta_1 \pi_0 \pi_0, \hat{u}_{5;8} \theta_0 \pi_1 \pi_0 )c \\
\lambda'' \pi_0 \pi_1 &= (\theta_2 \pi_1 \pi_0 ,
\hat{u}_{5;9} \pi \omega \pi_0 \pi_0 ,
\hat{u}_{5;9} \pi u_0 \theta \pi_0 \pi_0 w) c .
\end{align*}

The left-hand sides of equations (<ref>) and (<ref>) are equal by definition of $W_\square$ and this induces the unique map $\lambda' : \hat{U}_4 \to \cP_{cq}(\mC)$ such that the triangle

[ ]
_cq() [tail, "ι_cq"]     P() t×_ws W

Û_4 [dotted, "λ'"] [ur, "λ"']

commutes by the universal property of the equalizer $\cP_{cq}(\mC)$. By definition of the pullback $\cP(\mC)$ we have

\[ \lambda \pi_0 \iota_{eq} \pi_1 = \lambda \pi_1 \iota_{cq} \pi_0 = \lambda ' \iota_{cq} \pi_0 = \lambda '' \pi_0 ,\]

so that

\begin{align} \label{eq pre-zip 0}
(\lambda \pi_0 \iota_{eq} \pi_0 w , \lambda'' \pi_0 \pi_0) c = (\lambda \pi_0 \iota_{eq} \pi_0 w , \lambda'' \pi_0 \pi_1) c.
\end{align}

\[ \label{def eta}\eta = ( \theta_2 \pi_0 \pi_0 w ,
\hat{u}_5 \omega_1 \pi_0 \pi_0 ,
\hat{u}_{5;6} \omega_0 \pi_0 \pi_0 , \hat{u}_{5;7 } \theta_1 \pi_1 \pi_0 )c \tag{Def. $\eta$} \]

and then by definition of the first two Ore-square maps in diagram (<ref>) we have

\begin{align}\label{eq pre zip 1a}
\begin{split}
& \ \ \ \ \big( \lambda '' \pi_0 \pi_0 , \hat{u}_{5;9} \pi u \pi_0 \pi_1 \big) c \\
&= \big( (\theta_2 \pi_0 \pi_0 w ,
\hat{u}_5 \omega_1 \pi_0 \pi_0 ,
\hat{u}_{5;6} \omega_0 \pi_0 \pi_0 , \hat{u}_{5;7 } \theta_1 \pi_0 \pi_0w , \hat{u}_{5;8} \theta_0 \pi_1 \pi_0 )c,
\hat{u}_{5;9} \pi u \pi_0 \pi_1 \big) c \\
&= \big( \theta_2 \pi_0 \pi_0 w ,
\hat{u}_5 \omega_1 \pi_0 \pi_0 ,
\hat{u}_{5;6} \omega_0 \pi_0 \pi_0 , \hat{u}_{5;7 } \theta_1 \pi_0 \pi_0 w, \hat{u}_{5;8}( \theta_0 \pi_1 \pi_0 ,
\hat{u} 9 \pi u \pi_0 \pi_1 ) c\big) c \\
&= \big( \theta_2 \pi_0 \pi_0 w ,
\hat{u}_5 \omega_1 \pi_0 \pi_0 ,
\hat{u}_{5;6} \omega_0 \pi_0 \pi_0 , \hat{u}_{5;7 } \theta_1 \pi_0 \pi_0 w, \hat{u}_{5;7} \theta_1 \pi_0 \pi_1 \big) c \\
&= \big( \theta_2 \pi_0 \pi_0 w ,
\hat{u}_5 \omega_1 \pi_0 \pi_0 ,
\hat{u}_{5;6} \omega_0 \pi_0 \pi_0 , \hat{u}_{5;7 } (\theta_1 \pi_0 \pi_0w , \theta_1 \pi_0 \pi_1)c \big) c \\
&= \big( \theta_2 \pi_0 \pi_0 w ,
\hat{u}_5 \omega_1 \pi_0 \pi_0 ,
\hat{u}_{5;6} \omega_0 \pi_0 \pi_0 , \hat{u}_{5;7 } (\theta_1 \pi_1 \pi_0 , \theta_1 \pi_1 \pi_1 w)c \big) c \\
&= \big( \theta_2 \pi_0 \pi_0 w ,
\hat{u}_5 \omega_1 \pi_0 \pi_0 ,
\hat{u}_{5;6} \omega_0 \pi_0 \pi_0 , \hat{u}_{5;7 } \theta_1 \pi_1 \pi_0 , \hat{u}_{5;9 } \pi u \pi_1 \pi_0 w \big) c \\
&= ( \eta , \hat{u}_{5;9 } \pi u \pi_1 \pi_0 w ) c
\end{split}.
\end{align}

It will help to define,

\[ \label{def nu} \nu = (\theta_2 \pi_1 \pi_0 ,
\hat{u}_{5;9} \pi \omega \pi_0 \pi_0 ,
\hat{u}_{5;9} \pi u_0 \theta \pi_1 \pi_0 w )c \tag{Def. $\nu$}\]

and by definition of the Ore-square in the definition of composition on representative spans, $\sigma_\circ : U \to \spn$, we have

\begin{align}\label{eq pre zip 1b}
\begin{split}
& \ \ \ \ \big( \lambda '' \pi_0 \pi_1 , \hat{u}_{5;9} \pi u \pi_0 \pi_1 \big) c \\
&= \big( (\theta_2 \pi_1 \pi_0 ,
\hat{u}_{5;9} \pi \omega \pi_0 \pi_0 ,
\hat{u}_{5;9} \pi u_0 \theta \pi_0 \pi_0 w) c ,
\hat{u}_{5;9} \pi u \pi_0 \pi_1 \big) c \\
&= \big( \theta_2 \pi_1 \pi_0 ,
\hat{u}_{5;9} \pi \omega \pi_0 \pi_0 ,
\hat{u}_{5;9} \pi u_0 ( \theta \pi_0 \pi_0 w ,
u_1 \pi_0 \pi_1)c \big) c \\
&= \big( \theta_2 \pi_1 \pi_0 ,
\hat{u}_{5;9} \pi \omega \pi_0 \pi_0 ,
\hat{u}_{5;9} \pi u_0 ( \theta \pi_0 \pi_0 w ,
\theta \pi_0 \pi_1 )c \big) c \\
&= \big( \theta_2 \pi_1 \pi_0 ,
\hat{u}_{5;9} \pi \omega \pi_0 \pi_0 ,
\hat{u}_{5;9} \pi u_0 ( \theta \pi_1 \pi_0 w ,
\theta \pi_1 \pi_1 )c \big) c \\
&= \big( \theta_2 \pi_1 \pi_0 ,
\hat{u}_{5;9} \pi \omega \pi_0 \pi_0 ,
\hat{u}_{5;9} \pi u_0 \theta \pi_1 \pi_0 w ,
\hat{u}_{5;9} \pi u \pi_1 \pi_0 w \big) c \\
&= (\nu , \hat{u}_{5;9} \pi u \pi_1 \pi_0 w )c
\end{split}
\end{align}

Putting equations (<ref>), (<ref>), and (<ref>) all together gives

\begin{align}\label{eq rho'' equalizes}
\begin{split}
(\lambda \pi_0 \iota_{eq} \pi_0 w , \hat{u}_4 \eta , \hat{u}_{4;9} \pi u \pi_1 \pi_0 w ) c
&=(\lambda \pi_0 \iota_{eq} \pi_0 w , \hat{u}_4 \lambda'' \pi_0 \pi_0 , \hat{u}_{4;9} \pi u \pi_0 \pi_1 )c \\
&= (\lambda \pi_0 \iota_{eq} \pi_0 w , \hat{u}_4 \lambda'' \pi_0 \pi_1 , \hat{u}_{4;9} \pi u \pi_0 \pi_1 ) c \\
&= (\lambda \pi_0 \iota_{eq} \pi_0 w ,  \hat{u}_4 \nu , \hat{u}_{4;9} \pi u \pi_1 \pi_0 w ) c
\end{split}
\end{align}

and induces the unique map $\rho'' : \hat{U}_3 \to P(\mC) \prescript{}{t}{\times_{ws}} W$ which is determined by the projections

\begin{align*}
\rho'' \pi_1 &= \hat{u}_{4;9} \pi u \pi_1 \pi_0 w , \\
\rho'' \pi_0 \pi_0 &= (\lambda \pi_0 \iota_{eq} \pi_0 w ,  \hat{u}_4 \eta)c , \\
\rho'' \pi_0 \pi_1 &= (\lambda \pi_0 \iota_{eq} \pi_0 w , \hat{u}_4 \nu)c .
\end{align*}

equation (<ref>) induces the unique map $\rho' : \hat{U}_3 \to \cP_{cq}(\mC)$ such that the triangle

[ ]
_cq() [tail, "ι_cq"]     P() t×_ws W

Û [dotted, "ρ'"] [ur, "ρ"']

commutes by the universal property of the equalizer, $\cP_{cq}(\mC)$.

\begin{equation}\label{cover dgm - `outer' part 1}
\begin{tikzcd}[column sep = large]
&\cP(\mC) \rar["\pi_1"']
& \cP_{cq}(\mC)
\\
\hat{U}_2
\dar["\rho"', magenta]
\rar["/" marking, "\hat{u}_3" near start]
& \hat{U}_3
\uar["\lambda", magenta]
\dar["\rho' "]
\rar["/" marking, "\hat{u}_4" near start]
& \hat{U}_4
\uar["\lambda'"']
\dar["\theta_2"', olive]
\rar["/" marking, "\hat{u}_5" near start]
& \hat{U}_5
\dar["(\omega_1 \pi_1 {,} \hat{u}_{6;9} \pi \sigma_\circ \pi_0 )"]
\\
\cP(\mC) \rar["\pi_1"']
& \cP_{cq}(\mC)
& W_\square \rar["(\pi_0 \pi_1 {,} \pi_1 \pi_1)"']
& \csp
\end{tikzcd}.\tag{2}
\end{equation}

Applying Int.Frc(2) three times gives a cover that witnesses everything in Diagram <ref>, and from there we can find two sailboats, $\varphi , \psi : \hat{U} \to \slb$, along with a comparison span, $\varphi p_1 = \psi p_1$, whose left leg is in $W$.

\begin{equation}\label{cover dgm - `outer' part 2}
\begin{tikzcd}[column sep = large]
W_\circ \rar["(\pi_0 \pi_1 {,} \pi_0 \pi_2)"]
& W \prescript{}{wt}{\times_{ws}} W
&W_\circ \rar["(\pi_0 \pi_1 {,} \pi_0 \pi_2)"]
& W \prescript{}{wt}{\times_{ws}} W \\
\hat{U}
\dar[shift right, "\psi"', teal]
\dar[shift left, "\varphi", orange]
\uar["\omega_4", violet]
\rar["/" marking, "\hat{u}_0" near start]
\uar["(\omega_3 \pi_1 {,} \hat{u}_{2;5} \omega_1 \pi_1)"']
\dar["\omega_3"', violet]
\rar["/" marking, "\hat{u}_1" near start]
\uar["\omega_2", violet]
\dar["(\omega_2 \pi_1 {,} \hat{u}_{2;4}\theta_2 \pi_0 \pi_0)"]
\rar["/" marking, "\hat{u}_2" near start]
\uar["(\rho \pi_0 \iota_{eq} \pi_0 {,} \hat{u}_3 \lambda \pi_0 \iota_{eq} \pi_0 )"]
\\
\slb
& W_\circ \rar["(\pi_0 \pi_1 {,} \pi_0 \pi_2)"']
& W \prescript{}{wt}{\times_{ws}} W
\end{tikzcd} \tag{3}
\end{equation}

For defining the sailboats above we should notice that commutativity of the first two Ore-squares and weak-composition triangle along with the commuting forks given by zippering imply that the composites of solid arrows in Figure <ref> below are equal.

\begin{equation}\label{fig right leg intermediate spans}
\begin{tikzcd}[row sep = scriptsize, column sep = scriptsize]
&&& \cdot \\
&&& \cdot \\
\\
a & \cdot & a & b & \cdot & b & c & \cdot & \cdot & \cdot \\
&& \cdot \\
&&& \cdot &&b & &&& \\
&&& \cdot \\
&& \cdot && a \\
\\
&&& \cdot &&&&&&
\arrow[from=4-2, to=4-1, "\circ" marking, "\alpha(a)"', dotted]
\arrow[from=4-2, to=4-3 ,"\alpha(a)"', dotted, near end]
\arrow[from=4-3, to=4-4, "f"',dotted]
\arrow[curve={height=-12pt}, from=4-2, to=4-4, "\alpha(a) f",dotted]
\arrow[from=4-5, to=4-4, "\circ" marking, "\alpha(b)"',dotted]
\arrow[from=4-5, to=4-6,"\alpha(b)"']
\arrow[from=4-6, to=4-7,"g"']
\arrow[curve={height=-12pt}, from=4-5, to=4-7, "\alpha(b) g"]
%\arrow[curve={height=12pt}, from=2-4, to=4-2, "\circ" marking,, teal]
\arrow[curve={height=-12pt}, from=2-4, to=4-5, teal]
\arrow[from=1-4, to=2-4, teal]
%\arrow[curve={height=25pt}, from=1-4, to=4-1, "\circ" marking, teal]
\arrow[from=8-3, to=4-1, "\circ" marking, orange, "\alpha(a)"', dotted]
\arrow[from=8-3, to=8-5, "\alpha(a)"' near end, orange]
\arrow[from=8-5, to=6-6, orange, "f"']
\arrow[from= 6-6, to=4-7, "g"', orange]
\arrow[from=5-3, to=4-2, olive, dotted]
\arrow[from=5-3, to=8-3, olive, "\circ" marking, dotted]
\arrow[from=6-4, to=5-3, olive, "\circ" marking, dotted]
\arrow[from=6-4, to=4-5, olive, dotted]
\arrow[from=7-4, to=6-4, violet, dotted]
\arrow[from=7-4, to=8-3, violet, "\circ" marking]
\arrow[from=10-4, to=7-4, violet, crossing over]
%\arrow[curve={height=-24pt}, from=10-4, to=4-1, violet, "\circ" marking]
\arrow[curve={height=-30pt}, from=4-8, to=10-4, olive, "\circ" marking]
\arrow[curve={height=24pt}, from=4-8, to=1-4, olive]
\arrow[from=4-9, to=4-8, magenta, "\circ" marking]
\arrow[from=4-10, to=4-9,magenta, "\circ" marking]
%\arrow[from=6-10, to=4-10, violet]
%\arrow[from=6-10, to=4-8, violet, "\circ" marking]
%\arrow[from=10-10, to=6-10,violet]
%\arrow[from=10-10, to=10-4, "\circ" marking, violet]
%\arrow[curve={height=30pt}, from=13-4, to=10-10, violet]
%\arrow[curve={height=-30pt}, from=13-4, to=4-1,"\circ" marking, violet]
\end{tikzcd}\tag{B}
\end{equation}

This is seen internally by first taking the equation

\[(\rho \pi_0 \iota_{eq} \pi_0 w ,  \rho \pi_0 \iota_{eq} \pi_1 \pi_0) c = (\rho \pi_0 \iota_{eq} \pi_0 w ,  \rho \pi_0 \iota_{eq} \pi_1 \pi_1) c \]

from the definition of the equalizer $\cP_{eq}(\mC)$, post-composing (in $\mC$) on both sides with $\hat{u}_{3;9} \pi u \pi_1 \pi_1 : \hat{U}_3 \to \mC_1$ and using associativity to get the equation

\begin{align}\label{eq final zip}
(\rho \pi_0 \iota_{eq} \pi_0 w , \rho \pi_0 \iota_{eq} \pi_1 \pi_0 , \hat{u}_{3;9} \pi u \pi_1 \pi_1 ) c
&= (\rho \pi_0 \iota_{eq} \pi_0 w , \rho \pi_0 \iota_{eq} \pi_1 \pi_1 , \hat{u}_{3;9} \pi u \pi_1 \pi_1 ) c,
\end{align}

and then expanding the latter composites on both sides to get

\begin{align*}
( \rho \pi_0 \iota_{eq} \pi_1 \pi_0 , \hat{u}_{3;9} \pi u \pi_1 \pi_1 ) c
&= \big( \rho \pi_1 \iota_{cq} \pi_0 \pi_0 , (\hat{u}_{3;9} \tilde{u} \pi_1 (s \alpha w , 1) c \big)c\\
&= (\hat{u}_3 \rho ' \iota_{cq} \pi_0 \pi_0 ,  \hat{u}_{3;9} \tilde{u} \pi_1s \alpha w , \hat{u}_{3;9} \tilde{u} \pi_1 ) c \\
&= (\hat{u}_3 \rho '' \pi_0 \pi_0 ,  \hat{u}_{3;9} \pi u \pi_1 \pi_0 w , \hat{u}_{3;9} \tilde{u} \pi_1 ) c \\
&= \big( \hat{u}_3 (\lambda \pi_0 \iota_{eq} \pi_0 w , \hat{u}_{4} \eta)c,  \hat{u}_{3;9} \pi u \pi_1 \pi_0 w , \hat{u}_{3;9} \tilde{u} \pi_1 \big) c \\
&= ( \hat{u}_3 ( \lambda \pi_0 \iota_{eq} \pi_0 w , \hat{u}_4 \eta,  \hat{u}_{4;9} \pi u \pi_1 \pi_0 w)c , \hat{u}_{3;9} \tilde{u} \pi_1 ) c \\
\end{align*}

from the left-hand side, and

\begin{align*}
( \rho \pi_0 \iota_{eq} \pi_1 \pi_1 , \hat{u}_{3;9} \pi u \pi_1 \pi_1 ) c
&= ( \rho \pi_1 \iota_{cq} \pi_0 \pi_1 , \hat{u}_{3;9} \tilde{u} \pi_1 (s \alpha w , 1)c ) c \\
&= ( \hat{u}_3 \rho' \iota_{cq} \pi_0 \pi_1 ,  \hat{u}_{3;9} \tilde{u} \pi_1 s \alpha w , \hat{u}_{3;9} \tilde{u} \pi_1 ) c \\
&= ( \hat{u}_3 \rho'' \pi_0 \pi_1 ,  \hat{u}_{3;9} \pi u \pi_1 \pi_0 w , \hat{u}_{3;9} \tilde{u} \pi_1 ) c \\
&= ( \hat{u}_3 ( \lambda \pi_0 \iota_{eq} \pi_0 w , \hat{u}_4 \nu)c ,  \hat{u}_{3;9} \pi u \pi_1 \pi_0 w , \hat{u}_{3;9} \tilde{u} \pi_1 ) c \\
&= ( \hat{u}_3 ( \lambda \pi_0 \iota_{eq} \pi_0 w , \hat{u}_4 \nu,  \hat{u}_{4;9} \pi u \pi_1 \pi_0 w)c , \hat{u}_{3;9} \tilde{u} \pi_1 ) c
\end{align*}

from the right-hand side. These expansions are used below in equation (<ref>) where we start establishing how the middle arrows for the sailboats picked out by $\varphi, \psi : \hat{U} \to \slb$ coincide. These middle arrows will be picked out by maps, $\mu_0, \mu_1 : \hat{U} \to \mC_1$, which will be internal composites, $\mu_0 = (\omega' ,\hat{u}_{0;2} \mu_0')c$ and $\mu_1 = (\omega', \hat{u}_{0;2} \mu_1')c$, for the arrow $\omega' :\hat{U} \to \mC_1$ that is defined after Figure (<ref>). The map picking out the part of the middle arrows in the sailboats determined by $\varphi : \hat{U} \to \slb$ is

\[ \mu_0' = (\rho \pi_0 \iota_{eq} \pi_0 w , \hat{u}_3 \lambda \pi_0 \iota_{eq} \pi_0 w , \hat{u}_{3;4} \theta_2 \pi_0 \pi_0 w , \hat{u}_{3;5} \omega_1 \pi_0 \pi_0 , \hat{u}_{3;6} \omega_0 \pi_1 w) c \]

and by expanding the composites with the definitions of $\theta_0, \theta_1,$ and $ \omega_0$ in <ref> along with the fact that $\pi u \pi_0 \pi_1 = \tilde{u} \pi_0 (s \alpha w , 1) c$ from $\ref{pb comp + representatives for L_1}$ we can see

\[ (\rho \pi_0 \iota_{eq} \pi_0 w , \hat{u}_3 \lambda \iota_{eq} \pi_0 w , \hat{u}_{3;4} \eta , \hat{u}_{3;9} \pi u \pi_0 \pi_1 ) c
= \big( \mu_0' , \hat{u}_{3;9} \tilde{u} c ( s \alpha w , 1) c \big)c . \]

The middle of the sailboats being picked out by $\psi$ are given explicitly by

\[ \mu_1' = (\rho \pi_0 \iota_{eq} \pi_0 w , \hat{u}_3 \lambda \pi_0 \iota_{eq} \pi_0 w , \hat{u}_{3;4} \theta_2 \pi_1 \pi_0) c .\]

Putting together equation (<ref>) with the expansions and definitions of $\mu_0'$ and $\mu_1'$ and the definitions (<ref>) and (<ref>) and the definition of $\sigma_\circ : U \to \spn$.

\begin{align}\label{eq mu_0' to mu_1'}
\begin{split}
\big( \mu_0' , \hat{u}_{3;9} \tilde{u} c ( s \alpha w , 1) c \big)c
&= \big( \rho \pi_0 \iota_{eq} \pi_0 w , \hat{u}_3 \lambda \iota_{eq} \pi_0 w , \hat{u}_{3;4} \eta , \hat{u}_{3;9} \pi u \pi_1 \pi_1 )c\\
&= \big( \rho \pi_0 \iota_{eq} \pi_0 w , \hat{u}_3 \lambda \iota_{eq} \pi_0 w , \hat{u}_{3;4} \nu , \hat{u}_{3;9} \pi u \pi_1 \pi_1 )c\\
&= \big(\mu_1' , \hat{u}_{3;9} \pi \sigma_\circ \pi_1)c
\end{split} .
\end{align}

The maps $\varphi$ and $\psi$ picking out the sailboats can be seen in Figure (<ref>) below as the appropriate composites of the solid arrows.

\begin{equation}\label{fig - witnessing sailboats}
\begin{tikzcd}[row sep = scriptsize, column sep = scriptsize]
&&& \cdot \\
&&& \cdot \\
\\
a & \cdot & a & b & \cdot & b & c & \cdot & \cdot & \cdot \\
&& \cdot \\
&&& \cdot &&b & &&& \cdot \\
&&& \cdot \\
&& \cdot && a \\
\\
&&& \cdot &&&&&& \cdot \\
\\
\\
&&& \cdot
\arrow[from=4-2, to=4-1, "\circ" marking, "\alpha(a)"', dotted]
\arrow[from=4-2, to=4-3 ,"\alpha(a)"', dotted, near end]
\arrow[from=4-3, to=4-4, "f"', dotted]
\arrow[curve={height=-12pt}, from=4-2, to=4-4, "\alpha(a) f", dotted]
\arrow[from=4-5, to=4-4, "\circ" marking, "\alpha(b)"', dotted]
\arrow[from=4-5, to=4-6,"\alpha(b)"']
\arrow[from=4-6, to=4-7,"g"']
\arrow[curve={height=-12pt}, from=4-5, to=4-7, "\alpha(b) g"]
\arrow[curve={height=12pt}, from=2-4, to=4-2, "\circ" marking,teal, dotted]
\arrow[curve={height=-12pt}, from=2-4, to=4-5, teal]
\arrow[from=1-4, to=2-4, teal]
\arrow[curve={height=25pt}, from=1-4, to=4-1, "\circ" marking, teal]
\arrow[from=8-3, to=4-1, "\circ" marking, orange, "\alpha(a)"']
\arrow[from=8-3, to=8-5, "\alpha(a)"' near end, orange]
\arrow[from=8-5, to=6-6, orange, "f"']
\arrow[from= 6-6, to=4-7, "g"', orange]
\arrow[from=5-3, to=4-2, olive, dotted]
\arrow[from=5-3, to=8-3, olive, "\circ" marking, dotted]
\arrow[from=6-4, to=5-3, olive, "\circ" marking, dotted]
\arrow[from=6-4, to=4-5, olive, dotted]
\arrow[from=7-4, to=6-4, violet, dotted]
\arrow[from=7-4, to=8-3, violet, "\circ" marking]
\arrow[from=10-4, to=7-4, violet, crossing over]
\arrow[curve={height=-24pt}, from=10-4, to=4-1, violet, "\circ" marking, dotted]
\arrow[curve={height=-30pt}, from=4-8, to=10-4, olive, "\circ" marking]
\arrow[curve={height=24pt}, from=4-8, to=1-4, olive]
\arrow[from=4-9, to=4-8, magenta, "\circ" marking, dotted]
\arrow[from=4-10, to=4-9,magenta, "\circ" marking, dotted]
\arrow[from=6-10, to=4-10, violet, dotted]
\arrow[from=6-10, to=4-8, violet, "\circ" marking]
\arrow[from=10-10, to=6-10,violet]
\arrow[from=10-10, to=10-4, "\circ" marking, violet, dotted]
\arrow[curve={height=30pt}, from=13-4, to=10-10, violet]
\arrow[curve={height=-30pt}, from=13-4, to=4-1,"\circ" marking, violet]
\end{tikzcd} \tag{C}
\end{equation}

Explicitly define $\omega' : \hat{U} \to \mC_1$ to be the composite of the weak-composition arrows in (<ref>),

\[ \label{def omega'} \omega' = (\omega_4 \pi_0 \pi_0 , \hat{u}_0 \omega_3 \pi_0 , \hat{u}_{0;1} \omega_2 \pi_0) c, \tag{Def. $\omega'$}\]

and then $\mu_0 : \hat{U} \to \mC_1$ by

\[ \label{def mu_0} \mu_0 = ( \omega' , \hat{u}_{0;2} \mu_0') c. \tag{Def. $\mu_0$} \]

By definition of $\omega_4 : \hat{U} \to W_\circ$ we have

\[ \omega_4 \pi_1 = (\mu_0 , \hat{u} \tilde{u} \pi_0 s \alpha w ) c \]

so the map $\varphi : \hat{U} \to \slb$, that picks out the sailboats in the bottom of Figure (<ref>) (consisting of orange and violet arrows and factoring through the bottom of the olive coloured Ore-square arrows), given by

\[ \label{def varphi} \varphi = \big( ( (\mu_0, \hat{u} \tilde{u} \pi_0 s \alpha w ), \omega_4 \pi_1), \hat{u} \tilde{u} c ( s \alpha w , 1) c \big) \tag{Def. $\varphi$} \]

is well-defined. Similarly define

\[ \label{def mu_1} \mu_1 = (\omega' , \hat{u}_{0;2} \mu_1')c \tag{ Def. $\mu_1$ }.\]

By the first zippering, $\lambda : \hat{U}_3 \to \cP(\mC)$, in (<ref>), in particular by $\lambda \pi_0 : \hat{U}_3 \to \cP_{eq}(\mC)$ and the equalizer in its codomain we have that

\begin{align*}
& \ \ \ \ (\hat{u}_{0;2}\mu_1' , \hat{u}_{0 ;9} \pi \omega \pi_0 \pi_0 , \hat{u} \pi u_0 \theta \pi_0 \pi_0 w)c \\
&= (\hat{u}_{0;2} \rho \pi_0 \iota_{eq} \pi_0 w , \hat{u}_{0;3} \lambda \pi_0 \iota_{eq} \pi_0 w , \hat{u}_{0;3} \lambda \pi_0 \iota_{eq} \pi_1 \pi_1)c \\
&= (\hat{u}_{0;2}\rho \pi_0 \iota_{eq} \pi_0 w , \hat{u}_{0;3} \lambda \pi_0 \iota_{eq} \pi_0 w , \hat{u}_{0;3} \lambda \pi_0 \iota_{eq} \pi_1 \pi_0)c
\end{align*}

where the second to last line comes from the definition of $\mu_0'$ and the Ore-square picked out by $\theta_0 : \hat{U}_8 \to W_\square$ and the last line is by definition of $\omega_4 : \hat{U} \to W_\circ$. This allows us to see

\begin{align*}
& \ \ \ \ (\mu_1 , \hat{u} \pi \sigma_\circ \pi_0 w) c\\
&= (\omega' , \hat{u}_{0;2}\mu_1' , \hat{u} \pi \omega \pi_0 \pi_0 , \hat{u} \pi u_0 \theta \pi_0 \pi_0 w, \hat{u} \pi u \pi_0 \pi_0 w) c \\
&= (\omega' , \hat{u}_{0;2} \mu_1' , \hat{u} \pi \omega \pi_0 \pi_0 \hat{u} \pi u_0 \theta \pi_0 \pi_0 w, \hat{u} \pi u \pi_0 \pi_0 w) c \\
&= (\omega' , \hat{u}_{0;2} \rho \pi_0 \iota_{eq} \pi_0 w , \hat{u}_{0;3} \lambda \pi_0 \iota_{eq} \pi_0 w , \hat{u}_{0;3} \lambda \pi_0 \iota_{eq} \pi_1 \pi_0, \hat{u} \pi u \pi_0 \pi_0 w)c
\\
&= (\omega ' , \hat{u}_{0;2} \mu_0' , \hat{u} \pi u \pi_0 \pi_0 w) \\
&= ( \mu_0, \hat{u} \tilde{u} \pi_0 s \alpha w) \\
&= \omega_4 \pi_1
\end{align*}

so that the map $\psi : \hat{U} \to \slb$ determined by

\[ \label{def psi} \psi = \big( ( ( \mu_1 , \hat{u} \pi \sigma_\circ \pi_0 ) , \omega_4 \pi_1 ), \hat{u} \pi \sigma_\circ \pi_1 \big) \tag{Def. $\psi$} \]

is well-defined. Notice the intermediate spans picked out by $\varphi$ and $\psi$ coincide due to the composites in Figure (<ref>) being equal. Formally, by (<ref>), (<ref>), and equation (<ref>), we can see

\begin{align}\label{eq varphi p_1}
\begin{split}
\varphi p_1
&= \varphi (\pi_0 \pi_1, (\pi_0 \pi_0 \pi_0 , \pi_1)c) \\
&= \big( \omega_4 \pi_1 , (\mu_0, \hat{u}_{3;9} \tilde{u} c ( s \alpha w , 1) c \big) c \\
&= \big( \omega_4 \pi_1 , (\omega' , \hat{u}_{0;2} \mu_0' , \hat{u}_{3;9} \tilde{u} c ( s \alpha w , 1) c \big) c \\
&= \big( \omega_4 \pi_1 , (\omega' , \hat{u}_{0;2} \mu_1' , \hat{u}_{3;9} \tilde{u} \pi \sigma_\circ \pi_1) c \big) c \\
&= \big( \omega_4 \pi_1 , (\mu_1, \hat{u} \tilde{u} \pi \sigma_\circ \pi_1) c \big) c\\
&= \psi (\pi_0 \pi_1, (\pi_0 \pi_0 \pi_0 , \pi_1)c) \\
&= \psi p_1
\end{split}
\end{align}

Also notice that by (<ref>),

\begin{align}\label{eq varphi p_0}
\begin{split}
\varphi p_0
&= \varphi ( \pi_0 \pi_0 \pi_1 , \pi_1) \\
&= \big( \hat{u} \tilde{u} \pi_0 s \alpha w , \hat{u} \tilde{u} c ( s \alpha w , 1) c \big) \\
&= \hat{u} \tilde{u} \big( \pi_0 s \alpha w , c ( s \alpha w , 1) c \big)
\end{split}
\end{align}

and by (<ref>),

\begin{align}\label{eq psi p_0}
\begin{split}
\psi p_0
&= \psi ( \pi_0 \pi_0 \pi_1 , \pi_1) \\
&= (\hat{u} \pi \sigma_\circ \pi_0 , \hat{u} \pi \sigma_\circ \pi_1 ) \\
&= \hat{u} \pi \sigma_\circ.
\end{split}
\end{align}

Putting equations (<ref>), (<ref>), and (<ref>) together gives

\begin{align*}
\hat{u} \tilde{u} \big( \pi_0 s \alpha w , c ( s \alpha w , 1) c \big) q
&= \varphi p_0 q \\
&= \varphi p_1 q\\
&= \psi p_1 q \\
&= \psi p_0 q \\
&= \hat{u} \pi \sigma_\circ q \\
&= \hat{u} \pi u c'\\
&= \hat{u} \tilde{u} \big( \pi_0 ( s \alpha {,} ( s \alpha w {,} 1) c ){,}\pi_1 ( s \alpha {,} ( s \alpha w {,} 1) c ) \big) c'
\end{align*}

and since $\hat{u} \tilde{u} : \hat{U} \to \mC_2$ is epic, we get

\[ \big( \pi_0 s \alpha w , c ( s \alpha w , 1) c \big) q = \big( \pi_0 ( s \alpha {,} ( s \alpha w {,} 1) c ){,}\pi_1 ( s \alpha {,} ( s \alpha w {,} 1) c ) \big) c' \]

as promised.

§.§.§ Inverting the Canonical Cartesian Cleavage

Now that we know $L : \mC \to \mCW$ is an internal functor, we can show that it satisfies an important property. The rest of this section consists of lemmas leading to Proposition <ref>, which shows that the localization functor, $L : \mC \to \mCW$, inverts $w : W \to \mC_1$ in the sense of the following definition.

We say a map $x : X \to \mC_1$ is invertible if there exists a map $x^{-1} : X \to \mC_1$ such that the diagrams

\[ \begin{tikzcd}
X \ar[drr, bend left, "x^{-1}"] \ar[ddr, bend right, "x"'] \ar[dr, dotted, "(x {,} x^{-1})"] \\
& \mC_2 \dar["\pi_0"'] \rar["\pi_1"] & \mC_1 \dar["s"] \\
& \mC_1 \rar["t"'] & \mC_1
\end{tikzcd} ,\qquad \qquad
\begin{tikzcd}
X \ar[drr, bend left, "x"] \ar[ddr, bend right, "x^{-1}"'] \ar[dr, dotted, "(x^{-1} {,} x)"] \\
& \mC_2 \dar["\pi_0"'] \rar["\pi_1"] & \mC_1 \dar["s"] \\
& \mC_1 \rar["t"'] & \mC_1
\end{tikzcd},\]

\[ \begin{tikzcd}
X \rar["(x{,} x^{-1})"] \dar["x"'] & \mC_2 \dar["c"] \\
\mC_1 \rar["s e "'] & \mC_1
\end{tikzcd},\qquad \text{ and } \qquad
\begin{tikzcd}
X \rar["(x^{-1}{,} x)"] \dar["x"'] & \mC_2 \dar["c"] \\
\mC_1 \rar["t e "'] & \mC_1
\end{tikzcd}\]

commute in $\cE$. In this case we say $x^{-1}$ is an inverse for $x$ in $\mC$.

The next definition describes what it means for an internal functor to invert a class of arrows in its domain.

We say an internal functor, $F : \mC \to \mD$ inverts $x : X \to \mC_1$ if there exists a map $F(x)^{-1} : X \to \mD_1$ such that $F(x)^{-1}$ is an inverse for the composite

\[ \begin{tikzcd}
X \rar["x"] \ar[dr, "F(x)"'] & \mC_1 \dar["F_1"] \\
& \mD_1
\end{tikzcd}\]

in $\mD_1$.

One might expect that internal functors preserve inverses, and sure enough the following lemma states and proves this:

If $x : X \to \mC_1$ is an arrow in $\cE$ that has an inverse $x^{-1} : X \to \mC_1$ and $F : \mC \to \mX$ is an internal functor, then the composite

\[\begin{tikzcd}
X \ar[dr, "F(x)"'] \rar["x"] & \mC_1 \dar["F_1"] \\
& \mD_1
\end{tikzcd}\]

has an inverse given by

\[\begin{tikzcd}
X \ar[dr, "F(x)^{-1}"'] \rar["x^{-1}"] & \mC_1 \dar["F_1"] \\
& \mD_1
\end{tikzcd}. \]

By functoriality we can compute

\begin{align*}
(F(X) , F(X)^{-1}) c
&= (x F_1 , x^{-1} F_1 ) c \\
&= (x , x^{-1}) c F_1 \\
&= x s e F_1 \\
&= x F_1 s e \\
&= F(X) s e
\end{align*}

\begin{align*}
(F(X)^{-1} , F(X)) c
&= (x^{-1} F_1 , x F_1 ) c \\
&= (x^{-1 , x}) c F_1 \\
&= x t e F_1 \\
&= x F_1 t e \\
&= F(X) t e
\end{align*}

and the result follows from Definition <ref>.

The following lemma shows how every span is equivalent to a canonical composite of spans and will be useful for proving our main result, Proposition <ref>. The idea is that every span, represented as

\[\begin{tikzcd}
c & a \lar["\circ" marking, "v"'] \rar["f"] & b,
\end{tikzcd}\]

is equivalent to a composite of the pair of composable spans, represented as

\[\begin{tikzcd}
c & a \lar["\circ" marking, "v"' near start] \rar[equals] & a & d \lar["\circ" marking, "\alpha(b)"'] \rar[rr,bend left = 40, "\alpha(a) f"] \rar[dashed, "\circ" marking, "\alpha(a)"] & a \rar[dashed, "f"] & b
\end{tikzcd}\]

in particular. This is translated to the following statement about internal categories.

The triangle

[column sep = huge]
[drrr, two heads, "q"'] [rrr, "( (π_0 , π_0 w s e)  ,  (π_0 w s α, (π_0 w s αw , π_1 )c ) )"]           ^2 ["c'"]

commutes in $\cE$.

Let $\gamma : \spn \to \spn^2$ be the unique pairing map

\[\gamma = \big( (\pi_0 {,} \pi_0 w s e) \ {,} \ (\pi_0 w s \alpha {,} (\pi_0 w s \alpha {,} \pi_1 )c ) \big).\]

Take the pullback of the cover $u : U \to \spn^2$, used to define $c' : \spn^2 \to \mCW_1$ in Lemmas <ref> and <ref>, along $\gamma$ to get a cover $\tilde{u} : \tilde{U} \to \spn$ that witnesses the span composition process for the family of composable spans represented by $\gamma$.

\[ \begin{tikzcd}[]
\tilde{U} \arrow[dr, phantom, "\usebox\pullback" , very near start, color=black] \dar["/" marking , "\tilde{u}" near start] \rar["\pi"] & U \dar["/" marking , "u" near start] \\
\spn \rar["\gamma"'] & \spn^2
\end{tikzcd}\]

It suffices to construct a (family of) sailboat(s) $\varphi : \tilde{U} \to \slb$ such that

\[ \varphi p_0 = \tilde{u} \quad \text{ and } \varphi p_1 = \pi \sigma_\circ \]

because that would give

\[ \tilde{u} q = \varphi p_0 q = \varphi p_1 q = \pi \sigma_\circ q = \pi u c' = \tilde{u} \gamma c' \]

and since $\tilde{u}$ is epic we could conclude that

\[ \gamma c' = q\]

as desired. This family of sailboats will be constructed using the definition of the span composition, but let us take a moment to consider how this works when $\cE = \Set$. In this case, for each $f : a \to b$ in $\mC_1$ and $u : a \to c$ in $W$ we have a diagram that looks like

\[\begin{tikzcd}
&& \cdot \\
&& \cdot \\
c & a & a & d & a & b
\arrow[from=3-2, to=3-1, "\circ" marking, "v"' near start]
\arrow[from=3-2, to=3-3, equals]
\arrow[from=3-5, to=3-6, "f"]
\arrow[from=3-4, to=3-3, "\circ" marking, "\alpha(a)"near start]
\arrow[from=3-4, to=3-5,"\circ" marking, "\alpha(a)"' near start]
\arrow[from=2-3, to=3-2, "\circ" marking, "v'"']
\arrow[from=2-3, to=3-4, "k"]
\arrow[curve={height=34pt}, from=3-3, to=3-6, "f"]
\arrow[from=1-3, to=2-3, "h"]
\arrow[curve={height=6pt}, from=1-3, to=3-1,"\circ" marking, "v''"']
\arrow[curve={height=-25pt}, from=3-4, to=3-6, "\alpha(a)f"]
\end{tikzcd}\]

which gives rise to the sailboat

[column sep = huge, row sep = huge]

c     a     b

[from=1-2, to=2-1, "∘" marking, "v”"']
[from=1-2, to=2-3, dotted, "h k α(a) f"]
[from=2-2, to=2-1, "∘" marking, "v"]
[from=2-2, to=2-3, "f"]
[from=1-2, to=2-2, "hv'"]

showing that the span $(u, f)$ is equivalent to the composite $(u, 1) * (\alpha(a) , \alpha(a) f)$. The map picking out such sailboats internally, $\varphi : \tilde{U} \to \slb$, can be constructed by picking out the corresponding arrows through the composition process witnessed by the cover $u : U \to \spn^2$. Explicitly, this is given by

\[ \varphi = \big( ( (		(\pi \omega \pi_0 \pi_0 , \pi u_0 \theta \pi_0 \pi_0 w )c ,
\tilde{u} \pi_0) ,
\pi \sigma_\circ \pi_0 ),
\tilde{u} \pi_1 \big) \]

and this is well-defined because $\tilde{u} \pi_0 = \tilde{u} \gamma \pi_0 \pi_0$ and the definition of $W_\circ$ shows

\begin{align*}
\big( (\pi \omega \pi_0 \pi_0 , \pi u_0 \theta \pi_0 \pi_0 w )c , \tilde{u} \pi_0 w \big) c
&= \big( \pi \omega \pi_0 \pi_0 , \pi u_0 \theta \pi_1 \pi_0, \tilde{u} \gamma \pi_0 \pi_0 w \big) c \\
&= \big( \pi \omega \pi_0 \pi_0 , \pi u_0 \theta \pi_0 \pi_0 w, \pi u \pi_0 \pi_0 w \big) c \\
&= \pi \omega \pi_1 w   \\
&= \pi \sigma_\circ \pi_0 w.
\end{align*}

We can immediately see that

\begin{align}\label{eq varphi p0 - factorization lemma for spans}
\varphi p_0 = \varphi (\pi_0 \pi_0 \pi_1 , \pi_1) = ( \tilde{u} \pi_0 , \tilde{u} \pi_1 ) = \tilde{u}
\end{align}

and by adding an identity map, $\tilde{U} \to \mC_1$, given by

\[\tilde{u} \pi_0 w s e = \tilde{u} \gamma \pi_0 \pi_1 = \pi u \pi_0 \pi_1 \]

into the following computation we can use the definition of $W_\square$, the fact that

\[ (\tilde{u} \pi_0 w s \alpha w , \tilde{u} \pi_1 ) c = \tilde{u} \gamma \pi_1 = \pi u \pi_1,\]

and the definition of $\sigma_\circ : U \to \spn$ in Lemma <ref>.

\begin{align*}
\varphi (\pi_0 \pi_0 \pi_0 , \pi_1) c
&= \big( (\pi \omega \pi_0 \pi_0 , \pi u_0 \theta \pi_0 \pi_0 w )c , \tilde{u} \pi_1 \big) c\\
&= (\pi \omega \pi_0 \pi_0 , \pi u_0 \theta \pi_0 \pi_0 w , \tilde{u} \pi_1 ) c\\
&= (\pi \omega \pi_0 \pi_0 , \pi u_0 \theta \pi_0 \pi_0 w, \tilde{u} \pi_0 w s e , \tilde{u} \pi_1 ) c\\
&= (\pi \omega \pi_0 \pi_0 , \pi u_0 \theta \pi_0 \pi_0 w, \pi u \pi_0 \pi_1 , \tilde{u} \pi_1 ) c\\
&= (\pi \omega \pi_0 \pi_0 , (\pi u_0 \theta \pi_0 \pi_0 w, \pi u \pi_0 \pi_1)c , \tilde{u} \pi_1 ) c\\
&= (\pi \omega \pi_0 \pi_0 , (\pi u_0 \theta \pi_1 \pi_0, \pi u \pi_1 \pi_0 w)c , \tilde{u} \pi_1 ) c\\
&= (\pi \omega \pi_0 \pi_0 , \pi u_0 \theta \pi_1 \pi_0, \tilde{u} \pi_0 w s \alpha w , \tilde{u} \pi_1 ) c\\
%&= \big( \pi \omega \pi_0 \pi_0 , \pi u_0 \theta \pi_1 \pi_0, \tilde{u} ( \pi_0 w s \alpha w , \pi_1)c \big) c\\
%&= \big( \pi \omega \pi_0 \pi_0 , \pi u_0 \theta \pi_1 \pi_0, \tilde{u} \gamma \pi_1 \big) c\\
%&= \big( \pi \omega \pi_0 \pi_0 , \pi u_0 \theta \pi_1 \pi_0, \pi u \pi_1 \big) c\\
&= \pi (\omega \pi_0 \pi_0 , u_0 \theta \pi_1 \pi_0, u \pi_1 ) c\\
&= \pi \sigma_\circ \pi_1.
\end{align*}

Now we can easily see

\begin{align}\label{eq varphi p1 - factorization lemma for spans}
\begin{split}\varphi p_1
&= \varphi \big(\pi_0 \pi_1 , (\pi_0 \pi_0 \pi_0 , \pi_1) c \big)\\
&= \big( \pi \sigma_\circ \pi_0 , \pi \sigma_\circ \pi_1) \\
&= \pi \sigma_\circ
\end{split}
\end{align}

The result follows from equations (<ref>) and (<ref>) as discussed at the beginning of this proof.

The next lemma is used to give an equivalent representation of the identity spans in $\mCW$ which we use in the proof of Proposition <ref>.

The diagram

W ["(1 ,w)"] ["wt"']     [two heads, "q"]

_0 ["(α, αw)q "']     _1

commutes, where $\alpha : \mC_0 \to W$ is a section of $wt : W \to \mC_0$ from .

By Int.Frc.(2) and Int.Frc.(3) there exist covers, $\tilde{u}_0$ and $\tilde{u}_1$, and lifts, $\tilde{\omega}$ and $\tilde{\theta}$, that make the squares in the following diagram commute respectively:

[column sep = huge]
W_∘["(π_0 π_1 , π_0 π_2)"]
W wt×_ws W

[dotted, "ω̃"]
["/" marking, "ũ_0" near start]
[dotted, "θ̃"']
["/" marking, "ũ_1" near start]
W ["(1,w t αw)"]

W_□["(π_0 π_1 , π_1 π_1)"']

The map $\tilde{\omega} \pi_1 : \tilde{U} \to W$ results in an intermediate (family of) span(s), $( \tilde{\omega} \pi_1 , \tilde{\omega} \pi_1 w) : \tilde{U} \to \spn$ and by definition of $W_\square$ and the maps in the diagram above we have that

\[ \tilde{\omega} \pi_1 = ( \tilde{\omega} \pi_0 \pi_0 , \tilde{u}_0 \tilde{\theta} \pi_0 \pi_0 w, \tilde{u} w) . \]

This gives a map $\tilde{U} \to W_\triangle$ and since $\slb = W_\triangle \tensor[_{\pi_0 \pi_1 s}]{\times}{_s} \mC_1$ we can see this determines a sailboat, $\varphi: \tilde{U} \to \slb$, given by the unique pairing map

\[ \varphi = \big( ( ( ( \tilde{\omega} \pi_0 \pi_0 , \tilde{u}_0 \tilde{\theta} \pi_0 \pi_0 w)c ,
\tilde{u} ),
\tilde{\omega} \pi_1),
\tilde{u} w\big). \]

Similarly, we have

\[ \tilde{\omega} \pi_1 = ( \tilde{\omega} \pi_0 \pi_0 , \tilde{u}_0 \tilde{\theta} \pi_1 \pi_0 , \tilde{u} w t \alpha w)\]

giving another unique map $\tilde{U} \to W_\triangle$ and determining a sailboat $\psi: \tilde{U} \to \slb$, by the unique pairing map

\[ \psi = \big( ( ( ( \tilde{\omega} \pi_0 \pi_0 , \tilde{u}_0 \tilde{\theta} \pi_1 \pi_0 )c ,
\tilde{u} w t \alpha ),
\tilde{\omega} \pi_1),
\tilde{u} w t \alpha w \big) .\]

First we can use the calculations and definitions above (along with the definition of the pullback projections and how they interact with pairing maps) to see

\begin{align*}
\varphi p_0
&= \varphi (\pi_0 \pi_0 \pi_1 , \pi_1) \\
&= \tilde{u} (1 , w)
\end{align*}

\begin{align*}
\varphi p_1
&= \varphi (\pi_0 \pi_1 , (\pi_0 \pi_0 \pi_0 , \pi_1)c) \\
&= (\tilde{\omega} \pi_1 , \tilde{\omega} \pi_1 w)\\ &= \tilde{\omega} (\pi_1 , \pi_1 w)
\end{align*}

as well as

\begin{align*}
\psi p_0
&= \psi (\pi_0 \pi_0 \pi_1 , \pi_1) \\
&= ( \tilde{u} w t \alpha , 	\tilde{u} w t \alpha w) \\
&= ( \tilde{u} w t ( \alpha , \alpha w)
\end{align*}

\begin{align*}
\psi p_1
&= \psi (\pi_0 \pi_1 , (\pi_0 \pi_0 \pi_0 , \pi_1)c) \\
&= (\tilde{\omega} \pi_1 , \tilde{\omega} \pi_1 w) \\
&= \tilde{\omega} (\pi_1 , \pi_1 w) .
\end{align*}

Putting it all together shows

\[ \tilde{u} (1 , w)q = \varphi p_0 q = \varphi p_1q = \psi p_1 q = \psi p_0 q = \tilde{u} w t ( \alpha , \alpha w) q \]

and since $\tilde{u}$ is epic we get that

\[ (1 , w)q = w t ( \alpha , \alpha w) q  \]

as desired.

An immediate corollary to Lemma <ref> is that the internal localization functor, $L : \mC \to \mCW$, maps the arrows from $w : W \to \mC_1$ to arrows in $\mCW$ that have left inverses.

The map $L_1 : \mC_1 \to \mCW_1$ has left inverses with respect to $w : W \to \mC_1$, in the sense that the diagram

[column sep = huge]
W ["( (1 , wse) q , w L_1 ) "] ["(1, w)"']     _2["c"]

["q "']     _1

Consider the following diagram.

[column sep = large]
W [dddlll, bend right = 35, "(1, w)"'] [ddd, "( ( 1 , w s e )  ,  ( w s αw , (w s α,w) c ) )"' ] [dddr, "( (1, wse)q , w L_1 )"]

[drrr, two heads, "q"'] [rrr, "( (π_0 , π_0 w s e)  ,  (π_0 w s α, (π_0 w s αw , π_1 )c ) )"]            ^2 ["c'"] [two heads, "q ×q"]     _2 [dl, "c"]

The bottom left triangle commutes by Lemma <ref>; the bottom right commutes by definition of $c$; the top left triangle commutes by the universal property of the pullback $\spn^2$; and the top right triangle commutes by the universal property of the pullback $\mCW_2$ along with the definitions of $L_1$ and $q \times q$. More precisely, post-composing the upper right triangle with the projection $\pi_1 : \mCW_2 \to \mCW_1$ gives precisely

\[ ( w s \alpha {,} (w s \alpha {,}w) c ) q = w ( s \alpha {,} ( s \alpha {,}1) c ) q = w L_1. \]

It follows that the diagram above commutes, in particular the outer square commutes.

Next we prove a lemma that shows the internal localization functor, $L : \mC \to \mCW$, maps arrows coming from $w : W \to \mC_1$ to arrows that have right inverses in $\mCW$.

The diagram

[column sep = huge]
W ["( w L_1 , (1 , wse) q ) "] ["w s(α, αw)"']     _2["c"]

["q "']     _1

Using the fact that

\[ ( w s \alpha {,} (w s \alpha {,}w) c ) q = w ( s \alpha {,} ( s \alpha {,}1) c ) q = w L_1\]

and the universal property of the pullback $\mCW_2$ we can see the top triangle in the diagram,

[column sep = large]
[rrrr, bend left = 40, "(w L_1 , ( 1 , wse) q ) "]
["(w s α, w s αw)"']
[rrr,"( ( w s α, ( w s αw , w ) c)  ,  (1 , w s e) ) "]           ^2 ["c'"] ["q ×q"]     _2 [dl, "c"]

[rrr,"q"']           _1

commutes. The right triangle commutes by definition so it suffices to show the bottom left square commutes.

Let $\gamma = \big( ( w s \alpha {,} ( w s \alpha w {,} w ) c) \ {,} \ (1 {,} w s e) \big)$ and take the pullback of the cover $u : U \to \spn^2$ along $\gamma$.

[column sep = huge]
Ũ [dr, phantom, "" , very near start, color=black] [r, "π"] ["/" marking , "ũ"' near end]    U ["/" marking , "u" near start]

W [r, "γ"']    ^2

The cover $\tilde{u} : \tilde{U} \to W$ witnesses the composition of the spans being picked out by $\gamma$. Thinking momentarily about the case when $\cE = \Set$ for visualization purposes, this says that for every arrow $v : a \to b$ in $W$ there exists a point in $\tilde{U}$ witnessing the commuting diagram:

\[ \begin{tikzcd}[column sep = large]
&&\cdot \\
&& \cdot \\
a & c & a & b & a & a
\arrow[from=3-3, to=3-4, "\circ" marking,"v" near start]
\arrow[from=3-2, to=3-1,"\circ" marking, "\alpha(a)"]
\arrow[from=3-2, to=3-3,"\circ" marking, "\alpha(a)" near end]
\arrow[from=3-5, to=3-4,"\circ" marking, "v" near end]
\arrow[from=3-5, to=3-6, equals]
\arrow[from=2-3, to=3-2,"\circ" marking, "v'"']
\arrow[curve={height=-6pt}, from=2-3, to=3-5, "k"]
\arrow[from=1-3, to=2-3,"h"]
\arrow[curve={height=18pt}, from=3-2, to=3-4, "\alpha(a) v"']
\arrow[from=1-3, to=3-1, bend right = 10, "\circ" marking, "v''"']
\end{tikzcd}\]

In this case the parallel pair of arrows, $hv' \alpha(a)$ and $hk$ being coequalized by $v : a \to b$ allows us to zipper before applying weak composition for $W$ to get a span whose left leg is in $W$, as pictured in the following diagram:

\[ \begin{tikzcd}[column sep = large]
& \cdot &\cdot \\
&&\cdot \\
&& \cdot \\
a & c & a & b & a & a
\arrow[from=4-3, to=4-4, "\circ" marking,"v" near start]
\arrow[from=4-2, to=4-1,"\circ" marking, "\alpha(a)"]
\arrow[from=4-2, to=4-3,"\circ" marking, "\alpha(a)" near end]
\arrow[from=4-5, to=4-4,"\circ" marking, "v" near end]
\arrow[from=4-5, to=4-6, equals]
\arrow[from=3-3, to=4-2,"\circ" marking, "v'"']
\arrow[curve={height=-6pt}, from=3-3, to=4-5, "k"]
\arrow[from=2-3, to=3-3,"h"]
\arrow[curve={height=18pt}, from=4-2, to=4-4, "\alpha(a) v"']
\arrow[from=2-3, to=4-1, bend right = 10, "\circ" marking, "v''"']
\arrow[from=1-3, to=2-3, "\circ" marking, "d"]
\arrow[from=1-2, to=1-3, "g"]
\arrow[from=1-2, to=4-1, bend right = 10, "\circ" marking, "v'''"']
\end{tikzcd}\]

The zippering axiom says there exists a map $d$ such that

\[ d h v' \alpha(a) = d h k \]

and the weak-composition axiom says there exists a map $g$ in the diagram above such that $gd v'' = v'''$ is in $W$. This data gives rise to two sailboats with a common projection,

[column sep = huge, row sep = large]
·[dl, "v”'"'] [dr, dotted, "gdhk"] [d, "gdhv'"']

a     c ["α(a)"] ["α(a)"']      a

[column sep = huge, row sep = large]
·[dl, "v”'"'] [dr, dotted, "gdhk"] [d, "gd'"']

a     ·["v”"] ["hk"']      a

implying that the composite of spans, $(\alpha(a) , \alpha(a) v) * (v , 1_a) = (v'' , hk)$, is equivalent to the span $(\alpha(a), \alpha(a))$ by transitivity. Translating this argument to the internal setting for $\cE$ not necessarily equal to $\Set$ amounts to defining the map $\delta : \tilde{U} \to \cP_{cq}(\mC)$ in the following diagram,

[column sep = large]
W_∘["(π_0 π_1 , π_0 π_2)"]
W wt×_ws W

["/" marking, "û_0" near start]

["/" marking, "û" near start]
["(δ̂ π_0 ι_eq π_0 , û_1 πσ_∘π_0) "']

_cq ()

applying Int.Frc(4) to get the cover $\hat{u}_1 : \hat{U}_0 \to \tilde{U}$ and the lift $\hat{\delta} : \hat{U}_1 \to \cP(\mC)$, and then applying by Int.Frc(2) to get the cover $\hat{u}_0 : \hat{U} \to \hat{U}_0$ and the lift $\hat{\omega} : \hat{U} \to W_\circ$.

The map $\delta : \tilde{U} \to \cP_{cq}(\mC)$ is induced by the universal property of the equalizer $\cP_{cq}(\mC)$ and the map $\delta' : \tilde{U} \to P(\mC) \prescript{}{t}{\times_{ws}} W$. The map $\delta'$ is induced by the universal property of the pullback $P(\mC) \prescript{}{t}{\times_{ws}} W$ and to define it we start by using the definition of $W_\square$ to see

\[ \label{eq inducing delta'} \pi (\omega \pi_0 \pi_0 , u_0 \theta \pi_0 \pi_0 w , u \pi_0 \pi_1)c = \pi (\omega \pi_0 \pi_0, u_0 \theta \pi_1 \pi_0, u \pi_1 \pi_0w) c \tag{$\star$} .\]

\[ \pi u \pi_0 \pi_1 = \tilde{u} \gamma \pi_0 \pi_1 = \tilde{u} (ws \alpha w, w)c \]

the left-hand side of equation (<ref>) becomes

\[ \pi (\omega \pi_0 \pi_0 ,  u_0 \theta \pi_0 \pi_0 w , u \pi_0 \pi_1) = (\pi \omega \pi_0 \pi_0 , \pi u_0 \theta \pi_0 \pi_0 w , \tilde{u} ws \alpha w, \tilde{u} w)c .\]

Rewriting equation (<ref>) while recalling that $\pi u = \tilde{u} \gamma$ and $\gamma \pi_1 \pi_0 = 1_W$ gives

\[ \label{eq inducing delta} (\pi \omega \pi_0 \pi_0 , \pi u_0 \theta \pi_0 \pi_0 w , \tilde{u} ws \alpha w, \tilde{u} w)c
= (\pi\omega \pi_0 \pi_0,\pi u_0 \theta \pi_1 \pi_0, \tilde{u} w) c \tag{$\star \star$} \]

and induces a unique $\delta' : \tilde{U} \to P(\mC) \prescript{}{t}{\times_{ws}} W$ such that

\begin{align*}
\delta' \pi_1 &= \tilde{u} \\
\delta' \pi_0 \pi_0 &= (\pi \omega \pi_0 \pi_0 , \pi u_0 \theta \pi_0 \pi_0 w , \tilde{u} ws \alpha w)c \\
\delta' \pi_0 \pi_0 &= (\pi\omega \pi_0 \pi_0,\pi u_0 \theta \pi_1 \pi_0)c .
\end{align*}

equation (<ref>) can then be simplified as

\begin{align*}
\delta' (\pi_0 \pi_0 , \pi_1)c = \delta' (\pi_0 \pi_1 , \pi_1)c
\end{align*}

which induces the unique map $\delta : \tilde{U} \to \cP_{cq}(\mC)$ such that

_cq() [tail, "ι_cq"]     P() t×_ws W

Ũ [ur, "δ'"'] [dotted, "δ"] .

The two (families of) sailboats, $\varphi , \psi : \hat{U} \to \slb$, with a common projection, $\varphi \pi_1 = \psi \pi_1$, can now be defined. By definition of

\[ W_\circ = (\mC_1 \tensor[_t]{\times}{_{ws}} W \tensor[_{wt}]{\times}{_{ws}} W ) \tensor[_c]{\times}{_{ws}} W \]

we have

\[ \hat{\omega} \pi_1 = ( \hat{\omega} \pi_0 \pi_0 , \hat{u}_0 \hat{\delta} \pi_0 \iota_{eq} \pi_0 w , \hat{u} \pi \sigma_\circ \pi_0 w)c \]

so let

\[ \mu_0 = ( \hat{\omega} \pi_0 \pi_0 , \hat{u}_0 \hat{\delta} \pi_0 \iota_{eq} \pi_0 w )c \]

to determine the unique pairing map

\[ \psi = \big( ( ( \mu_0,
\hat{u} \pi \sigma_\circ \pi_0 ),
\hat{\omega }\pi_1 ),
\hat{u} \pi ( \omega \pi_0 \pi_0,
u_0 \theta \pi_1 \pi_0)c \big). \]

Notice the last map in the composite

\[ \hat{u} \pi u \pi_1 \pi_1 = \hat{u} \tilde{u} w s e \]

is the identity structure map for $\mC$. The identity laws in $\mCW$ and $\mC$ can then both be used in the final calculation we need to determine the span projections for $\psi : \hat{U} \to \slb$.

\begin{align*}
(\hat{u} \pi \omega \pi_0 \pi_0, \hat{u} \pi u_0 \theta \pi_1 \pi_0)c
&= \hat{u} \pi (\omega \pi_0 \pi_0 , u_0 \theta \pi_1 \pi_0)c \\
&= (\hat{u} \pi \omega \pi_0 \pi_0 , \hat{u} \pi u_0 \theta \pi_1 \pi_0 )c \\
&= (\hat{u} \pi \omega \pi_0 \pi_0 , \hat{u} \pi u_0 \theta \pi_1 \pi_0(1, t e)c  )c \\
&= (\hat{u} \pi \omega \pi_0 \pi_0 , \hat{u} \pi u_0 \theta \pi_1 \pi_0, \hat{u} \pi u_0 \theta \pi_1 \pi_0 t e  )c \\
&= (\hat{u} \pi \omega \pi_0 \pi_0 , \hat{u} \pi u_0 \theta \pi_1 \pi_0, \hat{u} \pi u_0 \theta \pi_1 \pi_1 w s e  )c \\
&= (\hat{u} \pi \omega \pi_0 \pi_0 , \hat{u} \pi u_0 \theta \pi_1 \pi_0, \hat{u} \pi u \pi_1 \pi_0 w s e  )c \\
&= (\hat{u} \pi \omega \pi_0 \pi_0 , \hat{u} \pi u_0 \theta \pi_1 \pi_0, \hat{u} \pi u \pi_1 \pi_1 s e  )c \\
&= (\hat{u} \pi \omega \pi_0 \pi_0 , \hat{u} \pi u_0 \theta \pi_1 \pi_0, \hat{u} \tilde{ u} w s e s e  )c \\
&= (\hat{u} \pi \omega \pi_0 \pi_0 , \hat{u} \pi u_0 \theta \pi_1 \pi_0, \hat{u} \tilde{ u} w s e  )c \\
&= (\hat{u} \pi \omega \pi_0 \pi_0 , \hat{u} \pi u_0 \theta \pi_1 \pi_0, \hat{u} \pi u \pi_1 \pi_1 )c \\
&= \hat{u} \pi ( \omega \pi_0 \pi_0 , u_0 \theta \pi_1 \pi_0, u \pi_1 \pi_1  )c \\
&= \hat{u} \pi \sigma_\circ \pi_1
\end{align*}

Now we can see

\[ \psi p_0 = \psi (\pi_0 \pi_0 \pi_1 , \pi_1) = (\hat{u} \pi \sigma_\circ \pi_0 , \hat{u} \pi \sigma_\circ \pi_1) = \hat{u} \pi \sigma_\circ \]

\[ \psi p_1 = \psi (\pi_0 \pi_1 , (\pi_0 \pi_0 \pi_0 , \pi_1 )c ) = \big( \hat{\omega }\pi_1 , (\mu_0, \hat{u} \pi \omega \pi_0 \pi_0, \hat{u} \pi u_0 \theta \pi_1 \pi_0)c \big). \]

For $\varphi : \hat{U} \to \slb$ let

\[ \mu_1 = (\mu_0 , \hat{u} \pi \omega \pi_0 \pi_0 , \hat{u} \pi u_0 \pi_0 \pi_0w )c \]

and notice on one hand that

\[ (\mu_1 , \hat{u} \tilde{u} w s \alpha w )c = (\mu_1 , \hat{u} \pi u \pi_0 \pi_0 w) c = ( \mu_0 , \hat{u} \pi \sigma_\circ \pi_0 w)c = \hat{\omega} \pi_1\]

and on the other hand that

\begin{align*}
(\mu_1 , \hat{u} \tilde{u} w s \alpha w )c
&= (\hat{\omega} \pi_0 \pi_0 , \delta \pi_0 \iota_{eq} \pi_0 , \delta \pi_0 \iota_{eq} \pi_1 \pi_0)c\\
&= (\hat{\omega} \pi_0 \pi_0 , \delta \pi_0 \iota_{eq} \pi_0 , \delta \pi_0 \iota_{eq} \pi_1 \pi_1)c\\
&= (\mu_0 , \hat{u} \pi \omega \pi_0 \pi_0, \hat{u} \pi u_0 \theta \pi_1 \pi_0)c
\end{align*}

Then define

\[ \varphi = \big( ( ( \mu_1 ,
\hat{u} \tilde{u} w s \alpha ),
\hat{\omega} \pi_1 ),
\hat{u} \tilde{u} w s \alpha w \big) \]

and we get

\begin{align*}
\varphi p_0
&= (\pi_0 \pi_0 \pi_1 , \pi_1) \\
&= (\hat{u} \tilde{u} w s \alpha, \hat{u} \tilde{u} w s \alpha w)
\end{align*}

\begin{align*}
\varphi p_1
&= \varphi \big( \pi_0 \pi_1 , (\pi_0 \pi_0 \pi_0 , \pi_1)c \big) \\
&= \big( \hat{\omega} \pi_1 , \mu_1 , \hat{u} \tilde{u} w s \alpha w )c \big) \\
&= (\hat{\omega} \pi_1 , (\mu_0 , \hat{u} \pi \omega \pi_0 \pi_0, \hat{u} \pi u_0 \theta \pi_1 \pi_0)c \\
&= \psi p_1.
\end{align*}

Combining our computations gives us that

\begin{align*}
\hat{u} \tilde{u} (ws \alpha , ws \alpha w) q
&= \varphi p_0 q = \varphi p_1 q \\
&= \psi p_1 q = \psi p_0 q \\
&= \hat{u} \pi \sigma_\circ q \\
&= \hat{u} \pi u c' \\
&= \hat{u} \tilde{u} \gamma c'
\end{align*}

and since the composite $\hat{u} \tilde{u}$ is epic we can conclude

\[ (ws \alpha , ws \alpha w) q = \gamma c'. \]

Now we prove the second main result of this section.

The localization (internal) functor, $L : \mC \to \mCW$ inverts $w : W \to \mC_1$.

Consider the composite

\[ \begin{tikzcd}
W \rar["(1 {,} wse)"] \ar[dr] & \spn \dar[two heads, "q"] \\
& \mCW_1
\end{tikzcd}\]

In the proofs of Lemma <ref> and Corollary <ref> we have already seen that

\[ (1,wse) q s = w L_1 t , \qquad (1,wse) q t = w L_1 s\]

so it suffices to show the last two diagrams from Definition <ref> commute in this setting.

First note that $e = (\alpha, \alpha w) q : \mC_0 \to \mCW_1$ is the identity structure map on $\mCW$, and that the source map $s : \mCW_1 \to \mC_0$ is uniquely determined by the map $q s = \pi_0 w t : \spn \to \mC_0$. Also recall that

\[w L_1 = (w s \alpha , (w s \alpha , w ) c ) q \]

and then compute

\begin{align*}
w L_1 s e
&= w L_1 s (\alpha, \alpha w) q \\
&= (w s \alpha , (w s \alpha , w ) c ) q s (\alpha, \alpha w) q \\
&= (w s \alpha , (w s \alpha , w ) c ) \pi_0 w t (\alpha, \alpha w) q \\
&= w s \alpha w t (\alpha, \alpha w) q \\
&= w s (\alpha, \alpha w) q .
\end{align*}

We can replace the left and bottom composite in the commuting square of Lemma <ref> by the last equation to give the commuting square

[column sep = huge]
W ["( w L_1 , (1 , wse) q ) "]
["w L_1"']     _2["c"]

_1 ["s e "']     _1

in $\cE$ and shows $(1, w s e)q : W \to \mCW_1$ satisfies half of Definition <ref>. For the rest of it we recall that $q t = \pi_1 t : \spn \to \mC_0$ uniquely determines the structure map $t : \mCW_1 \to \mC_0$ and similarly compute

\begin{align*}
w L_1 t e
&= w L_1 t (\alpha, \alpha w) q \\
&= (w s \alpha , (w s \alpha , w ) c ) q t (\alpha, \alpha w) q \\
&= (w s \alpha , (w s \alpha , w ) c ) \pi_1 t (\alpha, \alpha w) q \\
&= (w s \alpha , w ) c t (\alpha, \alpha w) q \\
&= w t (\alpha, \alpha w) q .
\end{align*}

Putting this together with Lemma <ref> gives

\[ w L_1 t e = w t (\alpha, \alpha w) q = (1,w)q\]

and allows us to rewrite the commuting square in Corollary <ref> as

[column sep = huge]
W ["( (1 , wse) q , w L_1 ) "] ["w L_1"']     _2["c"]

_1 ["t e"']     _1

This means $(1 {,} wse) q $ inverts $(w L_1)$ by Definition <ref>.

§.§ Universal Property of Internal Fractions

The main result of this section is Theorem <ref>, the universal property of internal localization. It is an isomorphism of categories between the category of internal functors, $\mC \to \mD$, that invert $w : W \to \mC_1$ and their natural transformations, and the category of internal functors $\mCW \to \mD$ and their natural transformations. In Section <ref> we prove that the objects in each category uniquely correspond to one another in Proposition <ref>, and then in Lemma <ref> we show that the 2-cells in each category uniquely correspond to one another. In Lemma <ref> we show that the correspondence between natural transformations is functorial, and Theorem <ref> follows immediately.

§.§.§ Correspondence Between 1-cells

The results in this subsection come together to prove that for any internal functor $F : \mC \to \mX$ that inverts $w : W \to \mC_1$, there exists a unique internal functor $\lbrack F \rbrack : \mCW \to \mX$ such that the diagram

[dr, "L"'] [rr,"F"]

[ur, dotted, "F "']

commutes. First we define $[F]$ and prove it is an internal functor, then we notice how every internal functor $\mCW \to \mX$ corresponds to an internal functor $\mC \to \mX$ that inverts $W$ by pre-composition with $L : \mC \to \mX$. Finally we show that these assignments are inverses to one another to prove the main result of this subsection, Proposition <ref>.

It's clear how to define $[F]$ on objects:

[column sep = large]
_0 [equals] ["F _0"]     _0 [equals]

_0 [r, "F_0"']     _0

On arrows we use the universal property of the coequalizer $\mCW_1$. By Definition <ref>, there exists a map $F(w)^{-1} : W \to \mX_1$ that inverts $w F_1 : W \to \mX_1$ in $\mX$. That is, the diagrams

\[ \begin{tikzcd}[]
W\dar["wF_1"'] \rar[rr,"(w F_1 {,} F(w)^{-1})"] && \mX_2 \dar["c"] \\
\mX_1 \rar[rr,"se"'] && \mX_1
\end{tikzcd}\qquad \qquad \qquad
\begin{tikzcd}[]
W\dar["wF_1"'] \rar[rr,"( F(w)^{-1} {,} w F_1 )"] && \mX_2 \dar["c"] \\
\mX_1 \rar[rr,"te"'] && \mX_1
\end{tikzcd}\]

commute in $\cE$. In particular we have that

\[ F(w)^{-1} t = w F_1 s \]

and this along with functoriality of $F$ and the definition of $\spn = W \tensor[_{ws}]{\times}{_s} \mC_1$ is enough to see that the outside of the diagram,

[column sep = large]
["π_0"'] ["π_1"] [dr, dotted, "F '"]     _1 [dr, bend left, "F_1"]

W [dr, bend right, "F(w)^-1"']     _2 [dr, phantom, "" , very near start, color=black]
["π_1"] ["π_0"']     _1 ["s"]

_1 ["t"']     _0

commutes and induces the unique map $\lbrack F \rbrack' : \spn \to \mX_2$. This map is used to define $\lbrack F \rbrack_1 : \mCW_1 \to \mX_1$ in the following lemma by the universal property of the coequalizer $\mCW_1$.

The coequalizer diagram,

[shift left, "p_0"] [shift right, "p_1"']     ["F '"'] [two heads, "q"]     _1 [dotted, "F _1"]

_2 ["c"]     _1

commutes in $\cE$ and uniquely determines the map $\lbrack F \rbrack_1 : \mCW_1 \to \mX_1$.

The main idea here is that the left legs of the two spans inhabiting a sailboat, represented by $p_0 , p_1 : \slb \to \spn$, are arrows coming from $W$. These are part of a commuting triangle represented by $\pi_0 : \slb \to W_\triangle.$ More precisely, the left leg of the $p_1$ projection factors through the left leg of the $p_0$ projection by the arrow represented by the map $\pi_0 \pi_0 \pi_0 : \slb \to \mC_1$ in $\cE$. This is shown in the following calculation:

\begin{align*}
p_1 \pi_0 w
&= \pi_0 \pi_1 w\\
&= \pi_0 ( \pi_0 \pi_0 , \pi_0 \pi_1 w) c \\
&=( \pi_0 \pi_0 \pi_0 , \pi_0 \pi_0 \pi_1 w) c \\
&= ( \pi_0 \pi_0 \pi_0 , p_0 \pi_0 w) c
\end{align*}

Functoriality of $F$ then gives

\begin{align*}
p_1 \pi_0 w F_1
= ( \pi_0 \pi_0 \pi_0 F_1 , p_0 \pi_0 w F_1 ) c.
\end{align*}

The internal functor $F$ inverts the arrows coming from $w : W \to \mC_1$ so we can internally post-compose with $ p_0 \pi_0 F(w)^{-1} : \slb \to \mX_1$ to give the following calculation. This calculation uses associativity and the identity laws for internal composition in $\mX$, along with the definitions of $F(w)^{-1}$ and $\slb$ and functoriality of $F$.

\begin{align*}
(p_1 \pi_0 w F_1 , p_0 \pi_0 F(w)^{-1} ) c
&= (\pi_0 \pi_0 \pi_0 F_1
,p_0 \pi_0 w F_1
,p_0 \pi_0 F(w)^{-1} ) c\\
&= (\pi_0 \pi_0 \pi_0 F_1
,p_0 \pi_0
(w F_1 , F(w)^{-1} ) c )c \\
&= (\pi_0 \pi_0 \pi_0 F_1
,p_0 \pi_0 w F_1 s e)c \\
&= (\pi_0 \pi_0 \pi_0 F_1
, \pi_0 \pi_0 \pi_1 w F_1 s e)c \\
&= (\pi_0 \pi_0 \pi_0 F_1
, \pi_0 \pi_0 \pi_1 w s F_0 e)c \\
&= (\pi_0 \pi_0 \pi_0 F_1
, \pi_0 \pi_0 \pi_0 t F_0 e)c \\
&= (\pi_0 \pi_0 \pi_0 F_1
, \pi_0 \pi_0 \pi_0 F_1 t e)c \\
&= \pi_0 \pi_0 \pi_0 F_1 ( 1
, t e)c \\
&= \pi_0 \pi_0 \pi_0 F_1
\end{align*}

A similar internal composition involving the first and last terms in the equation above with $p_1 \pi_0 F(w)^{-1} : \slb \to \mX_1$ gives

\begin{align*}
( p_1 \pi_0 F(w)^{-1} , \pi_0 \pi_0 \pi_0 F_1 ) c
&= (p_1 \pi_0 F(w)^{-1} , p_1 \pi_0 w F_1 , p_0 \pi_0 F(w)^{-1} ) c \\
&= (p_1 \pi_0 (F(w)^{-1} ,w F_1)c , p_0 \pi_0 F(w)^{-1} ) c \\
&= (p_1 \pi_0 w F_1 t e , p_0 \pi_0 F(w)^{-1} ) c \\
&= (p_1 \pi_0 w t F_0 e , p_0 \pi_0 F(w)^{-1} ) c \\
&= (p_0 \pi_0 w t F_0 e , p_0 \pi_0 F(w)^{-1} ) c \\
&= (p_0 \pi_0 w F_1 t e , p_0 \pi_0 F(w)^{-1} ) c \\
&= (p_0 \pi_0 F(w)^{-1} s e , p_0 \pi_0 F(w)^{-1} ) c \\
&= p_0 \pi_0 F(w)^{-1} (s e , 1 ) c \\
&= p_0 \pi_0 F(w)^{-1}
\end{align*}

Now we can substitute the last equation into the following calculation to see $\lbrack F \rbrack' c$ coequalizes the pair $p_0$ and $p_1$:

\begin{align*}
p_0 \lbrack F \rbrack' c
&= p_0 (\pi_0 F(w)^{-1} , \pi_1 F_1)c \\
&= (p_0 \pi_0 F(w)^{-1} , p_0 \pi_1 F_1)c \\
&= \big(
( p_1 \pi_0 F(w)^{-1} , \pi_0 \pi_0 \pi_0 F_1 ) c ,
p_0 \pi_1 F_1 \big) c\\
&= ( p_1 \pi_0 F(w)^{-1} ,
\pi_0 \pi_0 \pi_0 F_1 ,
p_0 \pi_1 F_1 ) c\\
&= ( p_1 \pi_0 F(w)^{-1} ,
(\pi_0 \pi_0 \pi_0 F_1 ,
p_0 \pi_1 F_1) c ) c\\
&= ( p_1 \pi_0 F(w)^{-1} ,
(\pi_0 \pi_0 \pi_0,
p_0 \pi_1 ) c F_1 ) c\\
&= ( p_1 \pi_0 F(w)^{-1} ,
p_1 \pi_1 F_1 ) c\\
&= p_1 (\pi_0 F(w)^{-1} ,
\pi_1 F_1 ) c\\
&= p_1 \lbrack F \rbrack' c\\
\end{align*}

The existence and uniqueness of the map $\lbrack F \rbrack_1 : \mCW_1 \to \mX_1$ such that $q \lbrack F \rbrack_1 = \lbrack F \rbrack' c$ follows from the universal property of $\mCW_1$.

The next step is to show that $\lbrack F \rbrack = (\lbrack F \rbrack_0 , \lbrack F \rbrack_1)$ is an internal functor. First we show identities are preserved by proving the following lemma.

The diagram

\[ \begin{tikzcd}[]
\mC_0 \rar["F_0"] \dar["(\alpha {,} \alpha w)q"'] & \mX_0 \dar["e"] \\
\mCW_1 \rar["\lbrack F \rbrack_1"'] & \mX_1
\end{tikzcd}\]

commutes in $\cE$.

By the universal property of the pullback $\mX_2$, the definition of $F(w)^{-1}$, functoriality of $F$, and the fact that $\alpha$ is a section of $wt$ we have

\begin{align*}
(\alpha , \alpha w) q \lbrack F \rbrack_1
&= (\alpha , \alpha w) \lbrack F \rbrack' c \\
&= (\alpha , \alpha w) (\pi_0 F(w)^{-1} , \pi_1 F_1) c \\
&= (\alpha F(w)^{-1} , \alpha w F_1) c \\
&= \alpha ( F(w)^{-1} , w F_1) c \\
&= \alpha w F_1 t e \\
&= \alpha w t F_0 e \\
&= F_0 e
\end{align*}

The following lemma shows that $\lbrack F \rbrack$ preserves (internal) composition. When $\cE = \Set$ this is saying that for any pair of composable spans

\[ \begin{tikzcd}[]
a & b \lar["\circ" marking, "v"] \rar["f"] & c & d \lar["\circ" marking, "v'"] \rar["f'"]& e
\end{tikzcd}\]

with composite span,

\[ \begin{tikzcd}[]
a & b' \lar["\circ" marking, "v''"] \rar["f''"] & e
\end{tikzcd},\]

the diagram

\[ \begin{tikzcd}[]
F(a) \rar["F(v)^{-1} "] \dar[dd, "f(v'')^{-1} "'] & F(b) \rar["F(f)"] & F(c) \dar["f(v')^{-1} "] \\
& & F(d) \dar["F(f')"] \\
F(b') \rar[rr, "F(f'')"'] && F(e)
\end{tikzcd}\]

commutes in $\mX$. To see this we look at the composition data

\[\begin{tikzcd}
&& e \\
& {} & d \\
a & b & c & {b'} & {a'}
\arrow["v", from=3-2, to=3-1,"\circ" marking]
\arrow["f"', from=3-2, to=3-3]
\arrow["{v_0}"', from=2-3, to=3-2,"\circ" marking]
\arrow["h", from=1-3, to=2-3]
\arrow["{v'}", from=3-4, to=3-3,"\circ" marking]
\arrow["{f'}"', from=3-4, to=3-5]
\arrow["k", from=2-3, to=3-4]
\arrow["{v''}"', curve={height=6pt}, from=1-3, to=3-1,"\circ" marking]
\arrow["{f''}",curve={height=-6pt}, from=1-3, to=3-5]
\end{tikzcd}\]

and apply the functor $F$ to the weak-composition triangle on the left to get the equation

\[ F(v'') = F(h) F(v_0) F(v).\]

Since $F$ inverts $W$, we can pre-compose both sides by $F(v'')^{-1}$ and post-compose them both by $F(v)^{-1} $ to get the equation

\[ F(v)^{-1} = F(v'')^{-1} F(h) F(v_0). \]

Similarly, applying $F$ to the Ore-square gives the equation

\[ F(v_0) F(f) = F(k) F(v')\]

and post-composing with $F(v')^{-1}$ gives

\[ F(v_0) F(f) F(v')^{-1} = F(k). \]

Put it all together with functoriality of $F$ to see the square commutes.

\begin{align*}
F(v)^{-1} F(f) F(v')^{-1} F(f')
&= F(v'')^{-1} F(h) F(v_0) F(f) F(v')^{-1} F(f') \\
&=F(v'')^{-1} F(h) F(k) F(f')\\
&=F(v'')^{-1} F(f'')  .
\end{align*}

The diagram,

[column sep = large]
_2 ["c"'] ["F _1 ×F _1"]     _2 ["c"]

_1 ["F _1"']     _1

where $\lbrack F \rbrack_1 \times \lbrack F \rbrack_1 = (\pi_0 \lbrack F \rbrack_1 , \pi_1 \lbrack F \rbrack_1)$ is the unique pairing map, commutes in $\mX$.

Recall that $u : U \nrightarrow \spn \tensor[_t]{\times}{_s} \spn$ is the cover on which we defined composition, with $u = u_0 u_1$ in the diagram constructed by the Internal Fractions Axioms:

[column sep = huge ]
W_∘[rr, "(π_0 π_1 , π_0 π_2)"]
W ×__0 W

[rr, "/" marking , "u_0" near start]

["(θπ_0 π_0 ,  u_1 π_0 π_0) "']

["/" marking , "u_1" near start]
["( π_0 π_1 ,  π_1 π_0)"]

W_□["(π_0 π_1 , π_1 π_1)"']

We use this cover when we need to show certain maps out of $\spn \tensor[_t]{\times}{_s} \spn$ are equal. More precisely, by showing it (or its composition with other epimorphisms) equalizes two maps we are interested in proving are equal. We begin this proof with the weak-composition triangle, $\omega : U \to W_\circ$, and the equation encoding it is commutativity.

\[ \omega_0 \pi_1 = (\omega_0 \pi_0 \pi_0 , u_0 \theta \pi_0 \pi_0 w , u \pi_0 \pi_0 w ) c \]

By functoriality of $F$ we have

\[ \omega \pi_1 w F_1 = (\omega_0 \pi_0 \pi_0 F_1 , u_0 \theta \pi_0 \pi_0 w F_1 , u \pi_0 \pi_0 w F_1 ) c .\]

We can internally pre-compose both sides of $\mX$ with the map $\omega \pi_1 F(w)^{-1} : U \to \mX_1$ and internally post-compose with $u \pi_0 \pi_0 F(w)^{-1} : U \to \mX_1$. Before writing down the new equation however we do the following intermediate calculation:

\begin{align*}
(\omega \pi_1 F(w)^{-1} , \omega \pi_1w F_1)c
&= \omega \pi_1 (F(w)^{-1} , w F_1)c\\
&= \omega \pi_1 w F_1 t e \\
&= \omega \pi_1 w t e F_1 \\
&= u \pi_0 \pi_0 w t e F_1 \\
&= u \pi_0 \pi_0 w F_1 t e\\
&= u \pi_0 \pi_0 F(w)^{-1} s e
\end{align*}

Using this along with the definitions of $W_\square$, $\theta$, and $\csp$ gives

\begin{align*}
( u \pi_0 \pi_0 w F_1 , u \pi_0 \pi_0 F(w)^{-1} ) c
&= u \pi_0 \pi_0 ( w F_1, F(w)^{-1})c \\
&= u \pi_0 \pi_0 w F_1 s e \\
&= u \pi_0 \pi_0 w s e F_1 \\
&= u_0 u_1 \pi_0 \pi_1 w t e F_1 \\
&= u_0 \theta \pi_0 \pi_0 w t e F_1\\
&= u_0 \theta \pi_0 \pi_0 w F_1 t e.
\end{align*}

Now the pre/post-composed equation is

\begin{align*}
& \ \ \ \ ( u \pi_0 \pi_0 F(w)^{-1} s e , u \pi_0 \pi_0 F(w)^{-1})c\\
& = = (\omega \pi_1 F(w)^{-1} , \omega_0 \pi_0 \pi_0 F_1 , u_0 \theta \pi_0 \pi_0 w F_1, u_0 \theta \pi_0 \pi_0 w F_1 t e )c
\end{align*}

where the left side simplifies via the identity law in $\mX$ as

\[ ( u \pi_0 \pi_0 F(w)^{-1} s e , u \pi_0 \pi_0 F(w)^{-1})c = u \pi_0 \pi_0 F(w)^{-1} (s e , 1 )c = u \pi_0 \pi_0 F(w)^{-1} \]

and the right side simplifies similarly as

\begin{align*}
& \ \ \ \ (\omega \pi_1 F(w)^{-1} , \omega_0 \pi_0 \pi_0 F_1 , u_0 \theta \pi_0 \pi_0 w F_1, u_0 \theta \pi_0 \pi_0 w F_1 t e)c \\
&= \big(\omega \pi_1 F(w)^{-1} , \omega_0 \pi_0 \pi_0 F_1 ,
u_0 \theta \pi_0 \pi_0 w F_1(1, t e)c \big) c \\
&= \big(\omega \pi_1 F(w)^{-1} , \omega_0 \pi_0 \pi_0 F_1 ,
u_0 \theta \pi_0 \pi_0 w F_1 \big) c
\end{align*}

giving the simplified equation:

\[ \label{eq F(wc triangle) conj'd simp'd}
u \pi_0 \pi_0 F(w)^{-1} = \big(\omega \pi_1 F(w)^{-1} , \omega_0 \pi_0 \pi_0 F_1 ,
u_0 \theta \pi_0 \pi_0 w F_1 \big) c \tag{$\star$}. \]

Now take the Ore-square, $u_0 \theta : U \to W_\square$, and the equation describing commutativity,

\[ (u_0 \theta \pi_0 \pi_0 w , u \pi_0 \pi_1) c = (u_0 \theta \pi_1 \pi_0 , u \pi_1 \pi_0 w)c , \]

and apply $F$ to get the equation

\[ (u_0 \theta \pi_0 \pi_0 wF_1 , u \pi_0 \pi_1 F_1) c = (u_0 \theta \pi_1 \pi_0 F_1 , u \pi_1 \pi_0 w F_1 )c .\]

Since $F$ inverts $w: W \to \mC_1$ we can post-compose both sides with $u \pi_1 \pi_0 F(w)^{-1} : U \to \mX_1$ to get a new equation. The following computation showing how this is done follows more or less by the definitions of $F(w)^{-1}$ and $\theta$ and functoriality of $F$:

\begin{align*}
( u \pi_1 \pi_0 w F_1 , u \pi_1 \pi_0 F(w)^{-1}) c
&= u \pi_1 \pi_0 (w F_1 , F(w)^{-1}) c \\
&= u \pi_1 \pi_0 w F_1 s e \\
&= u \pi_1 \pi_0 w s e F_1 \\
&= u_0 \theta \pi_1 \pi_0 t e F_1 \\
&= u_0 \theta \pi_1 \pi_0 F_1 t e
\end{align*}

Adding internal composition with $u_0 \theta \pi_1 \pi_0 F_1 : U \to \mX_1$ on the right of both side of the internal compositions shown in the last equation and applying the identity law in $\mX$ gives:

\begin{align*}
(u_0 \theta \pi_1 \pi_0 F_1 , u \pi_1 \pi_0 w F_1 , u \pi_1 \pi_0 F(w)^{-1} )c
&= (u_0 \theta \pi_1 \pi_0 F_1 , u_0 \theta \pi_1 \pi_0 F_1 t e ) c \\
&= u_0 \theta \pi_1 \pi_0 F_1 (1 , te) c\\
&= u_0 \theta \pi_1 \pi_0 F_1.
\end{align*}

Then by the definition of $W_\square$ we get the equation

\begin{align*}
& \ \ \ \ (u_0 \theta \pi_0 \pi_0 wF_1 , u \pi_0 \pi_1 F_1 , u \pi_1 \pi_0 F(w)^{-1}) c \\
&= ((u_0 \theta \pi_0 \pi_0 w F_1 , u \pi_0 \pi_1 F_1)c , u \pi_1 \pi_0 F(w)^{-1}) c \\
&= ((u_0 \theta \pi_1 \pi_0 F_1 , u \pi_1 \pi_0 w F_1)c , u \pi_1 \pi_0 F(w)^{-1}) c \\
&= (u_0 \theta \pi_0 \pi_0 wF_1 , u \pi_0 \pi_1 F_1 , u \pi_1 \pi_0 F(w)^{-1}) c \\
&=u_0 \theta \pi_1 \pi_0 F_1. \tag{$\star \star$}
\end{align*}

which simplifies to the equality

\[ \label{eq F(ore sqr) conj'd simp'd} (u_0 \theta \pi_0 \pi_0 wF_1 , u \pi_0 \pi_1 F_1 , u \pi_1 \pi_0 F(w)^{-1}) c
= u_0 \theta \pi_1 \pi_0 F_1. \tag{$\star \star$} \]

which we use in following calculation that shows $[F]$ preserves composition. By equations (<ref>) and (<ref>) along with functoriality of $F$ and the identity law in $\mX$ we have:

\begin{align*}
& \ \ \ \ u (q \times q) c \lbrack F \rbrack_1 \\
&= u c' \lbrack F \rbrack_1 \\
&= \sigma_c q \lbrack F \rbrack_1 \\
&= \sigma_c \lbrack F \rbrack ' \\
&= (\sigma_c \pi_0 F(w)^{-1} , \sigma_c \pi_1 F_1) c  \\
&= (\omega \pi_1 F(w)^{-1} , \omega \pi_0 \pi_0 F_1 , u_0 \theta \pi_1 \pi_0 F_1, u \pi_1 \pi_1 F_1 ) c \\
&= (\omega \pi_1 F(w)^{-1} , \omega \pi_0 \pi_0 F_1 , u_0 \theta \pi_0 \pi_0 wF_1 , u \pi_0 \pi_1 F_1 , u \pi_1 \pi_0 F(w)^{-1} , u \pi_1 \pi_1 F_1 ) c \\
&= ((\omega \pi_1 F(w)^{-1} , \omega \pi_0 \pi_0 F_1 , u_0 \theta \pi_0 \pi_0 wF_1 )c , u \pi_0 \pi_1 F_1 , u \pi_1 \pi_0 F(w)^{-1} , u \pi_1 \pi_1 F_1 ) c \\
&= (u \pi_0 \pi_0 F(w)^{-1} , u \pi_0 \pi_1 F_1 , u \pi_1 \pi_0 F(w)^{-1} , u \pi_1 \pi_1 F_1 ) c \\
&= \big( u \pi_0 (\pi_0 F(w)^{-1} , \pi_1 F_1)c , u \pi_1 (\pi_0 F(w)^{-1} , \pi_1 F_1 )c \big) c \\
&= \big( u \pi_0 \lbrack F \rbrack' c , u \pi_1 \lbrack F \rbrack' c \big) c \\
&= u \big( \pi_0 q \lbrack F \rbrack_1 , \pi_1 q \lbrack F \rbrack_1 \big) c \\
&= u (q \times q) (\lbrack F \rbrack_1 \times \lbrack F \rbrack_1) c .
\end{align*}

The composite $u (q \times q)$ is epic, so we get

\[ c \lbrack F \rbrack_1 = (\lbrack F \rbrack_1 \times \lbrack F \rbrack_1) c \]

as desired.

The maps $\lbrack F \rbrack_0 = F_0 : \mC_0 \to \mX_0$ and $\lbrack F \rbrack_1 : \mCW_1 \to \mX_1$ determine an internal functor $\lbrack F \rbrack : \mCW \to \mX$ such that the diagram

\[ \begin{tikzcd}[]
\mC \rar[rr, "F"] \ar[dr, "L"'] & & \mX\\
& \mCW \ar[ur, "\lbrack F \rbrack"']
\end{tikzcd}\]

commutes in $\cE$.

Functoriality follows from Lemma <ref> and Lemma <ref>. To see the diagram commutes we can immediately see

\[ L_0 \lbrack F \rbrack_0 = 1_{\mC_0} F_0 = F_0 \]

and then use the definitions of $L_1$, $\lbrack F \rbrack_1$, and $\lbrack F \rbrack'$, along with functoriality of $F$, the identity law, $(se , 1) c =1$, in $\mX$, and the fact that $\alpha$ is a section of $wt$ to compute

\begin{align*}
L_1 \lbrack F \rbrack_1
&= (s \alpha , (s \alpha w , 1) c) q \lbrack F \rbrack_1 \\
&= (s \alpha , (s \alpha w , 1) c) \lbrack F \rbrack' c\\
&= (s \alpha , (s \alpha w , 1) c) (\pi_0 F(w)^{-1} , \pi_1 F_1) c\\
&=(s \alpha F(w)^{-1} , (s \alpha w , 1) c F_1) c\\
&=(s \alpha F(w)^{-1}, s \alpha wF_1 , F_1) c\\
&= (s \alpha (F(w)^{-1} , w F_1) c , F_1)c \\
&= (s \alpha w F_1 t e , F_1) c \\
&= (s \alpha w t e F_1 , F_1) c \\
&= (s e F_1 , F_1) c \\
&= (F_1 se , F_1) c\\
&= F_1 (se , 1) c\\
&= F_1.
\end{align*}

Every internal functor $F : \mC \to \mX$ that inverts $w : W \to \mC_1$ corresponds uniquely to an internal functor $ [F] : \mCW \to \mX$.

Lemma <ref> implies the forward direction. Now notice that for any internal functor $G : \mCW \to \mX$, there is an internal functor $LG : \mC \to \mX$ given by pre-composing with the localization functor $L : \mC \to \mCW$. In Proposition <ref> we saw that $L$ inverts $w : W \to \mC_1$, with $(wL)^{-1} = ( 1 , w s e) q : W \to \mCW_1$. Functoriality of $G$ implies $(wL)^{-1} G_1 : W \to \mX_1$ is an inverse of $wLG : W \to \mX_1$ in $\mX$ so this establishes the other direction of the correspondence.

For any $F : \mC \to \mX$ inverting $w : W \to \mC_1$, let $[F] : \mCW \to \mX$ be the corresponding internal functor. Pre-composing with $L : \mC \to \mX$ gives

\[ L [F] = F\]

so composing the assignments in one direction gives an identity. On the other hand, for any $G : \mCW \to \mX$, if we pre-compose with $L : \mC \to \mCW$ and then find the corresponding internal functor $\mCW \to \mX$ we get that

\[ [LG] : \mCW \to \mX \]

where $q [LG] = [LG]' c : \spn \to \mX_1$. Now expanding this with the explicit definition of

\[ [LG]' = (\pi_0 (LG)(w)^{-1} , \pi_1 (LG)_1 ) \]

we can use the definition

\[ (LG)(w)^{-1} = (wL)^{-1} G_1 = (1, wse)q G_1 ,\]

functoriality of $L$ and $G$, the definition

\[ L_1 = (s\alpha, (s \alpha w, 1)c )q ,\]

a bit of factoring with pairing maps, the fact that $q_2 c = c' : \spn \tensor[_t]{\times}{_s} \spn \to \spn$, and Lemma <ref> in the last line to see:

\begin{align*}
&= (\pi_0 (LG)(w)^{-1} , \pi_1 (LG)_1 )c \\
&= (\pi_0 (wL)^{-1} G_1 , \pi_1 L_1 G_1 )c \\
&=(\pi_0 (wL)^{-1} , \pi_1 L_1 )c G_1 \\
&=(\pi_0 (1 , w s e)q , \pi_1 (s\alpha, (s \alpha w, 1)c )q ) c G_1 \\
&=(( \pi_0 , \pi_0 w s e ) q , (\pi_1 s\alpha, (\pi_1 s \alpha w, \pi_1)c )q ) c G_1 \\
&=(( \pi_0 , \pi_0 w s e ) , (\pi_0 s\alpha, (\pi_0 s \alpha w, \pi_1)c ) q_2 c G_1 \\
&=(( \pi_0 , \pi_0 w s e ) , (\pi_0 s\alpha, (\pi_0 s \alpha w, \pi_1)c ) c' G_1 \\
&= q G_1
\end{align*}

This implies that $[LG] = G_1$ by the universal property of the coequalizer $\mCW_1$. We have shown that the assignments in either direction are inverses to one another, so this correspondence is unique.

§.§.§ Correspondence Between 2-Cells

Next we show the 2-cell correspondence between internal natural transformations for the internal functors in the 1-cell correspondence of Proposition <ref>.

In this subsection we see that internal natural transformations, $\alpha : F \implies G$, between internal functors, $F,G: \mC \to \mX$, that invert $w : W \to \mC_1$ correspond uniquely to natural transformations, $[\alpha] : [F] \implies [G]$, between the uniquely corresponding internal functors $[F] , [G] : \mCW \to \mX$ from Section <ref>. The main result of Section <ref> is the isomorphism of categories established in Theorem <ref>.

We begin with a lemma that shows one direction of the correspondence between the aforementioned natural transformations,

Every internal natural transformation,

\[ \begin{tikzcd}[column sep = huge, row sep = huge, every label/.append style={font=\scriptsize}]
\mC
\arrow[r, bend left=50, "F"{name=f}]
\arrow[r, bend right=50,"G"'{name=g}]
& \mX
\arrow[Rightarrow, shorten <= 10pt, shorten >=10pt, from=f, to=g, "\alpha"]
\end{tikzcd},\]

induces a canonical natural transformation:

\[ \begin{tikzcd}[column sep = huge, row sep = huge, every label/.append style={font=\scriptsize}]
\mCW
\arrow[r, bend left=50, "\lbrack F \rbrack"{name=f}]
\arrow[r, bend right=50,"\lbrack G \rbrack"'{name=g}]
& \mX
\arrow[Rightarrow, shorten <= 10pt, shorten >=10pt, from=f, to=g, "\lbrack \alpha \rbrack"]
\end{tikzcd}\]

Since $\mCW_0 = \mC_0$, define the components of $[\alpha]$ to be the components of $\alpha$:

\[ \begin{tikzcd}[]
\mCW_0 \rar["\lbrack \alpha \rbrack"] & \mX_1 \\
\mC_0 \uar[equals, "L_0"] \ar[ur, "\alpha"']
\end{tikzcd}\]

To see this is well-defined we need to show the (naturality) square

\[ \begin{tikzcd}[column sep = large, row sep = large]
\mCW_1 \rar["(s [\alpha \rbrack {,} [ g \rbrack_1)"]
\dar["( [ f \rbrack_1 {,} t[ \alpha \rbrack)"']
& \mX_2 \dar["c"] \\
\mX_2 \rar["c"'] & \mX_1
\end{tikzcd}\]

commutes in $\cE$. Let $F(w)^{-1}, G(w)^{-1} : W \to \mX_1$ denote the inverses of $w F_1 , w G_1: W \to \mX_1$. Naturality of $\alpha : F \implies G$ implies the diagram

\[ \begin{tikzcd}[column sep = huge, row sep = large]
W \rar["(w s \alpha {,} w G_1)"] \dar["(w F_1 {,} w t \alpha)"'] & \mX_2 \dar["c"] \\
\mX_2 \rar["c"'] & \mX_1
\end{tikzcd} \]

commutes in $\cE$. Using internal composition in $\mX$ to compose with $F(w)^{-1} : W \to \mX_1$ on the left and $G(w)^{-1} : W \to \mX_1$ on the right on both sides gives a new commuting diagram,

\[ \begin{tikzcd}[column sep = huge, row sep = large]
W \rar["(F(W)^{-1} {,}w s \alpha )"] \dar["( w t \alpha {,} g(W)^{-1})"'] & \mX_2 \dar["c"] \\
\mX_2 \rar["c"'] & \mX_1
\end{tikzcd}, \]

by cancellation using the identity law in $\mX$. It will also be helpful to recall the following commuting diagrams from the definition of $\mCW$ and its universal property.

\[
\begin{tikzcd}[column sep = large]
\spn \rar[two heads, "q"] \dar["(\pi_0 F(w)^{-1} {,} \pi_1 F_1 )"'] & \mCW_1 \dar[dotted, "[F \rbrack_1"] \\
\mX_2 \rar["c"'] & \mX_1
\end{tikzcd}\qquad \qquad \]

\[
\begin{tikzcd}[column sep = large]
\spn \rar[two heads, "q"] \dar["\pi_0"'] & \mCW_1 \dar[dotted, "s"] \\
W \rar["wt"'] & \mC_0
\end{tikzcd}\qquad \qquad
\begin{tikzcd}[column sep = large]
\spn \rar[two heads, "q"] \dar["\pi_1"'] & \mCW_1 \dar[dotted, "t"] \\
\mC_1 \rar["t"'] & \mC_0
\end{tikzcd}\]

Now consider the following diagram:

\[ \begin{tikzcd}[column sep = huge, row sep = huge]
\mCW_1
\dar["( [F \rbrack_1 {,} t \lbrack \alpha \rbrack )"']
& \spn
\lar[two heads, "q"'] \rar[two heads, "q"]
\ar[dr, "(q s [\alpha\rbrack {,} q [G \rbrack_1 )"' near end]
\ar[dl, "( q [F \rbrack_1 {,}q t [\alpha\rbrack )" near end]
& \mCW_1 \dar["(s [\alpha\rbrack {,} [G \rbrack_1 )"] \\
\mX_2 \ar[dr, "c"'] & & \mX_2 \ar[dl, "c"] \\
& \mX_1 &
\end{tikzcd}\]

The inside commutes by the following calculation which uses associativity of composition along with naturality of $\alpha$ and the definitions of $[F]_1$, $[G]_1$, and the pullback $\spn = W \tensor[_{ws} ]{\times}{_s} \mC_1$:

\begin{align*}
(q [F]_1 , qt\alpha) c
&=\big( ( \pi_0 F(w)^{-1} , \pi_1 f_1 ) c , q t \alpha \big)c & \text{Def. }[F]_1 \\
&= \big( \pi_0 F(w)^{-1} , \pi_1 f_1 , \pi_1 t \alpha \big)c & \text{Assoc.} \\
&= \big( \pi_0 F(w)^{-1} , \pi_1 (F_1 , t \alpha)c \big)c & \text{Assoc.} \\
&= \big( \pi_0 F(w)^{-1} , \pi_1 (s \alpha , G_1)c \big)c & \text{Nat. }\alpha \\
&= \big( \pi_0 F(w)^{-1} , \pi_1 s \alpha , \pi_1 G_1 \big)c & \text{Assoc.} \\
&= \big( \pi_0 F(w)^{-1} , \pi_0 w s \alpha , \pi_1 G_1 \big)c & \text{Def. }\spn \\
&= \big( \pi_0 (F(w)^{-1} , w s \alpha)c , \pi_1 G_1 \big)c & \text{Assoc.} \\
&= \big( \pi_0 (w t \alpha , G(w)^{-1} )c , \pi_1 G_1 \big)c & \text{Nat. }\alpha \\
&= \big( \pi_0 w t \alpha , \pi_0 G(w)^{-1} , \pi_1 G_1 \big)c & \text{Assoc.} \\
&= \big( q s \alpha , (\pi_0 G(w)^{-1} , \pi_1 G_1) c \big)c & \text{Assoc. }\\
&= \big( q s \alpha , q [G]_1 \big)c & \text{Def. }[g]_1 .
\end{align*}

Since $q$ is an epi we can conclude that$[\alpha]$ satisfies the appropriate naturality condition:

\[( [F \rbrack_1 {,} t \lbrack \alpha \rbrack ) c = ([\alpha\rbrack {,} [G \rbrack_1 ) c .\]

It's source and target can be computed component-wise by the following commuting diagrams

\[ \begin{tikzcd}[column sep = large]
\mCW_0 \dar[equals] \rar["[\alpha\rbrack"] & \mX_1 \dar["s"] \\
\mC_0 \rar["F_0"'] \ar[ur, "\alpha"'] \dar[equals] & \mX_0\\
\mCW_0 \ar[ur, "[F\rbrack_0"'] &
\end{tikzcd} \qquad \qquad \qquad \begin{tikzcd}[column sep = large]
\mCW_0 \dar[equals] \rar["[\alpha\rbrack"] & \mX_1 \dar["t"] \\
\mC_0 \rar["G_0"'] \ar[ur, "\alpha"'] \dar[equals] & \mX_0\\
\mCW_0 \ar[ur, "[G\rbrack_0"'] &
\end{tikzcd}, \]

It follows that $[\alpha] : [F] \implies [G]$ is an internal natural transformation.

We continue with another lemma establishing the other direction of the correspondence between natural transformations.

Every internal natural tranformation,

\[ \begin{tikzcd}[column sep = huge, row sep = huge, every label/.append style={font=\scriptsize}]
\mCW
\arrow[r, bend left=50, "H"{name=f}]
\arrow[r, bend right=50,"K"'{name=g}]
& \mX
\arrow[Rightarrow, shorten <= 10pt, shorten >=10pt, from=f, to=g, " \beta "]
\end{tikzcd},\]

induces a canonical natural transformation:

\[ \begin{tikzcd}[column sep = huge, row sep = huge, every label/.append style={font=\scriptsize}]
\mC
\arrow[r, bend left=50, "LH"{name=f}]
\arrow[r, bend right=50,"LK"'{name=g}]
& \mX
\arrow[Rightarrow, shorten <= 10pt, shorten >=10pt, from=f, to=g, "L\beta"]
\end{tikzcd}\]

The notation is suggestive of the fact that this these are given by composing with the internal functors $H, K : \mCW \to \mX$ and whiskering the internal natural transformation $\beta : H \implies K$ with the internal functor $L : \mC \to \mCW$. Note that the components of the whiskered transformation coincide with those of $\beta$ because $L$ is the identity on objects:

\[ \begin{tikzcd}[]
\mC_0 \rar["L \beta"] & \mX_1 \\
\mCW_0 \uar[equals , "L_0"] \ar[ur, "\beta"']
\end{tikzcd}. \]

Lemmas <ref> and <ref> show us the two directions of the correspondence we need to prove. Now we show the assignments described in the proofs of these lemmas are inverses to get the correspondence we need in the following lemma.

Let $F, G : \mC \to \mX$ be internal functors that invert $w : W \to \mC_1$ in $\mX$. Then the internal natural transformations

\[ \begin{tikzcd}[column sep = huge, row sep = huge, every label/.append style={font=\scriptsize}]
\mC
\arrow[r, bend left=50, "F"{name=f}]
\arrow[r, bend right=50,"G"'{name=g}]
& \mX
\arrow[Rightarrow, shorten <= 10pt, shorten >=10pt, from=f, to=g, "\alpha"]
\end{tikzcd}\]

(bijectively) correspond to the internal natural transformations

\[ \begin{tikzcd}[column sep = huge, row sep = huge, every label/.append style={font=\scriptsize}]
\mCW
\arrow[r, bend left=50, "[F\rbrack"{name=f}]
\arrow[r, bend right=50,"[G\rbrack"'{name=g}]
& \mX
\arrow[Rightarrow, shorten <= 10pt, shorten >=10pt, from=f, to=g, "\lbrack \alpha \rbrack"]
\end{tikzcd}. \]

Let $\alpha : F \implies G$ be an internal natural transformation between internal functors $\mC \to \mX$ that invert $w : W \to \mC_1$ in $\mX$. We will show whiskering the internal natural transformation $[\alpha] : [F] \implies [G]$ with $L : \mC \to \mCW$ recovers $\alpha : F \implies G$:

\[ \begin{tikzcd}[column sep = huge, row sep = huge]
\mC
\arrow[r, bend left=50, "L[F\rbrack"{name=f}]
\arrow[r, bend right=50,"L[G\rbrack"'{name=g}]
& \mX
\arrow[Rightarrow, shorten <= 10pt, shorten >=10pt, from=f, to=g, "L[\alpha\rbrack"]
\end{tikzcd}\quad = \quad
\begin{tikzcd}[column sep = huge, row sep = huge, every label/.append style={font=\scriptsize}]
\mC
\arrow[r, bend left=50, "F"{name=f}]
\arrow[r, bend right=50,"G"'{name=g}]
& \mX
\arrow[Rightarrow, shorten <= 10pt, shorten >=10pt, from=f, to=g, "\alpha"]
\end{tikzcd}\]

By definition of $[F], [G] : \mCW \to \mX$ we have

\[ L [F] = F \qquad \qquad L[G] = G \]

and the following commuting diagram in $\cE$ shows the components of $L[\alpha] : F \implies G$ are precisely those of $\alpha$:

\[ \begin{tikzcd}[column sep = large, row sep = large]
\mC_0 \rar["L [\alpha\rbrack"] & \mX_1\\
\mCW_0 \uar[equals, "L_0"] \rar[equals] \ar[ur, "[\alpha\rbrack"'] & \mC_0 \uar["\alpha"']
\end{tikzcd}\]

On the other hand, for any natural transformation

\[ \begin{tikzcd}[column sep = huge, row sep = huge, every label/.append style={font=\scriptsize}]
\mCW
\arrow[r, bend left=50, "H"{name=f}]
\arrow[r, bend right=50,"K"'{name=g}]
& \mX
\arrow[Rightarrow, shorten <= 10pt, shorten >=10pt, from=f, to=g, " \beta "]
\end{tikzcd}\]

we can see that

\[ \begin{tikzcd}[column sep = huge, row sep = huge, every label/.append style={font=\scriptsize}]
\mCW
\arrow[r, bend left=50, "[Lh\rbrack"{name=f}]
\arrow[r, bend right=50,"[LK\rbrack"'{name=g}]
& \mX
\arrow[Rightarrow, shorten <= 10pt, shorten >=10pt, from=f, to=g, " [L\beta \rbrack"]
\end{tikzcd} \quad = \quad
\begin{tikzcd}[column sep = huge, row sep = huge, every label/.append style={font=\scriptsize}]
\mCW
\arrow[r, bend left=50, "H"{name=f}]
\arrow[r, bend right=50,"K"'{name=g}]
& \mX
\arrow[Rightarrow, shorten <= 10pt, shorten >=10pt, from=f, to=g, " \beta "]
\end{tikzcd}\]

by first noticing that the triangles,

\[ \begin{tikzcd}[column sep = huge, row sep = huge]
\mX & \mC \rar["L [LK\rbrack "] \lar["L [LH\rbrack "'] \dar["L"] & \mX\\
\mC \uar["LH"] \rar["L"']
& \mCW
\ar[ur, dotted, "[LK\rbrack"]
\ar[ul, dotted,"[LH \rbrack"']
& \mC \uar["LK"'] \lar["L"]
\end{tikzcd},\]

commute in $\cE$ and imply that $[LH\rbrack = H $ and $ [LK\rbrack = K$ by the 1-cell universal property of the internal localization in Proposition <ref>. The following commuting diagram shows that the components for the natural transformations agree too:

\[\begin{tikzcd}[column sep = large, row sep = large]
\mCW_0 \rar["[L\beta\rbrack"] & \mX_1 \\
\uar[equals] \mC_0 \rar[equals, "L_0"'] \ar[ur, "L\beta"] & \mCW_0 \uar["\beta"']
\end{tikzcd}\]

The only other piece we need to prove Theorem <ref> is that the correspondence between 2-cells in Lemma <ref> is functorial. It suffices to show functoriality in one direction. We show it in the direction of Lemma <ref> and leave the other direction (involving whiskering) as an exercise to the reader who wants to take a break.

The assignment of natural transformations, $\alpha \mapsto [\alpha]$, in Lemma <ref> is functorial.

For any internal functor $f : \mC \to \mX$, we have

\[ \begin{tikzcd}[column sep = huge, row sep = huge, every label/.append style={font=\scriptsize}]
\mC
\arrow[r, bend left=50, "F"{name=f}]
\arrow[r, bend right=50,"F"'{name=g}]
& \mX
\arrow[Rightarrow, shorten <= 10pt, shorten >=10pt, from=f, to=g, "1_{F}"]
\end{tikzcd}
\begin{tikzcd}[]
\ \rar[mapsto] & \
\end{tikzcd}
\begin{tikzcd}[column sep = huge, row sep = huge, every label/.append style={font=\scriptsize}]
\mCW
\arrow[r, bend left=50, "[F\rbrack"{name=f}]
\arrow[r, bend right=50,"[F\rbrack"'{name=g}]
& \mX
\arrow[Rightarrow, shorten <= 10pt, shorten >=10pt, from=f, to=g, "\lbrack 1_{F} \rbrack"]
\end{tikzcd}\]

where the commuting diagram

\[ \begin{tikzcd}[]
\mCW_0 \rar["\lbrack 1_{F} \rbrack"] & \mX_1 \\
\mC_0 \uar[equals] \ar[ur, bend right, "1_F"'] & \\
\mCW_0 \uar[equals] \ar[uur, bend right, "1_{[F\rbrack}"']
\end{tikzcd}\]

shows that the components of $[1_F]$ coincide with those of $1_{[f]}$. This means $[1_F] = 1_{[F]}$ are the same natural transformation and so identities are preserved.

To see composition is preserved suppose we have two vertically composable internal natural transformations:

\[ \begin{tikzcd}[column sep = huge, row sep = huge, every label/.append style={font=\scriptsize}]
\mC
\arrow[r, shift left, bend left=60, "F"{name=f}]
\arrow[r, "G"near start, ""{name=g}]
\arrow[r, shift right, bend right=60,"H"'{name=h}]
& \mX
\arrow[Rightarrow, shorten <= 5pt, shorten >=1pt, from=f, to=g, "\alpha"]
\arrow[Rightarrow, shorten <= 5pt, shorten >=5pt, from=g, to=h, "\beta"]
\end{tikzcd}
\begin{tikzcd}[]
\ \rar[mapsto] & \
\end{tikzcd}
\begin{tikzcd}[column sep = huge, row sep = huge, every label/.append style={font=\scriptsize}]
\mCW
\arrow[rr, bend left=80, "[F\rbrack"{name=f}]
\arrow[rr, "[G\rbrack"near start, "\ "{name=g}]
\arrow[rr, bend right=80,"[H\rbrack"'{name=h}]
&& \ \ \ \mX \ \ \
\arrow[Rightarrow, shorten <= 5pt, shorten >=1pt, from=f, to=g, "\lbrack \alpha \rbrack"]
\arrow[Rightarrow, shorten <= 5pt, shorten >=5pt, from=g, to=h, "\lbrack \beta \rbrack"]
\end{tikzcd}\]

We can see

\[\begin{tikzcd}[column sep = huge, row sep = huge, every label/.append style={font=\scriptsize}]
\mCW
\arrow[rr, bend left=80, "[F\rbrack"{name=f}]
\arrow[rr, "[G\rbrack"near start, "\ "{name=g}]
\arrow[rr, bend right=80,"[H\rbrack"'{name=h}]
&& \ \ \ \mX \ \ \
\arrow[Rightarrow, shorten <= 5pt, shorten >=1pt, from=f, to=g, "\lbrack \alpha \rbrack"]
\arrow[Rightarrow, shorten <= 5pt, shorten >=5pt, from=g, to=h, "\lbrack \beta \rbrack"]
\end{tikzcd} \qquad = \qquad
\begin{tikzcd}[column sep = huge, row sep = huge, every label/.append style={font=\scriptsize}]
\mCW
\arrow[r, bend left=50, "[F\rbrack"{name=f}]
\arrow[r, bend right=50,"[H\rbrack"'{name=g}]
& \mX
\arrow[Rightarrow, shorten <= 10pt, shorten >=10pt, from=f, to=g, "\lbrack \alpha \beta \rbrack"]
\end{tikzcd}\]

by noticing that their components coincide via the following commuting diagram:

\[ \begin{tikzcd}[]
\mCW_0 \rar["([\alpha \rbrack {,} [ \beta \rbrack)"]
& \mX_2 \rar["c"]
&\mX_1 \\
\mC_0 \uar[equals] \ar[ur, "(\alpha {,} \beta)"']
\ar[urr, bend right, "\alpha \beta"']
&& \\
\mCW_0 \uar[equals, "L_0"] \ar[uurr, bend right, "[\alpha \beta\rbrack"']
\end{tikzcd}\]

The following theorem is a direct consequence of all the lemmas that came before in this section and formalizes the universal property of the internal localization, $\mCW$.

There is an isomorphism of categories

\[ [\mC , \mX]_W^\cE \cong [\mCW , \mX]^{\cE}\]

between internal functors $\mC \to \mX$ in $\cE$ that invert $w : W \to \mC_1$ and their internal natural transformations, and internal functors $\mCW \to \mX$ in $\cE$ and their internal natural transformations.

The objects are in bijection by Proposition <ref>, the arrows are in bijection by Lemma <ref>, and functoriality follows from Lemma <ref>.

§ PSEUDOCOLIMITS OF SMALL FILTERED DIAGRAMS OF INTERNAL CATEGORIES

§.§ Internal Fractions Applied to the internal category of elements

Exercise 6.6, of Exposé VI in [1] states that the pseudocolimit of a filtered diagram $\cA^{op} \to \Cat$ can be obtained by localizing the Grothendieck construction with respect to the cartesian arrows. A current paper in progress, [15], by Bustillo-Vazquez, Pronk, and Szyld shows that with a weaker composition axiom for the category of fractions, the class of arrows one needs to invert to get the pseudocolimit can be reduced from all cartesian arrows to a convenient cleavage of them. For the rest of this chapter we consider an arbitrary but fixed filtered diagram, $D : \cA^{op} \to \Cat(\cE)$ so that every finite diagram in $\cA^{op}$ has a cone. The main theorem of this section states that, in a suitable context $\cE$, the pseudocolimit of a filtered diagram of internal categories, $\cA^{op} \to \Cat(\cE)$, can be computed by forming the internal category of (right) fractions of the internal category of elements with respect to the object representing the canonical cleavage of the cartesian arrows.

Note that the axioms we gave in Section <ref> are for a category of right fractions, so we need to use the contravariant form of the internal category of elements for a functor $D : \cA^{op} \to \Cat(\cE)$. In Section <ref> we introduce the object representing the canonical cleavage and show that it satisfies the Internal Fractions Axioms in Definition <ref>. Section <ref> is all about proving the main result of this thesis. Namely that, when it exists, the internal category of (right) fractions, $\mDW$, of the internal category of elements with respect to the canonical cleavage object, $(\mD , W)$, is the pseudocolimit of the original filtered diagram $D : \cA^{op} \to \Cat(\cE)$.

§.§.§ The Canonical Cleavage of the Internal Category of Elements

The internal category of elements we need for a contravariant functor and a calculus of (right) fractions has an object of arrows defined by

\[ \mD_1 = \coprod_{\varphi \in \cA_1} D_\varphi \qquad \text{ where } \qquad \begin{tikzcd}
D_\varphi \arrow[dr, phantom, "\usebox\pullback" , very near start, color=black]\dar["\pi_0"'] \rar["\pi_1"]
& D(A)_1 \dar["t"] \\
D(B)_0 \rar["D(\varphi)_0"']
& D(A)_0 \end{tikzcd} \]

whenever $\varphi : A \to B$ is an arrow in $\cA$. The subtle difference in this definition is that the vertical map on the right is a target rather than a source and that $D(\varphi) : D(B) \to D(A)$ for $\varphi : A \to B$ in $\cA$. Another subtle but important difference is the definition of cofiber composition for this version of the Grothendieck construction. For $\varphi : A \to B$ and $\psi : B \to C$ in $\cA$, the cofiber composition is given by

\[ \begin{tikzcd}[]
D_{\varphi ; \psi}
\ar[d, "\pi_1"']
\ar[r,"c'_{\varphi ; \psi ; \delta^{-1}}"]
\ar[dr, dotted, "c_{\varphi ; \psi}"]
& D(A)_3 \ar[dr, bend left, "c"] & \\
\ar[dr, bend right, "\pi_0"']
& D_{\varphi \circ \psi} \rar["\pi_1"]
\dar["\pi_0"']
\arrow[dr, phantom, "\usebox\pullback" , very near start, color=black]
& D(A)_1 \dar["t"] \\
& D(C)_0 \rar["D(\varphi \circ \psi)_0"'] & D(A)_0
\end{tikzcd}\]

where $c'_{\varphi ; \psi ; \delta^{-1}}$ is the universal map

\[\begin{tikzcd}[]
D_{\varphi ; \psi}
\ar[ddr, bend right, "c'_{\varphi ; \psi}"']
\ar[drr, bend left, "c'_{(\varphi ; \psi) ; \delta^{-1}}"]
\ar[dr, dotted, "c'_{\varphi ; \psi ; \delta^{-1}}"]
& & \\
& D(A)_3 \rar["\pi_1"] \dar["\pi_0"'] & D(A)_2 \dar["\pi_0"] \\
& D(A)_2 \rar["\pi_1"'] & D(A)_1
\end{tikzcd}.\]

given explicitly by the triple:

\[ \label{contravar cofiber composition arrow} c'_{\varphi ; \psi ; \delta^{-1}} = \big( \pi_0 \pi_1 , \pi_1 \pi_1 D(\varphi)_1 , \pi_1 \pi_0 \delta_{\varphi ; \psi}^{-1} \big) \tag{$\star$} \]

in which $\delta_{\varphi ; \psi}^{-1} : D(C)_0 \to D(A)_1$ represents the inverse components for the structure isomorphism of the pseudofunctor, $D : \cA^{op} \to \Cat(\cE)$.

When $\cE = \Set$, the arrows represented by $\mD_1$ are pairs $(\varphi, f) : ( A,a) \to (B,b)$ where $b \in D(B)_0$ and $f : a \to D(\varphi)(b)$ is in $D(A)_1$. The arrows being picked out by $w : W \to \mD_1$ should correspond to pairs $(\varphi, 1_{D(\varphi)}(b)) : (A,D(\varphi)(b)) \to (B,b)$ where $b \in D(B)_0$ and $1_{D(\varphi)(b)} : D(\varphi)(b) \to D(\varphi)(b)$ is the identity map in $D(A)_1$. The following definition describes an extra condition on $\cE$ that we need in order to work with an object of the canonical cleavage of cartesian arrows in $\mD$.

Suppose $\cE$ admits an internal category of elements of $D : \cA^{op} \to \Cat(\cE)$. Then we say that $\mD$ admits a canonical cleavage of cartesian arrows if for each $\varphi : A \to B$ in $\cA$, the top pullback

\[
\begin{tikzcd}[]
W_\varphi \arrow[dr, phantom, "\usebox\pullback" , very near start, color=black] \dar[tail, "w_\varphi"'] \rar["\pi_\varphi"] & D(A)_0 \dar[tail, "e"] \dar[dd, bend left = 45, equals] \\
D_\varphi \arrow[dr, phantom, "\usebox\pullback" , very near start, color=black]\dar["\pi_0"'] \rar["\pi_1"]
& D(A)_1 \dar["t"] \\
D(B)_0 \rar["D(\varphi)_0"']
& D(A)_0
\end{tikzcd}
\]

exists and the coproduct

\[ W = \coprod_{\varphi \in \cA_1} W_\varphi\]

over all $\varphi \in \cA_1$ exists in $\cE$.

When $\mD$ admits an object of the canonical cleavage of cartesian arrows as in Definition <ref> we can use the universal property of the coproduct, $W$, to get the map $w : W \to \mD_1$ in $\cE$ as follows:

\[\begin{tikzcd}