M2Internship/Report/M2Report.tex

% !TeX spellcheck = en_US
\documentclass[10pt,a4paper]{article}

\input{./header.tex}

% po4a: environment remark
% po4a: environment tikzpicture
% po4a: environment property

\title{Categorical semantics of the reduction of GATs to two-sorted GATs.
	\\[1ex] \large Notes on my 4.5-month internship at the Laboratoire d'Informatique de l'École Polytechnique (Palaiseau, France)}
\hypersetup{pdftitle={Categorical semantics of the reduction of GATs to two-sorted GATs}}
\author{Samy Avrillon, supervised by
	\\[1ex] Ambroise Lafont (LIX, Palaiseau, France)}

\begin{document}
	\doparttoc
	\maketitle
	
	\hsep
	
	\tableofcontents
	
	\newpage

	\section{Introduction}
	
	A Generalized Algebraic Theory (or GAT), first introduced by Cartmell \cite{CartmellGATs}, is a syntactic specification of an algebraic structure. From a GAT, one can define a category of models describing the models of the algebraic structure.
	A GAT typically starts with a sort specification i.e. a list of sort declarations, eventually followed by a list of constructors.
	In this document, we will not ask ourselves about the specific syntax of GATs. A \enquote{vague} definition is enough to understand the rest of the document.
	
	\paragraph{Sort specification}
	
	A sort specification is a list of \emph{sort declarations}, composed of \emph{parameters} and $\Set$ as their codomain.
	
	We give an example of a sort specification for Type Theory. On the right column we give the interpretation of the sort declarations as components of the models of the GAT.
	
	\vspace{1em}
	\renewcommand\arraystretch{1.5}
	\begin{tabular}{l|p{.5\textwidth}}
	$\Con : \Set$ & A set of contexts $X_\Con$\\
	$\Ty : (\Gamma : \Con) \to \Set$ & For each context $\Gamma \in X_\Con$, a set $X_\Ty(\Gamma)$ of types in this context\\
	$\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set$ & For each context $\Gamma \in X_\Con$ and each type $A \in X_\Ty(\Gamma)$ in this context, a set $X_\Tm(\Gamma,A)$ of terms of this type.
	\end{tabular}
	\vspace{1em}
	
	A sort specification therefore specifies the differents families of sets contained in a model, and how they relate to each other in terms of indexing.
	
	\paragraph{Constructor specification}
	We can also add constructors to a sort specification. They are composed of parameters (the same kind as sort declarations) and of a codomain which is a sort defined in a previous sort declaration. Those constructors specify elements of the sets contained in the model.
	For example, for the previous sort specification, one can add the following constructors:
	
	\vspace{1em}
	\renewcommand\arraystretch{1.5}
	\begin{tabular}{p{.37\textwidth}|p{.6\textwidth}}
		$\operatorname{unit} : (\Gamma : \Con) \to \Ty\;\Gamma$ & In any context $\Gamma \in X_\Con$, a type $\operatorname{unit}(\Gamma) \in X_\Ty(\Gamma)$.\\
		
		$\operatorname{tt}: (\Gamma : \Con) \to \Tm\;\Gamma\;(\operatorname{unit}(\Gamma))$ & In any context $\Gamma \in X_\Con$, an element $\operatorname{tt}(\Gamma) \in X_\Tm(\Gamma,\operatorname{unit}(\Gamma))$.
	\end{tabular}
	\vspace{1em}
	
	\paragraph{Two-sortification}
	
	It was observed \cite{AmbrusSzumiXie2sort} that one can transform any GAT into a GAT with only two sorts. We will present this transformation.
	
	The sort specification of the transformed GAT is always the same, and contains these two sort declarations:
	
	\vspace{1em}
	\begin{tabular}{p{0.37\textwidth}|p{0.5\textwidth}}
		$\UU : \Set$ & The set of sorts \\
		$\El : \mathcal{O} \to \Set$ & For every sort object $o$ in the set of sorts, a set called $\El(o)$ of objects corresponding to the sort object $o$.
	\end{tabular}
	\vspace{1em}
	
	
	
	Then, we replace all occurrences of $\Set$ to $\mathcal{O}$, and we apply $\El$ to every parameter. We write $\underline{o}$ rather than $\El(o)$ in order to ease reading. For example, the Type Theory GAT presented above becomes that which follows:
	
	\begin{tabular}{p{0.4\textwidth}|p{0.5\textwidth}}
		$\Con : \mathcal{O}$ & One sort object is called \enquote{$\Con$} \\
		$\Ty : (\Gamma : \underline{\Con}) \to \mathcal{O}$ &
		For each object $\Gamma$ corresponding to the sort object $\Con$, another sort object called \enquote{$\Ty\;\Gamma$} \\
		$\Tm : (\Gamma : \underline{\Con}) \to (A : \underline{\Ty\;\Delta}) \to \mathcal{O}$ &
		For each object $\Gamma$ corresponding to the sort object $\Con$,
		and for every object $A$ corresponding to the sort object $\Ty\;\Gamma$, another sort object called \enquote{$\Tm\;\Gamma\;A$}\\
		$\operatorname{unit} : (\Gamma : \underline{\Con}) \to \underline{\Ty\;\Gamma}$ &
		For each object $\Gamma$ corresponding to the sort object $\Con$, an object called "$\operatorname{unit} \Gamma$" corresponding to the sort object $\Ty\;\Gamma$\\
		$\operatorname{tt}: (\Gamma : \underline{\Con}) \to \underline{\Tm\;(\operatorname{unit}\;\Gamma)}$ &
		$\dots$
	\end{tabular}
	
	This process is useful when studying GATs, as it allows to restrict a study to GATs with only two sorts without loss of generality. Filippo Sestini noticed that in his thesis \cite{SestiniPhD}:
	
	\begin{quote}
		Many instances of multi-sorted IITs [IITs are a variant of GATs] can be reduced to equivalent two-sorted IITs, via a systematic reduction method originally observed by Zongpu (Szumi) Xie. We are not aware of a formal proof of this construction for arbitrary IITs, but we conjecture that it does apply to all instances of induction-induction and	consequently that it shows two-sorted IITs are enough to represent any specifiable IIT.
	\end{quote}
	
	\paragraph{Goal}
	
	The goal of my internship was to study and understand the relationship between the categories of models of an original GAT and the category of models of the transformed \enquote{two-sortified} GAT, in order to legitimate this transformation. In this document, we will only study sort specifications (i.e. lists of sort declaration, with no constructors).
	
	We constructed a coreflection between those two categories, whose formal definition is given in next section. It consists of an adjunction $F \vdash G$ between the category $\CC$ of the models of the GAT and the category $\BB$ of the models of the two-sortified GAT, where G is full and faithful.
	
	The category $\BB$ is equipped with a forgetful functor $R$ to $\BB_0$, the category of models of the two-sort sort specification $(\mathcal{O},\El)$.
	
	\begin{center}
		% YADE DIAGRAM GlobalConstructionSimple.json
		% GENERATED LATEX
		\input{graphs/GlobalConstructionSimple.tex}
		% END OF GENERATED LATEX
	\end{center}
	
	\section{Constructing the coreflection}
	
		\paragraph{Structure of the proof}
		
		We will formalize the transformation for \emph{sort specifications} (i.e. lists of sort declarations).
		
		This proof is an induction on the number of sorts taken into account. At each step, we will add a new sort declaration, represented by a functor $H_i$ described later (\autoref{sec:constructingCategory}).
		
		At the $i$-th recursion step, we will build the following objects :
		\begin{itemize}
			\setlength\itemsep{-1ex}
			\item The category of models of the GAT $\CC_i$
			\item The category of models of the transformed GAT $\BB_i$
			\item A forgetful functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$ that creates limits. In our type theory example, $R_1^2$ is a functor from the category of models of $(\mathcal{O},\El,\Con,\Ty,\Tm)$ to the category of models of $(\mathcal{O},\El,\Con,\Ty)$. 
			
			Those functors compose themselves into a functor $R_0^i : \BB_i \to \BB_0$, that also creates limits:
			\[
				R_0^i := R^1_0 \circ \dots \circ R_{i-1}^i
			\]
			\item An operator $\tl^i : \BB_i \times \BB_0 \to \BB_i$ along with a morphism $\inj_\tl^i : X \to X \tl^i Y$ for every $X,Y$ in $\BB_i \times \BB_0$, such that the canonical morphism $\en_{i-1}^i : (R_{i-1}^i X) \tl^{i-1} Y \to R_{i-1}^i (X \tl^i Y)$ is an isomorphism. This operation follows a specific universal property: For every morphisms $g : X \to Z$ and $h : Y \to R_0^iZ$, there is an unique morphism $\{g;h\}$ such that the two following diagrams commute:
			\label{sec:tlUniversalProperty}
			
			\begin{center}
				% YADE DIAGRAM TlUniversal.json
				% GENERATED LATEX
				\input{graphs/TlUniversal.tex}
				% END OF GENERATED LATEX
			\end{center}
				
			where $\en_0^i$ is the following composition:
			
			\[\en_0^i := R_0^{i-1} \en_{i-1}^i \circ  \dots \circ R_0^1\en_1^2 \circ \en_0^1 :  (R_0^i X) \oplus Y = (R_0^i X) \tl^0 Y \to R_0^i (X \tl^i Y)\]
			
			And where $\inj_2$ is the second injector of $\oplus$, the coproduct of the category $\BB_0 = \TSet$. We will define $\tl^0$ to be $\oplus$, so the equality above holds.
			
			The operator is also defined on morphisms, such that for any morphism $g : X \to X'$ in $\BB_i$ and $h : Y \to Y'$ in $\BB_0$, there is a morphism $g \tl^i h : X \tl^i Y \to X' \tl^i Y'$ in $\BB_i$.
			 
			\item A functor $F_i : \BB_i \to \CC_i$
			\item A functor $G_i : \CC_i \to \BB_i$
			\item An adjunction between them $F_i \vdash G_i$
			\item A proof that $F_iG_i \cong \Id_{\CC_i}$ (i.e. $F_i \vdash G_i$ make up a coreflection)
			\item A proof that $F_i\inj_\tl^i$ is an isomorphism. The inverse isomorphism will be denoted as $(F_i\inj_\tl^i)^{-1}$
		\end{itemize}
		
		Here is a figure that describes the recursive construction of some of the above objects
		\begin{center}
			% YADE DIAGRAM GlobalRecursiveConstruction.json
			% GENERATED LATEX
			\input{graphs/GlobalRecursiveConstruction.tex}
			% END OF GENERATED LATEX
		\end{center}
	
		\subsection{Preliminaries}
		
			\paragraph{Grothendieck Construction} 
		For a category $\mathcal{C}$ and a functor $F : \mathcal{C} \to \Cat$, the Grothendieck construction of $F$ is a category whose objects are pairs of
		\begin{itemize}
			\item $X$ an object of $\mathcal{C}$
			\item an object of $F(X)$
		\end{itemize}
		
		The morphism $(X,Y) \to (X',Y')$ is therefore a pair of a morphism $f : X \to X'$ in $\mathcal{C}$ and a morphism $g : F(f)(Y) \to Y'$ in $H(X')$.
		
		We will denote this category $(X : \mathcal{C}) \times F(X)$ as its objects are pairs.
		
		\paragraph{Slice category}
		For a category $\mathcal{C}$ and $X$ an object in that category, the slice category (or over category) $\mathcal{C}/X$ is a category whose objects are pairs of
		\begin{itemize}
			\item $Y$ an object of $\mathcal{C}$
			\item an arrow $Y \to X$ of $\mathcal{C}$
		\end{itemize}
		
		A morphism $(Y,f) \to (Y',f')$ is a morphism $g : Y \to Y'$ such that $f' \circ g = f$.
		
		We can define a functor $\left(\mathcal{C}/\dash\right) : \mathcal{C} \to \Cat$ from this construction.
		
		We will often concatenate the two method above to create from a category $\mathcal{C}$ and a functor $H : \mathcal{C} \to \Set$ a new category $(X : \mathcal{C}) \times \left(\Set\middle/H(X)\right)$.
		
		\paragraph{Slice category over a set}
		
		When the category $\mathcal{C}$ is $\Set$, we have the equivalence 
		\[\Set/X \simeq \Set^X\]
		
		This equivalence is described by the following correspondence of objects.
		An object $(Y,f)$ of $\Set/X$ is transformed into the family of sets $A : X \to \Set$ defined by
		\[
			A(x) := f^{-1}(\{x\}) = \text{the coimage by f of the singleton $\{x\}$}
		\]
		
		Conversly, a familiy of sets $A : X \to \Set$ is transformed into the following object of $\Set/X$
		\begin{center}
			% YADE DIAGRAM EquivSetXSetX.json
			% GENERATED LATEX
			\input{graphs/EquivSetXSetX.tex}
			% END OF GENERATED LATEX
		\end{center}
		
		where $\coprod$ is the coproduct of $\Set$ and $\pi_1$ is the first projection of the coproduct.
		
		Morphisms are translated using the same logic.
		
		\paragraph{Category of models of the two-sort sort specification}
		\label{sec:categoryOfModelsOfTwoSorts}
		The usual way of defining the category of models of the two-sort specification $\BB_0$ is by taking the category of families of sets $\FamSet$, defined as $(X:\Set) \times \Set^X$. However, we will rather use another category : $\TSet$, the category of presheaves over the category $\TT$, the category with two object and one non-trivial arrow between them. The objects and morphism of $\TT$ are described below:
			
		\begin{center}
			% YADE DIAGRAM CategoryTT.json
			% GENERATED LATEX
			\input{graphs/CategoryTT.tex}
			% END OF GENERATED LATEX
		\end{center}
		
		This category is equivalent to the catgegory $\FamSet$, as $(X : \Set) \times \Set^X$ is equivalent to $(X : \Set) \times (\Set/X)$ (as seen above), which is isomorphic to $\TSet$ (both categories consists of two sets and one arrow between them).
		
		With this formalisation, a model of the two-sort GAT is a functor $X : \TSet$, such that
		\begin{itemize}
			\item $X_\UU$ is the set of the \enquote{sort objects}
			\item For each sort object $\Gamma \in X_\UU$, the set of objects corresponding to the sort object is $X_p^{-1}(\{\Gamma\}) \subset X_\El$
		\end{itemize}
		
		Therefore the categories of models of the transformed GATs will be built atop of this category $\BB_0 = \TSet$.
		
		\paragraph{$K$ functor}
		
		We define a helper functor $K_A : (X:C) \times (\Set/A(X)) \to \TSet$ defined as follows
		\[
		K_A(X,(Y,f)) = \TSetObject{Y}{f}{A(X)}
		\]
		The morphisms are translated as-is.
		
		\begin{remark}
			This functor can be constructed using the formal construction of the Grothendieck construction of $\TSet \cong (X: \Set) \times (\Set/X)$ as a pullback in the category of categories $\Cat$
		\end{remark}
	
	\subsection{Initialization}
		In this subsection, we will build the objects of the first step of our induction. This will correspond to the empty sort specification, i.e. the induction step $i = 0$.
		
		\begin{itemize}
			\setlength\itemsep{-1ex}
			\item $\CC_0$ is $\one$, the category with only one object $\star$ and one trivial morphism (i.e. the terminal category of $\Cat$), because the empty sort specification only has one model.
			\item $\BB_0$ is $\TSet$, the category of models of the $(\mathcal{O},\El)$ sort specification (see dedicated paragraph in last subsection for a description).
			\item The universal property of $\tl^0$ is that of the coproduct. Therefore, we will define $\tl^0 : \BB_0 \times \BB_0 \to \BB_0$ to be the coproduct $\oplus$ of $\TSet$, with $\inj_\tl^0 : X \to X \oplus Y$ being the first injector of the coproduct. The second injector of the coproduct $\oplus$ will be refered as $\inj_2$.
			\item $F_0 : \TSet \to \one$ is the terminal functor of $\Cat$
			\item $G_0 : \one \to \TSet$ is the functor that sends the only object of $\one$ to the initial object of $\TSet$: $0_\TSet$
			\item For $X$ an object of $\TSet$, we have 
			\[\Hom(G_0 \star,X) = \Hom(0_\TSet,X) \cong \one \cong \Hom(\star,F_0 X)\]
			(reminder: $\star$ is the only object of $\one$)
			Therefore, we have that $F_0 \vdash G_0$.
			\item $F_0G_0 : \one \to \one$ so $F_0G_0 = \Id_\one$ as $\one$ is terminal in $\Cat$
			\item $F_i\inj_1 = \id_\star$ which is an isomorphism
		\end{itemize}
		
		
	\subsection{Inductive Step: Constructing the categories}
	
		\label{sec:constructingCategory}
		In this part, i will show how we construct recursively both categories $\CC_i$ and $\BB_i$, along with the functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$. We will use the loop invariants that we expressed in the introduction of this section.
		
		In order to construct the categories, we need some object describing the specific sort we are adding to the categories. This object is a specific functor $H_i : \CC_{i-1} \to \Set$. Those functors are the same that Altenkirsh and al. \cite{Altenkirch2018} used in their paper to describe a specification of sorts.
		We suppose that those $H_i$ functors are given.
		
		\begin{remark}
			There is a way of getting the functor $H_i$ from the syntax, which is described in \autoref{sec:HiFromSyntax}.
		\end{remark}
		
		\subsubsection{Constructing $\CC_i$}
		
		We construct the category $\CC_i$ as the following Grothendieck pair:
		\[
			\CC_i := (X : \CC_{i-1}) \times \left(\Set\middle/H_i(X)\right)
		\]
		and where $H_i$ is the specific functor described above.
		
		This way of constructing the category has formerly been described by Altenkirsch and al. \cite{Altenkirch2018}, with the only difference of the equivalence $\Set/H_i(X) \simeq \Set^{H_i(X)}$.
		
		\paragraph{An example of $H_i$ functors}
		Let us now give an example of those $H_i$ objects for our type theory example.
		
		\[
			\boxed{\Con : \Set}
		\]
		We begin with the following functor, corresponding to the sort declaration above
		\[
			H_1(\star) = 1 \in \Set
		\]
		
		This corresponds to the fact that $\Con$ takes no parameter.
		
		Therefore $\CC_1 = 1 \times \Set^1 \simeq \Set$, which is as expected: a model $X$ consists of a set $X_\Con$.
		
		\[
			\boxed{\Ty : (\Gamma : \Con) \to \Set}
		\]
		
		Then, we take the functor $H_2(X) = X_\Con$, corresponding to the sort declaration above. This functor means that types need \emph{one} context to be built.
		
		Therefore $\CC_2 = (X:\Set) \times (\Set/X) \simeq (X:\Set) \times (\Set^X) = \FamSet$, a model $X$ is a family of sets $\left(X_\Ty(\Gamma)\right)_{\Gamma \in X_\Con}$, as expected.
		\[
			\boxed{\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set}
		\]
		
		Finally, we take the functor $H_3(X) = \sum_{\Gamma : X_\Con}X_\Ty(\Gamma)$. It means that terms need \emph{one} context, and \emph{one} type of that context.
		
		An object of that final category $\CC_3$ is a triple
		\[
			(X_\Con: \Set, X_\Ty : X_\Con \to \Set, X_\Tm : (\Delta: X_\Con) \to X_\Ty(\Delta) \to \Set)
		\]
		\subsubsection{Constructing $\BB_i$}
		
		We construct the category $\BB_i$ as follows.
		
		An object of $\BB_i$ is a pair of:
		\begin{itemize}
			\item an object $X$ of $\BB_{i-1}$
			\item a \enquote{sort constructor} $\Cstr^X$ as a function $H_iF_{i-1}X \to (R_0^{i-1}X)_\UU$
			\newline
			where $H_i$ is the functor $\CC_{i-1} \to \Set$ described above and $F_{i-1}$ is the right part of the adjunction $\BB_{i-1} \to \CC_{i-1}$ that we have defined at the previous induction step.
		\end{itemize}
		
		If we have an object $X$ of $\BB_i$, the first component is denoted as $R_{i-1}^iX$, which is an object of $\BB_{i-1}$, and the second component is denoted as $\Cstr^X : R_{i-1}^i X \to (R_0^iX)_\UU$. 
		
		A morphism $X \to X'$ of $\BB_i$ is a morphism $f : R_{i-1}^iX \to R_{i-1}^iX'$ in $\BB_{i-1}$ such that the following diagram commutes.
		
		\begin{center}
			% YADE DIAGRAM BiMorphismDiagram.json
			% GENERATED LATEX
			\input{graphs/BiMorphismDiagram.tex}
			% END OF GENERATED LATEX
		\end{center}
		
		For a morphism $f : X \to X'$ of $\BB_i$, we denote as $R_{i-1}^if$ the underlying morphism $R_{i-1}^i X \to R_{i-1}^i X'$.
		
		Identities and compositions are that of the category $\BB_{i-1}$, and categorical equalities are trivially derived from the diagram above.
		
		$R_{i-1}^i$ acts on objects and morphisms, and induces a functor $\BB_i \to \BB_{i-1}$. The induced functor is monadic, and therefore preserves limits.
		
	\subsection{Inductive step: Constructing the functors $F_i$ and $G_i$}
	
		The adjunction $F_i \vdash G_i$ is built using the two functors from the adjunction $F_{i-1} \vdash G_{i-1}$ defined in the previous induction step. We use them to define the first part of the adjunction, and we compose them with two adjoint functors $W$ and $E$ that we will define in this section. The overall construction for this induction step is as follows:
		
		\begin{center}
			% YADE DIAGRAM InductionStepDiagram.json
			% GENERATED LATEX
			\input{graphs/InductionStepDiagram.tex}
			% END OF GENERATED LATEX
		\end{center}
		
		Where
		\[
			(F_{i-1} \times \id)(X,\underset{y : Y \to F_{i-1}(X)}{(Y,y)}) = (F_{i-1}X,\underset{y : Y \to F_{i-1}X}{(Y,y)})
		\]
		\[
			(F_{i-1} \times \id)(f,g) = (F_{i-1}f,g)
		\]
		and
		\[
			(G_{i-1} \times (H_i\eta_{i-1} \circ \dash))(X,\underset{y : Y \to H_iX}{(Y,y)}) = (G_{i-1}X,\underset{Y : Y \to H_i X \to H_iF_{i-1}(G_{i-1}X)}{(Y,H_i\eta_{i-1} \circ y)})
		\]
		\[
			(G_{i-1} \times (H_i\eta_{i-1} \circ \dash))(f,g) = (G_{i-1}f,g)
		\]
		with $\eta_{i-1} : X \to F_{i-1}G_{i-1}X$ being the unit of the adjunction $F_{i-1} \vdash G_{i-1}$.
		
		These equations define two functors, that create the following adjunction:
		\[F_{i-1} \times \id \vdash G_{i-1} \times (H_i\eta_{i-1} \circ \dash)\]
		
		The unit of this adjunction is $\eta_{i-1} \times (H_i\eta_{i-1}\circ \dash)$ and its counit is $\varepsilon_{i-1} \times \id$, where $\varepsilon_{i-1}$ is the counit of the adjunction $F_{i-1} \vdash G_{i-1}$
		
	\subsubsection{W definition}
	
		We define a functor $W : \left(\left(X : \BB_{i-1}\right) \times \Set/H_iF_{i-1}X\right) \to \BB_{i}$
		
		The action on objects is as follows:
		\[
		W(X,Y) := \left(X \tl^{i-1} K_{H_iF_{i-1}}(X,Y), \widetilde{\inj_2} \right)
		\]
		
		With $\widetilde{\inj_2}$ being defined by the composition
		\begin{center}
			% YADE DIAGRAM Wdef.json
			% GENERATED LATEX
			\input{graphs/Wdef.tex}
			% END OF GENERATED LATEX
		\end{center}
		
		The action on a morphism $(g,h)$ from $(X,Y)$ to $(X',Y')$ is the following:
		\[
			W(g,h) := \left(g \tl^{i-1} K_{H_iF_{i-1}}(g,h)\right)
		\]
		
		It is indeed a morphism of $\BB_{i}$ as it makes the following diagram commute.
		
		\begin{center}
			% YADE DIAGRAM WghMorphismOfBi.json
			% GENERATED LATEX
			\input{graphs/WghMorphismOfBi.tex}
			% END OF GENERATED LATEX
		\end{center}
	
	\subsubsection{E definition}
	
		We define $E : \BB_{i} \to \left(X : \BB_{i-1}\right) \times (\Set/H_iF_{i-1}X)$
		
		The action on objects is 
		\[
			E(X) = (R_{i-1}^i X, (A,h))
		\]
		Where $(A,h)$ is defined as the following pullback:
		
		\begin{center}
			% YADE DIAGRAM EDefinitionPullback.json
			% GENERATED LATEX
			\input{graphs/EDefinitionPullback.tex}
			% END OF GENERATED LATEX
		\end{center}
		
		The action on a morphism $f$ from $X$ to $X'$ is defined as $E(f) = (R_{i-1}^i f, !)$, with $!$ being the only morphism making the following diagram commute (thanks to the pullback property):
		
		\begin{center}
			% YADE DIAGRAM EDefinitionMorphism.json
			% GENERATED LATEX
			\input{graphs/EDefinitionMorphism.tex}
			% END OF GENERATED LATEX
		\end{center}
		 
	\subsection{Inductive Step: Proof of the adjunction}
		 
		 In this subsection, we prove that $(W,E)$ make an adjunction by showing that there is a natural isomorphism between $\Hom$ sets in both categories.
		 
		 We want to construct for each $(X,Y)$ in $(X : \BB_{i-1}) \times (\Set/H_iF_{i-1}X)$ and $Z$ in $\BB_i$, a natural isomorphism $\phi_{XYZ}$.
		 
		 \[
			 \phi_{XYZ} : \Hom(W(X,Y),Z) \to \Hom((X,Y),E(Z))
		 \]
		 
		 I will present how the isomorphisms and its inverse are constructed. The proof that $\phi_{XYZ}$ and $\phi_{XYZ}^{-1}$ are inverse one of the other, and that they are natural are given in  \autoref{apx:phi-WE-isnat}.
		 
	\subsubsection{Constructing $\phi_{XYZ}$}
		
		Let $f$ be in $\Hom(W(X,Y),Z)$.
		We want to construct $\phi_{XYZ}(f) : (X,Y) \to E(Z)$.
		
		The first component of $\phi_{XYZ}(f)$ is defined as the following composition:
		
		\begin{center}
			% YADE DIAGRAM PhiXYZFirstComponent.json
			% GENERATED LATEX
			\input{graphs/PhiXYZFirstComponent.tex}
			% END OF GENERATED LATEX
		\end{center}
		
		The second component is defined through the universal property of the pullback defined by $E(Z)$ according to the following diagram:
		
		\begin{center}
			% YADE DIAGRAM PhiXYZSndComponentPullback.json
			% GENERATED LATEX
			\input{graphs/PhiXYZSndComponentPullback.tex}
			% END OF GENERATED LATEX
		
\end{center}
		
	\subsubsection{Constructing $\phi^{-1}_{XYZ}$}
		
		Now, we take $(g,h)$ a morphism from $(X,Y)$ to $E(Z)$.
		
		The morphism $\phi^{-1}_{XYZ}(g,h)$ of $\BB_i$ from $W(X,Y)$ to $Z$ is a morphism of $\BB_{i-1}$ from $X \tl^{i-1} K_{H_iF_{i-1}} (X,Y)$ to $R_{i-1}^i(Z)$ that make a specific diagram commute. We build this morphism using the universal property of $\tl^{i-1}$, stated in \autoref{sec:tlUniversalProperty}
		
		\[
			\phi^{-1}_{XYZ}(g,h) := \left\{g ; \square \right\}
		\]
		
		\todo{Est-ce qu'il faut que j'écrive $R_{i-1}^i\phi^{-1}_{XYZ}(g,h) := ...$ pour être plus «homogène» ?}
		
		Where $\square$ is a morphism $K_{H_iF_{i-1}} (X,Y) \to R_0^i Z$ in $\TSet$ defined by the following diagram:
		
		\begin{center}
			% YADE DIAGRAM PhiXYZ-1Square.json
			% GENERATED LATEX
			\input{graphs/PhiXYZ-1Square.tex}
			% END OF GENERATED LATEX
		
\end{center}
		
		Finally, we check that $\phi^{-1}_{XYZ}(g,h)$ is a morphism of $\BB_i$ from $W(X,Y)$ to $Z$, i.e. that it makes the following diagram commute:
		
		\begin{center}
			% YADE DIAGRAM PhiXYZ-1MorphismOfBi.json
			% GENERATED LATEX
			\input{graphs/PhiXYZ-1MorphismOfBi.tex}
			% END OF GENERATED LATEX
		
\end{center}
	
		In order to complete this proof, we need to show that
		\begin{itemize}
			\item $\phi_{XYZ}^{-1} \circ \phi_{XYZ} (f) = f$
			\item $\phi_{XYZ} \circ \phi_{XYZ}^{-1} (g,h) = (g,h)$
			\item $\phi_{XYZ}$ is natural.
		\end{itemize}
		
		The proofs of these statements are given in \autoref{apx:phi-WE-isnat}.
		
		
		
	\subsubsection{Coreflection}
	
		We have proven that this newly created adjunction $F_i \vdash G_i$ create a coreflection. It means that $F_iG_i \cong \Id_{\CC_i}$, or equivalently that $G_i$ is full and faithful.
		
		The proof is that statement is given in \autoref{apx:FG-refl}.
			
	\subsection{Inductive step: Constructing $\tl^i$}
	
		\label{sec:coproductConstr}
		
		\paragraph{Constructing the objects}
		We will define the $\tl^i$ operator of two objects $X$ from $\BB_i$ and $Y$ from $\BB_0$ as follows:
		\[
			X \tl_i Y := \left((R_{i-1}^i X) \tl^{i-1} Y, (R_0^{i-1} \inj_\tl^{i-1})_\UU \circ \Cstr_i^X \circ (H_iF_{i-1}\inj_\tl^{i-1})^{-1}\right)
		\]
			
		The constructor goes as follows:
		
		\begin{center}
			% YADE DIAGRAM TlConstructor.json
			% GENERATED LATEX
			\input{graphs/TlConstructor.tex}
			% END OF GENERATED LATEX
		\end{center}
		
		The injector $\inj_\tl^i : X \to X \tl^i Y$ is defined as follows:
		\[
			\inj_\tl^i := \inj_\tl^{i-1} : R_{i-1}^i X \to R_{i-1}^i (X \tl^i Y) = R_{i-1}^i X \tl^{i-1} Y
		\]
		
		It is a morphism of $\BB_i$ as it makes the following diagram commute:
		
		\begin{center}
			% YADE DIAGRAM TlInj1MorphismOfBi.json
			% GENERATED LATEX
			\input{graphs/TlInj1MorphismOfBi.tex}
			% END OF GENERATED LATEX
		\end{center}
		
		\paragraph{Universal Property}
		We will now show that that the universal property stated in \autoref{sec:tlUniversalProperty} holds.
		To that end, we take two objects $X$ and $Z$ in $\BB_i$, $Y$ in $\BB_0$, a morphism $g : X \to Z$ in $\BB_i$ and a morphism $h : Y \to R_0^iZ$ in $\BB_0$. We want to build a morphism $\{g,h\}$ of $\BB_i$ such that the following two diagrams commute.
		
		\begin{center}
			% YADE DIAGRAM TlUniversal.json
			% GENERATED LATEX
			\input{graphs/TlUniversal.tex}
			% END OF GENERATED LATEX
		\end{center}
		
		We define $\{g ; h\}_i = \{R_{i-1}^i g ; h\}_{i-1}$. This is a morphism of $\BB_i$ as it makes the following diagram commute:
		
		\begin{center}
			% YADE DIAGRAM TlUniversalMorphismIsOfBi.json
			% GENERATED LATEX
			\input{graphs/TlUniversalMorphismIsOfBi.tex}
			% END OF GENERATED LATEX
		\end{center}
		
		With this definition, the isomorphism $\en_{i-1}^i : (R_{i-1}^i X) \tl^{i-1} Y \to R_{i-1}^i(X \tl^i Y)$ is simply the identity morphism.
		
		\paragraph{Building morphisms}
		
		For any two morphisms $g : X \to X'$ of $\BB_i$ and $h : Y \to Y'$ of $\BB_0$, we will create a morphism $X \tl^i Y \to X' \tl^i Y'$ as follows:
		\[
			g\tl^ih := R_{i-1}^ig \tl^{i-1} h
		\]
		\todo{Même question d'homogénéité}
		
		This is indeed a morphism of $\BB_i$ as it makes the following diagram commute:
		
		\begin{center}
			% YADE DIAGRAM TlDefOnMorphisms.json
			% GENERATED LATEX
			\input{graphs/TlDefOnMorphisms.tex}
			% END OF GENERATED LATEX
		\end{center}
		
		\paragraph{Composition with $F_i$}
		We finally need to prove, for any objects $X$ in $\BB_i$ and $Y$ in $\TSet$, that the morphism
		$F_i(\inj_\tl^i) : F_iX \to F_i(X \tl^i Y)$ is an isomorphism.
		
		Morphisms $\BB_{i}$ are morphisms of $\BB_{i-1}$ that follows some equations, and composition is the same. Moreover, we know from the definition above that $R_{i-1^i} \inj_\tl^i := \inj_\tl^{i-1}$.
		
		So, we just need to know that $R_{i-1}^i(F_{i-1}\inj_\tl^i)$ is an isomorphism.
		
		\[
			R_{i-1}^iF_i\inj_\tl^i = \left[(F_{i-1} \times \id) (E(\inj_\tl^i))\right]_1 = \left[(F_{i-1} \times \id) (R_{i-1}^i \inj_\tl^i,!)\right]_1 = F_{i-1} \inj_\tl^{-1}
		\]

		And we know from the previous induction step that $F_{i-1}\inj_\tl^{i-1}$ is an isomorphism. Therefore, $F_i\inj_\tl^i$ is an isomorphism.
	
	\section{Other Properties}
	
	\subsection{Fibration of the category $\CC_i$}
	
	In the formal proof, we defined $\CC_i$ as an inductive Grothendieck construction as in Altenkirsch and al. papers \cite{Altenkirch2018}.
	
	But there is an other way \cite{Fiore2008} of building the category $\CC_i$ which is equivalent to the one presented above.
	
	With this other method, a sort specification is described by a countable simple direct category $S$ (i.e. a countable category where all the arrows follow an unique direction, and $\Hom$-sets are finite). The models of the sort specification are therefore the presheaves over the category $S$ called $\left[S,\Set\right]$.
	
	\paragraph{Constructing $S$ as a sequence}
	In order to fall back on the definition we gave in the formal proof, we will build the final countable simple direct category $S$ as a sequence $\emptyset = S_0,S_1,\dots,S_i$ where $S_i$ is the category describing the sort specification limited to the $i$ first sort declarations.
	
	The input data describing the GAT will be a sequence of finite functors $\Gamma_i : S_{i-1} \to \Set$.
	
	We will then construct the category $S_i$ by adding a single object $\alpha_i$ to the category $S_{i-1}$, along with morphisms $f : \alpha_j \to \alpha_{i+1}$ for $f \in \Gamma_{i+1}(\alpha_j)$ and $j \leq i$. The morphisms follow the composition condition, describing that every pair of morphisms $f : \alpha_j \to \alpha_{i+1}$ and $g : \alpha_k \to \alpha_{i+1}$ (i.e. $f\in\Gamma_{i+1}(\alpha_k)$ and $g\in\Gamma_{i+1}(\alpha_j)$) and for every morphism of $S_{i}$ $h : \alpha_j \to \alpha_k$, we have $\Gamma_{i+1}(h)(f) \circ f = g$.
	
	Avec le formalisme de la construction de Grothendieck, on peut formaliser la construction de la nouvelle catégorie comme cela:
	\[
		S_i = S_{i-1} \times 
	\]
	
	The final category is simply $S = \bigcup S_i$.
	
	In our type theory example, the category $S$ is constructed as follows:
	
	\begin{center}
	\begin{tabular}{c|c|c}
		$\boxed{\Con : \Set}$ &
		$\boxed{\Ty : (\Gamma : \Con) \to \Set}$ &
		$\boxed{\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set}$ \\
		$S_1 = \qquad \Con$	&
		$S_2 = \qquad \Con \leftarrow \Ty$ &
		$S_3 = \qquad \Con \leftarrow \Ty \leftarrow \Tm$ \\
		$\left[S_1,\Set\right] \simeq \CC_1$ &
		$\left[S_2,\Set\right] \simeq \CC_2$ &
		$\left[S_3,\Set\right] \simeq \CC_3$
	\end{tabular}
	\end{center}
	
	\begin{remark}
		This definition is reversable (up to the order of the sorts), and therefore, one can define a sequence of $\Gamma_i$ functors from any countable simple direct category.
	\end{remark}
	
	\paragraph{Falling back on the formal proof}
	
		In the formal proof, we used categories $\CC_i$ and functors $H_i : \CC_i \to \Set$. We now undertand that the categories $\CC_i$ are defined on top of the categories $S_i$ with $\CC_i := \left[S_i,\Set\right]$.
		
		In the same way, the functors $H_i : \CC_{i-1} \to \Set$ are defined on top of the functors $\Gamma_i$ with the following relation:
		\[
			H_i(X) := \Hom_{\left[S_{i-1},\Set\right]}\left(\Gamma_i,X\right)
		\]
	
	\subsection{Creating semantics object from the syntax}
		\label{sec:HiFromSyntax}
		
		In this part, we will see how the functors $\Gamma_i$ given above can be constructed from the syntax of a sort specification. The previous subsection gives us a way of constructing the $H_i$ functors from the $\Gamma_i$ functors, and thus one can make the complete proof with the definition below.
		
		\paragraph{Verbose sort specification}
		We will take a verbose version of a sort specification, where when \enquote{implementing} a sort, we gave the name of the parameter and the name of the term. For example, our type theory example becomes the following verbose version:
		
		\begin{center}
		\renewcommand\arraystretch{1.5}
		\begin{tabular}{l}
			$\Con : \Set$\\
			$\Ty : (\Gamma : \Con) \to \Set$ \\
			$\Tm : (\Delta : \Con) \to (A : \Ty \left[\Gamma \mapsto \Delta\right]) \to \Set$
		\end{tabular}
		\end{center}
		\vspace{1em}
		The only sort declaration that changes is that of $\Tm$ as it is the only one for which one of its parameter is a sort with parameters.
		
		With that verbose definition, a generic sort specification is a list of sort declarations indexed by $\mathbb{T}$, the fully ordered set of all sorts. The sort declarations are as follow, for a sort $T \in \mathbb{T}$
		
		\[
			T : \left[x_a^T : U_T(a) \left[x^{U_T(a)}_{b} \mapsto x^T_{v_T(a,b)}\right]_{b\leq I_{U_T(a)}}\right]_{a \leq I_T} \to \Set
		\]
		
		Where
		\begin{itemize}
			\setlength\itemsep{-.2em}
			\item $I_T$ is the number of parameters of the sort $T$
			\item $x^T_a$ is the $a$-th parameter of the sort $T$
			\item $U_T(a)$ is the sort of the $a$-th parameter of the sort $T$ (we have $U_T(a) < T$)
			\item $I_{U_T(a)}$ is the number of parameters of the sort $U_T(a)$ i.e. the number of arguments we have to give to make an object of sort $U_T(a)$
			\item $x^{U_T(a)}_b$ is the $b$-th parameter of the sort $U_T(a)$
			\item $v_T(a,b)$ is the index of the parameter of the sort $T$ given as the $b$-th parameter of the $a$-th parameter of the sort $T$ (we have $v_T(a,b) < a$)
			\item The types of parameters have to be respected, therefore we must have the equality
			\[
				U_T(v_T(a,b)) = U_{U_T(a)}(b)
			\]
		\end{itemize}
		
		For example, for the above sort declaration, we would have
		\begin{itemize}
			\setlength\itemsep{-.2em}
			\item $\mathbb{T} = \left\{\Con < \Ty < \Tm\right\}$
			\item $I_\Con = 0$, $I_\Ty = 1$, $I_\Tm = 2$
			\item $x^\Ty_1 = "\Gamma"$, $x^\Tm_1 = "\Delta"$, $x^\Tm_2 = "A"$
			\item $U_\Ty(1) = \Con$, $U_\Tm(1) = \Con$, $U_\Tm(2) = \Ty$
			\item $v_\Tm(2,1) = 1$ such that $x^\Tm_{v_\Tm(2,1)} = "\Delta"$ (associated to $x^\Ty_{b=1} = "\Gamma"$)
		\end{itemize}
		
		\paragraph{Describing the category $S$}
			
			We will then describe what is the category $S$ corresponding to a given sort specification $(\mathbb{T},I,U,v)$
			
			Its objects are simply the sorts, i.e. the elements of $\mathbb{T}$.
			
			Morphisms from a sort $T_x$ to a different sort $T_y$ are described by $U$ and correspond to the parameters of the sort $T_x$ that are of sort $T_y$. In other words:
			
			\[
				\Hom_{S}(T_x,T_y) = \left\{x^{T_x}_a\middle| a \leq I_{T_x} \text{ and } U_{T_x}(a) = T_y\right\}
			\]
			
			We can see that the category is direct, because of the rule $U_T(a) < T$ i.e. if $T_x < T_y$ then $\Hom_S(T_x,T_y) = \emptyset$.
			For every sort $T$, we define $\Hom_S(T,T)$ to contain only the identity morphism $\id_T$, for which composition rules are already defined.
			
			Composition is described by $v$, corresponding to\enquote{parameters of parameters}.
			Let's take two morphisms $x^{T_x}_b : T_x \to T_y$ and $x^{T_y}_a : T_y \to T_z$. Their composition is defined by
			\[
				x^{T_y}_a \circ x^{T_x}_b = x^{T_x}_{v_{T_x}(a,b)}
			\]
			
			This composition is well-defined as 
			\[
				U_{T_x}(v_{T_x}(a,b)) = U_{U_{T_x}(a)}(b) = U_{T_y}(b) = T_z
			\]
			
			For our type theory example, the category $S$ is as follows
			
			\begin{center}
				% YADE DIAGRAM TyThExampleSCat.json
				% GENERATED LATEX
				\input{graphs/TyThExampleSCat.tex}
				% END OF GENERATED LATEX
			\end{center}
		
		\paragraph{Creating the functor $\Gamma_i$}
		
			We know we can create the functors $\Gamma_i$ directly from a complete category $S$, but we will look more in detail what those functors mean related to the syntax.
			
			If we are given the category $S_{i-1}$ with objects corresponding to the $i-1$ sorts already defined.
			
			We want to build a finite functor $\Gamma_i : S_{i-1} \to \Set$ corresponding to the following sort declaration of a new sort $T_i$
		
			We will build $\Gamma_i$ as follows:
			
			\[
				\Gamma_i(T_x) = \left\{x^{T_i}_a\middle| a \leq I_{T_i} \text{ and } U_{T_i}(a) = T_x\right\}
			\]
			
			\[
				\Gamma_i(x_b^{T_x} : T_x \to T_y)(x^{T_i}_a \in \Gamma_i(T_x)) = x^{T_i}_{v_{T_i}(a,b)}
			\]
			
			This definition is redundant with that of the last paragraph, but it has the advantage of directly creating the functor $\Gamma_i$ that are used to create the functors $H_i$ and all the rest of the proof.
	
	\subsection{Non-recursive definitions}
	
	\subsubsection{Redefinition of $\BB_i$}
	\subsubsection{Redefinition of $G_i$ and $F_i$}
	\subsubsection{Non-direct base category}
	
	\subsection{Infinite construction of $\BB_i$}
	\[
	\BB_i := \left(X : \TSet, \Cstr : (a : S_{i-1}) \to \Hom_{\BB_{a-1}}(G_{a-1}\Gamma_a,R_{a-1}^i(\this)) \to X(\UU)\right)
	\]
	A morphism from $(X,\Cstr)$ to $(X', \Cstr')$ is a morphism from $X$ to $X'$ in $\TSet$ (i.e. a natural transformation $X \implies X'$) which makes the following diagram commute, for all $a$ in $S_{i-1}$.
	
	\begin{center}
		% YADE DIAGRAM BiMorphismDiagram.json
		% GENERATED LATEX
		\input{graphs/BiMorphismDiagram.tex}
		% END OF GENERATED LATEX
	\end{center}
	
	Identities and compositions are that of the base category $\TSet$, and categorical equalities are trivially derived from the diagram above.
	
	The diagram expresses as
	\[
	\forall \gamma \in \Hom_{G_{a-1}\Gamma_a,X}, \quad \Cstr'_a(f \circ \gamma) = f_\UU(\Cstr_a \gamma)
	\]
	
	\todo{Define properly the use of \this}
	
	\subsection{$G$ and $F$ infinite constructions}
	
	\[
	G_i(Y) = \left(\sum_{a\in S_i}H_{Y(a)}\left(\lim_{(a/S_i)*}\overline{Y_a}\right), \lambda a.\lambda \eta.(a,u (\inj_2 \star))\right)
	\]
	
	where $u : \left(Y(a) \oplus 1, \inj_1\right) \to (\lim_{(a/S_i)*} \overline{Y_a})$
	
	so that $\varphi_{b,f} u (\star) = \eta_\El^b(f)$
	
	\[
	F_i(X,\Cstr)(a) = X(p)^{-1}\left(\Cstr_a\left(\Hom_{\BB_{a-1}}(G_{a-1}\Gamma_a,X)\right)\right)
	\]
	\[
	F_i(X,\Cstr)(f : a \to b)(X(p)(x); x \in \Cstr_a(\eta)) = \eta_\El^b(f)
	\]
	
	\todo{Show that those are the same functors as those defined recursively. Prove the adjunction/reflection infinitely ?}
	
	\section{Summary}
		
		\lipsum[2-3]
	
	
	
	\section{Bibliography}
	\begingroup
	\renewcommand{\section}[2]{}%
	\printbibliography
	\endgroup
	
	\newpage
	\addappheadtotoc
	\appendix
	\addtocontents{toc}{\protect\setcounter{tocdepth}{-1}}
	\appendixpage
	
	\section{$W \dashv E$ adjunction}
	\label{apx:phi-WE-isnat}
	
	
	\subsection{Composition $\phi_{XYZ} \circ \phi_{XYZ}^{-1}$}
	
	The first component of $\phi_{XYZ} (\phi_{XYZ}^{-1}(g,h))$ is
	\[
	R_{i-1}^i(\phi_{XYZ}^{-1}(g,h)) \circ \inj_\tl^{i-1} = \left\{g ; \square \right\} \circ \inj_\tl^{i-1} = g
	\]
	
	The second component of $\phi_{XYZ} (\phi_{XYZ}^{-1}(g,h))$ follows the following diagram
	
	\begin{center}
		% YADE DIAGRAM CompositionSecondComponent.json
		% GENERATED LATEX
		\input{graphs/CompositionSecondComponent.tex}
		% END OF GENERATED LATEX
	
\end{center}
	
	
	\todo{Justifier que la partie du haut commute, i.e. que \[
		(R_0^{i-1}\{g,\square\})_\El \circ (\en_0^i)_\El \circ (\inj_2)_\El = \square_\El
		\]}
		
	The diagram commutes, and so we can deduce that the second component of $\phi_{XYZ}(f)$ is $h$, by proprty of the pullback $E(Z)$
	
	\subsection{Composition $\phi_{XYZ}^{-1} \circ \phi_{XYZ}$}
	
	Now, the converse composition is
	
	\[
	\phi_{XYZ}^{-1} (\phi_{XYZ}(f)) = \left\{R_{i-1}^i f \circ \inj_\tl^{i-1} ; \square \right\}
	\]
	where $\square$ follows the following diagram
	
	\begin{center}
		% YADE DIAGRAM CompositionSquareConstruction.json
		% GENERATED LATEX
		\input{graphs/CompositionSquareConstruction.tex}
		% END OF GENERATED LATEX
	\end{center}
	
	We want to show that $\phi_{XYZ}^{-1} (\phi_{XYZ}(f)) = f$. By definition of $\{;\}$ in $\BB_i$, it suffices to show that $\square = R_0^i f \circ \en_0^{i-1} \circ \inj_2$.
	
	The two required equalities are proved by the diagram above:
	
	\begin{align*}
		\square_\El = \left(R_0^i f \circ \en_0^{i-1} \circ \inj_2\right)_\El \\
		\square_\UU = \left(R_0^i f \circ \en_0^{i-1} \circ \inj_2\right)_\UU
	\end{align*}
	
	\subsection{Naturality}
	
	We want to show that the following diagram commutes, for any objects $X$,$Y$,$Z$,$X'$,$Y'$,$Z'$ and morphisms $f$,$g$,$h$.
	
	\begin{center}
		% YADE DIAGRAM NaturalityDiagram.json
		% GENERATED LATEX
		\input{graphs/NaturalityDiagram.tex}
		% END OF GENERATED LATEX
	\end{center}
	
	We take a morphism $\ii$ in $\Hom\left(W(X,Y),Z\right)$. We want to show that it is sent by the above diagram to the same morphism of $\Hom\left((X',Y'),E(Z')\right)$.
	
	We first look at the first component of the result morphism.
	
	\[\begin{array}{rcl}
		\phi_{X'Y'Z'}(f \circ \ii \circ W(g,h))_1
		&=& R_{i-1}^i\left(f \circ \ii \circ (g \tl^{i-1} K_\bullet(g,h))^+\right) \circ \inj_\tl^{i-1} \\
		&=& R_{i-1}^i f \circ R_{i-1}^i \ii \circ (g \tl^{i-1} K_\bullet(g,h)) \circ \inj_\tl^{i-1} \\
		&=& R_{i-1}^i f \circ R_{i-1}^i \ii \circ \inj_\tl^{i-1} \circ g \\
		&=& \left[E(f) \circ \phi_{XYZ}(\ii) \circ (g,h)\right]_1
	\end{array}\]
	
	The second components are defined as described by the following diagram
	
	\begin{center}
		% YADE DIAGRAM NaturalityDoublePullbackDefinition.json
		% GENERATED LATEX
		\input{graphs/NaturalityDoublePullbackDefinition.tex}
		% END OF GENERATED LATEX
	\end{center}
	
	The second projection of $\phi_{XYZ}(f \circ \ii \circ W(g,h))$ is defined by the pullback of $E(Z')$ commuting with the two path highlighted by the inner blue line. And that of $\phi_{X'Y'Z'}(\ii)$ is defined by the red outer line.
	The outer squares commute, and therefore, by the pullback property, we get that
	\[
		\phi_{X'Y'Z'}(f\circ\ii\circ W(g,h))_2 = \left[E(f) \circ \phi_{XYZ}(\ii) \circ (g,h)\right]_2
 	\]
	
	And thus we have naturality.
	
	
	\section{$F_i \vdash G_i$ reflection}
	\label{apx:FG-refl}
	
	We want to find, for each object $(X,(B,g))$ of $\CC_i = (X : \CC_{i-1}) \times (\Set/H_i(X))$, an isomorphism $(X,(B,g)) \to F_iG_i(X,(B,g))$. $g$ is a morphism from $B$ to $H_i(X)$
	
	\[\begin{array}{rcl}
		F_iG_i(X,(B,g)) 
		&=& F_iW_i(G_{i-1}X,(B,H_i\eta_{i-1}\circ g))\\
		&=& F_i\left(G_{i-1}X \tl^{i-1}K_\bullet(G_{i-1}X,(B,H_i\eta_{i-1}\circ g)),\widetilde{\inj_2}\right)\\
		&=&(F_{i-1} \times \id)\left(G_{i-1}X \tl^{i-1}K_\bullet(G_{i-1}X,(B,H_i\eta_{i-1}\circ g)),(A,h)\right)\\
		&=&\left(F_{i-1}(G_{i-1}X \tl^{i-1}K_\bullet(G_{i-1}X,(B,H_i\eta_{i-1}\circ g))),(A,h)\right)
	\end{array}\]
	
	Where $(A,h)$ is the pullback defined as
	\begin{center}
		% YADE DIAGRAM ReflectionFGPullback.json
		% GENERATED LATEX
		\input{graphs/ReflectionFGPullback.tex}
		% END OF GENERATED LATEX
	\end{center}
	
	We can extend this pullback with the two isomorphisms $\en_0^i$ and $H_iF_{i-1}(\inj_\tl^{i-1})$ in another pullback. This new pullback is over the injection morphism $\inj_2$ of the coproduct of $\TSet$, so the new pullback object is the second component of the $\bullet \oplus B$ i.e. $B$.
	
	\begin{center}
		% YADE DIAGRAM ReflectionFGExtendedPullback.json
		% GENERATED LATEX
		\input{graphs/ReflectionFGExtendedPullback.tex}
		% END OF GENERATED LATEX
	\end{center}
	
	The first component of the isomorphism is the following isomorphism, where $\eta_{i-1}^{FG}$ if the counit of the adjunction $F_{i-1} \vdash G_{i-1}$, that we know to be an isomorphism from the induction hypothesis.
	
	\begin{center}
		% YADE DIAGRAM ReflectionFGIsomorphismFirst.json
		% GENERATED LATEX
		\input{graphs/ReflectionFGIsomorphismFirst.tex}
		% END OF GENERATED LATEX
	\end{center}
	
	And the second component is made using the isomorphism constructed by the pullback, that makes the diagram commute.
	\begin{center}
		% YADE DIAGRAM ReflectionFGIsomorphismSecond.json
		% GENERATED LATEX
		\input{graphs/ReflectionFGIsomorphismSecond.tex}
		% END OF GENERATED LATEX
	\end{center}
	
	
\end{document}