Test 3

The five-quotient diagram and the $3\times3$ lemma

$$\begin{array}{} \boxed{\begin{array}{} \text{2-cells} \\ \ssigma,\functionf,\ttau \\ \symsX \mathrel{\source\times} \SetXY \mathrel{\target\times} \symtY \\ \end{array}} & \mathop\rightrightarrows\limits^{\symsX \times \text{proj}}_{\symsX \target{\times \text{comp}}} & \boxed{\begin{array}{} \ssigma,\functionf \\ \ssigma,\functionf\ttau \\ \symsX \mathrel{\source\times} \SetXY \\ \end{array}} & {}\rlap{\mkern-7em\target{\xrightarrow[\mkern25em]{\displaystyle \symsX \mathrel{\source\times} \functiont}}} &&& \boxed{\begin{array}{} \ssigma, \target[\functionf\symtY\target] \\ \symsX \mathrel{\source\times} \target( \SetXY\target/\symtY \target) \\ \end{array}} \\ \smash{\lower8ex{\llap{\scriptstyle \text{proj}\times\symtY} \downdownarrows \rlap{\scriptstyle \source{\text{comp}}\times\symtY}}} && \llap{\scriptstyle \text{proj}} \downdownarrows \rlap{\scriptstyle \source{\text{comp}}} && && \smash{\lower8ex{\llap{\scriptstyle \text{proj}} \downdownarrows \rlap{\scriptstyle \source{\text{action}}}}} \\ \boxed{\begin{array}{} \functionf,\ttau\mkern.5em;\mkern.5em\ssigma\functionf,\ttau \\ \SetXY \mathrel{\target\times} \symtY \\ \end{array}} & \mathop\rightrightarrows\limits^{\text{proj}}_{\target{\text{comp}}} & \boxed{\begin{array}{} \scriptstyle \text{proj} \\ \scriptstyle (\symsX \times \text{proj})\text{proj} &&&& \scriptstyle (\symsX \times \target{\text{comp}})\text{proj} \\ \scriptstyle (\text{proj} \times \symtY)\text{proj} &&&& \scriptstyle (\text{proj} \times \symtY)\target{\text{comp}} \\ \functionf & {}\rlap{\mkern-2em \target{\xrightarrow[\mkern17em]{\displaystyle \ttau}}} &&& \functionf\ttau \\ &&&& \llap\ssigma \downarrow \\ \smash{\source{\llap\ssigma \Bigg\downarrow}} && \SetXY && {\displaystyle \ssigma\target(\functionf\ttau\target) \atop \source(\symsX \source\times \target{\text{comp}}\source)\source{\text{comp}}} \\ &&&& \Vert \\ \ssigma\functionf & {}\rlap{\mkern-2em \target{\xrightarrow[\displaystyle \ttau]{\mkern4.5em}}} & \source(\ssigma\functionf\source)\ttau & {}\rlap{\smash{\mkern-2em\xlongequal{\mkern5.5em}}} & \ssigma\functionf\ttau \\ \scriptstyle (\symsX \times \text{proj})\source{\text{comp}} && \scriptstyle (\source{\text{comp}} \times \symtY)\target{\text{comp}} && \scriptstyle \text{comp} \\ \scriptstyle (\source{\text{comp}} \times \symtY)\text{proj} \\ \end{array}} & {}\rlap{\target{\xrightarrow[\mkern15em]{\displaystyle \functiont}}} &&& \boxed{\begin{array}{} \target[\functionf\symtY\target], \ssigma\target[\functionf\symtY\target] = \target[\ssigma\functionf\symtY\target] \\\SetXY\target/\symtY \\ \end{array}} \\ &&&&&& \raise11ex{\smash{\Bigg\downarrow}} \\ \smash{\raise10ex{\smash{ \source{\llap\functions\Bigg\downarrow} \rlap{\mathrel{\target\times} \symtY} }}} && \smash{\raise6ex{\smash{ \source{\llap\functions\Bigg\downarrow} }}} && \searrow \rlap\functionr && \boxed{\begin{array}{} \symsX\target[\functionf\symtY\target] \\ \symsX\source\backslash \target( \SetXY \target{{/}} \symtY \target) \\ \end{array}} \\ &&&&&& \wr\Vert \\ \boxed{\begin{array}{} \source[\symsX\functionf\source], \ttau \\ \source( \symsX\source\backslash\SetXY \source) \mathrel{\target\times} \symtY \\ \end{array}} & \mathop\rightrightarrows\limits^{\text{proj}}_{\target{\text{action}}} & \boxed{\begin{array}{}\source[\symsX\functionf\source] \\ \source[\symsX\functionf\source]\ttau = \source[\symsX\functionf\ttau\source] \\ \symsX\source\backslash\SetXY \\ \end{array}} & {}\rlap{\mkern-7em\xrightarrow[\mkern9em]{}} & \boxed{\begin{array}{} \source[\symsX\functionf\source]\symtY \\ \source( \symsX\source\backslash\SetXY \source) \target{{/}} \symtY \\ \end{array}} & \cong & \boxed{\begin{array}{} \source[\symsX\functionf\symtY\source] \\ \symsX \source\backslash \SetXY \target{{/}} \symtY \\ \end{array}} \\ \end{array}$$

---

$\begin{array}{} \text{$2$-cells} \\ \ssigma,\functionf,\ttau \\ \symsX \mathrel{\source\times} \SetXY \mathrel{\target\times} \symtY \\ \end{array}$	$\mkern2em\mathop\rightrightarrows\limits^{\symsX \times \text{proj}}_{\symsX \target{\times \text{comp}}}$	$\begin{array}{} \source{\text{v-$1$-cells}} \\ \ssigma,\functionf \\ \ssigma,\functionf\ttau \\ \symsX \mathrel{\source\times} \SetXY \\ \end{array}$	$\mkern-6em\target{\xrightarrow[\mkern20em]{\displaystyle \symsX \mathrel{\source\times} \functiont}}$			$\begin{array}{} \ssigma, \target[\functionf\symtY\target] \\ \symsX \mathrel{\source\times} \target( \SetXY\target/\symtY \target) \\ \end{array}$
$\smash{\lower8ex{\llap{\scriptstyle \text{proj}\times\symtY} \downdownarrows \rlap{\scriptstyle \source{\text{comp}}\times\symtY}}}$		$\llap{\scriptstyle \text{proj}} \downdownarrows \rlap{\scriptstyle \source{\text{comp}}}$				$\smash{\lower8ex{\llap{\scriptstyle \text{proj}} \downdownarrows \rlap{\scriptstyle \source{\text{action}}}}}$
$\begin{array}{} \target{\text{h-$1$-cells}} \\ \functionf,\ttau\mkern.5em;\mkern.5em\ssigma\functionf,\ttau \\ \SetXY \mathrel{\target\times} \symtY \\ \end{array}$	$\mkern-2em\mathop\rightrightarrows\limits^{\text{proj}}_{\target{\text{comp}}}$	$\begin{array}{} && \text{$0$-cells} \\ \scriptstyle \text{proj} \\ \scriptstyle (\symsX \times \text{proj})\text{proj} &&&& \scriptstyle (\symsX \times \target{\text{comp}})\text{proj} \\ \scriptstyle (\text{proj} \times \symtY)\text{proj} &&&& \scriptstyle (\text{proj} \times \symtY)\target{\text{comp}} \\ \functionf & {}\rlap{\mkern-2em \target{\xrightarrow[\mkern17em]{\displaystyle \ttau}}} &&& \functionf\ttau \\ &&&& \llap\ssigma \downarrow \\ \smash{\source{\llap\ssigma \Bigg\downarrow}} && \SetXY && {\displaystyle \ssigma\target(\functionf\ttau\target) \atop \source(\symsX \source\times \target{\text{comp}}\source)\source{\text{comp}}} \\ &&&& \Vert \\ \ssigma\functionf & {}\rlap{\mkern-2em \target{\xrightarrow[\displaystyle \ttau]{\mkern4.5em}}} & \source(\ssigma\functionf\source)\ttau & {}\rlap{\smash{\mkern-2em\xlongequal{\mkern5.5em}}} & \ssigma\functionf\ttau \\ \scriptstyle (\symsX \times \text{proj})\source{\text{comp}} && \scriptstyle (\source{\text{comp}} \times \symtY)\target{\text{comp}} && \scriptstyle \text{comp} \\ \scriptstyle (\source{\text{comp}} \times \symtY)\text{proj} \\ \end{array}$	$\mkern.5em\target{\xrightarrow[\mkern11em]{\displaystyle \functiont}}$			$\begin{array}{} \target[\functionf\symtY\target], \ssigma\target[\functionf\symtY\target] = \target[\ssigma\functionf\symtY\target] \\\SetXY\target/\symtY \\ \end{array}$
						$\smash{\raise8ex{\Bigg\downarrow}}$
$\smash{\raise6ex{\source{\llap\functions\Bigg\downarrow} \rlap{\mathrel{\target\times} \symtY}}}$		$\source{\llap\functions\Bigg\downarrow}$			$\searrow \rlap\functionr$	$\begin{array}{} \symsX\target[\functionf\symtY\target] \\ \symsX\source\backslash \target( \SetXY \target{{/}} \symtY \target) \\ \end{array}$
						$\wr\Vert$
$\begin{array}{} \source[\symsX\functionf\source], \ttau \\ \source( \symsX\source\backslash\SetXY \source) \mathrel{\target\times} \symtY \\ \end{array}$	$\mkern2em\mathop\rightrightarrows\limits^{\text{proj}}_{\target{\text{action}}}$	$\begin{array}{}\source[\symsX\functionf\source] \\ \source[\symsX\functionf\source]\ttau = \source[\symsX\functionf\ttau\source] \\ \symsX\source\backslash\SetXY \\ \end{array}$	$\mkern-6.5em\xrightarrow[\mkern7em]{}$	$\begin{array}{} \source[\symsX\functionf\source]\symtY \\ \source( \symsX\source\backslash\SetXY \source) \target{{/}} \symtY \\ \end{array}$	$\cong$	$\begin{array}{} \source[\symsX\functionf\symtY\source] \\ \symsX \source\backslash \SetXY \target{{/}} \symtY \\ \end{array}$