M2Internship/Report/M2Report.tex

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

\input{./header.tex}

\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}
		
		\lipsum[7-9]
		
	\section{Content}
	
	Plan
	
	\begin{enumerate}
		\item Présentation de ce qu'est un GAT, simple exemple
		\item Présentation de la 2-sortification d'un GAT
		\item Présentation de la catégorification de Fiore
		\item Présentation de la catégorification de Altenkirsch -> Construction des $\BB_i$ récursive
		\item Schéma de construction récursif de l'adjonction
		\item Formulation de H1 et H3
		\item (ANNEXE?) Def de W et de E
		\item (ANNEXE?) Preuve de l'adjonction / de la reflexion
		\item (ANNEXE?) Preuve des propriétés
		\item Définition infinie de $\BB_i$	-> Foncteur $R_0^iG_i$ -> Reflexions sur les catégories pas directes
	\end{enumerate}
	
	
	\section{Sort specification}
	
	A Generalized Algebraic Theory (or GAT) and inductive-inductive types are syntaxes describing models.
	Both are composed of a sort specification, and eventually a list of constructors.
	In this document, we will not ask ourselves about the specificities of both syntaxes. A \enquote{vague} interpretation of them is enough to understand the constructions that follows.
	
	A sort specification is a list of \emph{sort constructors} that are defined with \emph{parameters} with $\Set$ as its codomain.
	
	Here is an example of a classical sort specification for Type Theory.
	
	\[  	\Con : \Set \\
	\]\[	\Ty : (\Gamma : \Con) \to \Set \\
	\]\[	\Tm : (\Gamma : \Delta) \to (A : \Ty \Delta) \to \Set
	\]
	This specification is to be read as follows:
	
	\begin{center}
		There is one sort that is $\Con$
		
		For every element $\Gamma$ of the sort $\Con$, there is a sort $\Ty \Gamma$
		
		For every element $\Gamma$ of the sort $\Con$, and every element $A$ of the sort $\Ty \Gamma$, there is a sort $\Tm \Gamma\;F$
	\end{center}
	
	We can also add constructors to a sort specification.
	For example, for the previous sort specification, one can add the following constructors:
	
	\[
		\operatorname{unit} : (\Gamma : \Con) \to \Ty \Gamma
	\]
	\[
		\verb*|_| = \verb*|_|: (\Gamma : \Con) \to (A : \Ty \Gamma) \to \Tm \Gamma A \to \Tm \Gamma A \to \Ty \Gamma
	\]
	
	Constructors construct terms and not sorts. A sort specification with or without constructor describes a class of models, which are in the intuitive sense of a model (a model implements \enquote{sort constructors}, regular constructors).
	
	A known process is that one can transform a specification of sorts, into a specification of sorts with two sorts and constructors.
	
	The two sorts are always the same:
	
	\[
		\mathcal{O} : \square
	\]
	\[
		\underline{\;\bullet\;} : \mathcal{O} \to \square
	\]
	
	Where $\mathcal{O}$ describes the \enquote{sort of sorts}, and $\underline{\;\bullet\;}$ give for every \enquote{sort object} the sort of the \enquote{objects of that sort}.
	
	Then, we replace all occurrences of $\Set$ to $\mathcal{O}$, and we apply underline to every sort constructor parameter. For example, the first Type Theory of sort specification becomes that which follows:
	
	\[  	\Con : \mathcal{O} \\
	\]\[	\Ty : (\Gamma : \underline{\Con}) \to \mathcal{O} \\
	\]\[	\Tm : (\Gamma : \underline{\Con}) \to (A : \underline{\Ty \Delta}) \to \mathcal{O}
	\]
	
	It is known that this new sorts and constructors specification is equivalent to the former one.
	
	Fiore \cite{Fiore2008} describes \emph{sort specifications} as countable simple direct categories. To every object, we associate a sort, which is built using parameters pointing out of them. We often write this category $S$, and for a sort $a$ in it, the parameters needed to construct the sort are indexed by $(a/S)*$.
	
	As an example, here is the category version of the above specification of sorts. We also add the equality $\Gamma \circ A = \Delta$. This equality describes that the $\Gamma$-parameter i.e. the first parameter of the $\Ty$ sort constructor is the variable $\Delta$. Without this equality, $\Gamma \circ A$ would be another arrow going from $\Tm$, and therefore another parameter on type $\Con$.
	
	
	\begin{center}
		% YADE DIAGRAM B1.json
		% GENERATED LATEX
		\input{graphs/B1.tex}
		% END OF GENERATED LATEX
	\end{center}
	
	The category of models over a specification of sorts is then the category of presheaves over the category of Fiore $\left[S,\Set\right]$.
	
	Altenkirsch \cite{Altenkirch2018} has another method to directly construct the category of models of a specification of sorts. His method is more general, but it does not give a \enquote{Tiny and simple} category as Fiore does.
	The other advantage of Altenkirsch's method is that they give a way of also describing the models of a constructor specification.
	
	What we will do is to try to make an adjunction between Fiore's category of models $\left[S,\Set\right]$, and Altenkirsch's category of models of the two-sorted GAT.
	
	We will describe how the two categories are constructed in detail.
	
	\subsection{Constructing the categories}
	
	We will construct both categories $S$ and $\BB$ recursively, addings new sorts one by one.
	
	\subsubsection{Fiore's category}
	
	At the same time, we construct the simple category recursively $\emptyset = S_0,S_1,S_2,...$.
	
	In order to construct the $i$-th sort, we use a finite functor $\Gamma_i : \left[S_{i-1} \to \Set\right]$ describing entirely the sort constructor.
	This functor is to be understood as $\Gamma_i(a)$ is the set of parameters of type $a$ for our new sort. In the above example, we would have $\Gamma_\Ty(\Con) = \{"\Gamma"\} = 1$ and $\Gamma_\Tm(\Con) = \{\Delta\}$,$\Gamma_\Tm(\Ty) = \{"A"\}$,$\Gamma_\Tm(\Gamma) = \left["A" \mapsto "\Delta"\right]$.
	
	Then, to construct $S_i$, we add one object $i$ to $S_{i-1}$, along with morphisms $x : i \to a$ for every $x \in \Gamma_i(a)$ for every $a$ in $S_{i-1}$. We also add equalities 
	$s \circ x = x'$ for every $s : b \to a$ and $x \in \Gamma_i(a)$ and $x' \in \Gamma_i(b)$ where $\Gamma_i(s)(x') = x$.
	
	\begin{remark}
		We have that $\Hom_{S_i}(a,b) = \Gamma_b(a)$ or $(a/S_i)* \equiv \Gamma_a$.TODO C'est sûr la deuxième partie ?
	\end{remark}
	
	\subsubsection{Altenkirsch's category}
	
	To start our series of category, we need the category of models of the two-sort specification of sorts ($\mathcal{O}$ and $\underline{\;\bullet\;}$). We do it Fiore's way and we get a simple category that we name $\TT$ with two elements and only one non-trivial arrow between them.
	
	\begin{center}
		% YADE DIAGRAM G0.json
		% GENERATED LATEX
		\input{graphs/G0.tex}
		% END OF GENERATED LATEX
	\end{center}
	
	The category of models $\TSet$ is also written $\BB_0$ as it is the first step of Altenkirsch's method of adding constructors.
	
	\begin{remark}
		Following Altenkirsch's construction of category of models for a sort specification, we end up on the category of families of sets $(X : \Set, Y : X \to \Set)$.
		This category is equivalent to $\TSet$ which allows us to give a clearer definition of functors. 
	\end{remark}
	
	Then, we recursively add constructors, constructing categories $\BB_1$,$\BB_2$, etc.
	
	For the $i$-th constructor, we define the category $\BB_i$ as :
	
	\[
	\BB_i := \left(X : \BB_{i-1}, \Cstr_i : \Hom_{\BB_{i-1}} (G_{i-1}\Gamma_i,X) \to (R_0^{i-1}X)_\UU \right)
	\]
	
	where $\Gamma_i$ is the functor $S_{i-1} \to \Set$ that describe the sort constructor being processed, and $G_{i-1}$ is the left part of the adjunction $\left[S_{i-1}, \Set\right] \to \BB_{i-1}$ that we are defining recursively at the same time.
	
	A morphism $(X,\Cstr_i) \to (X',\Cstr'_i)$ in $\BB_i$ is a morphism $f : X \to X'$ in $\BB_{i-1}$ such that the following diagram commutes.
	
	\begin{center}
		% YADE DIAGRAM D1.json
		% GENERATED LATEX
		\input{graphs/D1.tex}
		% END OF GENERATED LATEX
	\end{center}
	
	Identities and compositions are that of the category $\BB_{i-1}$, and categorical equalities are trivially derived from the diagram above.

	We also define a functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$ that sends objects and morphisms to their first component. This functor is a \emph{right adjunct} of another functor we call $L_{i-1}^i$.
	
	As we can compose the adjunctions $R_0^1$,$R_1^2$,...,$R_{i-1}^i$, we will create the two following syntactic sugars for the composed adjunctions.
	\[
	R_i^j = R_{i}^{i+1} \circ R_{i+1}^j = R_{i}^{j-1} \circ R_{j-1}^{j} = R_{i}^{i+1} \circ ... \circ R_{j-1}^{j}
	\]
	\[
	L_i^j = L_{j-1}^{j} \circ L_{i}^{j-1} = L_{i+1}^{j} \circ L_{i}^{i+1} = L_{j-1}^{j} \circ ... \circ L_{i}^{i+1}
	\]
	
	We will also denote $\eta_i^j : \mathbf{1} \to R_i^j L_i^j$ and $\varepsilon_i^j : L_i^j R_i^j \to \mathbf{1}$ to be the unit and counit of the adjunction $R_i^j \vdash L_i^j$.
	
	
	
	We know that this category has a coproduct, that we will denote $\oplus_i$ or just $\oplus$ when there is no ambiguity. We will also denote as $\inj_1^i : X \to X \oplus Y$ (resp. $\inj_2^i : Y \to X \oplus Y$) the first (resp. second) injector of the coproduct of $\BB_i$. For every morphisms $f : X \to Z$ and $g : Y \to Z$, we will denote with $\{f;g\}$ the unique morphism from $X \oplus Y$ to $Z$ such that $\{f;g\} \circ \inj^i_1 = f$ and $\{f;g\} \circ \inj^i_2 = g$.

	\begin{remark}
		This adjunction and the existence of a coproduct comes from seeing $\BB_i$ being a category of algebras in $\BB_{i-1}$ over the arrow $inj_1 : G_{i-1}\Gamma_i \to G_{i-1}\Gamma_i \oplus L_0^{i-1} y\UU$.
	\end{remark}
	
	\subsubsection{Summary}
	
	Here is a graph summarizing the categories and functors.
	We have constructed two chains of categories $\BB_0$,$\BB_1$,... and $S_0$,$S_1$,...
	
	The categories $\BB_{i-1}$ and $\BB_{i}$ are in an adjunction written $R_{i-1}^i \vdash L_{i-1}^i$.
	
	We will give in the next part the construction of the adjunction $F_i \vdash G_i$ at the step $i$. The functor $G_{i-1}$ is used in the definition of $\BB_i$, so the two recurrences have to be done at the same time.
	
	
	
	\begin{center}
		% YADE DIAGRAM G1.json
		% GENERATED LATEX
		\input{graphs/G1.tex}
		% END OF GENERATED LATEX
	\end{center}
	
	
	\subsection{Constructing the adjunction}
	
	\subsubsection{Hypotheses}
	
		In order to build and prove the adjunction, we will state hypotheses that we will progressively prove during our building of $\BB_i$, $F_i$, and $G_i$.
		
		\begin{property}[H1]
			\[
			\simpleArrow{R_{i-1}^i X \oplus L_0^{i-1} Y}{\left\{R_{i-1}^i \inj_1^i ; R_{i-1}^i \inj_2^i \circ \eta_{i-1}^i\right\}}{R_{i-1}^i(X \oplus_i L_0^i Y)}
			\]
			is an equivalence.
		\end{property}
		
		\begin{property}[H1r]
			\[
			\simpleArrow{ R_{0}^i X \oplus_{i-1} Y}{\left\{R_{i-1}^i \inj_1^i ; \eta_{i-1}^i\right\}}{R_{i-1}^i(X \oplus_i L_0^i Y)}
			\]
			is an equivalence.
			
			This property is proven easily by recursion over previous property H1.
		\end{property}
		
		\begin{property}[H3]
			\[
			\simpleArrow{F_i X}{F(\inj_1^i)}{F_i(X \oplus L_0^i Y)}
			\]
			is an equivalence.
		\end{property}
		
		\begin{property}[H3']
			\[
			\simpleArrow{\Hom(G_i\Gamma, X)}{(inj_1^i \circ \dash)}{\Hom(G_i\Gamma,X \oplus L_0^i Y)}
			\]
			is an equivalence.
			
			This proven with the adjunction property of $F_i \vdash G_i$ and H3, as w have that
			\[
				\Hom(G_i \Gamma, X) \cong \Hom(\Gamma, F_i X) \cong \Hom(\Gamma, F_i(X \oplus L_0^i Y)) \cong \Hom(G_i \Gamma, X \oplus L_0^i Y)
			\]
		\end{property}
		
	\subsubsection{Decomposing the proof}
	
		In order to use all the power of the recurrence, we will build the $F_i \vdash G_i$ adjunction using the $F_{i-1} \vdash G_{i-1}$ adjunction, following the diagram below.
		
		\begin{center}
			% YADE DIAGRAM G2.json
			% GENERATED LATEX
			\input{graphs/G2.tex}
			% END OF GENERATED LATEX
		\end{center}
		
		The category $\left[S_i, \Set\right]$ is seen as the category $\left[S_{i-1},\Set\right]$ to which we have added an object along with morphisms described by $\Gamma_i$. The morphisms we added to the object $X$ have the shape of the slice category of the set $\Hom(\Gamma_i,X)$.
		
		The first part $G_{i-1} \times \id \dashv F_{i-1} \times \id$ is proven and defined as an adjunction from the last step of the recurrence. 
		
		We will now define the two functors.
		
		
	\subsubsection{W definition}
	
		We define a functor $W : \displaystyle\sum_{X : \BB_{i-1}} (\Set/\Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,X)) \to \BB_{i}$
		
		\[
		W(X,Y) := \left(X \oplus L_0^{i-1} \Hbar_{\Hom(G_{i-1}\Gamma_i,\dash)}(X,Y), \widetilde{\inj_2} \right)
		\]
		
		With $\widetilde{\inj_2}$ being defined by
		\[
		\begin{array}{lcl}
			\Hom(G_{i-1}\Gamma_i,X \oplus L_0^{i-1} \Hbar_\bullet(X,Y)) & \to^{\text{H3'}} & \Hom(G_{i-1}\Gamma_i,X)\\
			& = & \Hbar_\bullet(X,Y)_\UU \\
			& \to^{\inj_2^0} &  \left(R_0^{i-1}X \oplus \Hbar_\bullet(X,Y)\right)_\UU \\
			& \to^{\text{H1r}} & \left(R_0^{i-1}(X \oplus L_0^{i-1}\Hbar_\bullet(X,Y))\right)_\UU
		\end{array}
		\]
		
		The action on a morphism $(g,h)$ from $(X,Y)$ to $(X',Y')$ is the following:
		\[
		W(g,h) := \left(g \oplus L_0^{i-1} \Hbar_{\Hom(G_{i-1}\Gamma_i,\dash)}(g,h)\right)
		\]
		
		It is indeed a morphism from $\BB_{i}$ as it makes the following diagram commute.
		
		\begin{center}
			% YADE DIAGRAM D2.json
			% GENERATED LATEX
			\input{graphs/D2.tex}
			% END OF GENERATED LATEX
		\end{center}
	
	\subsubsection{E definition}
	
		We define $E : \BB_{i} \to \displaystyle\sum_{X : \BB_{i-1}} (\Set/\Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,X))$
		
		\[
		E(X) = (R_{i-1}^i X, (A,h))
		\]
		Where $(A,h)$ is defined as the following pullback:
		
		\begin{center}
			% YADE DIAGRAM D3a.json
			% GENERATED LATEX
			\input{graphs/D3a.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 D3b.json
			% GENERATED LATEX
			\input{graphs/D3b.tex}
			% END OF GENERATED LATEX
		\end{center}
		 
		 
	\subsubsection{Proof of the adjunction}
		 
		 We prove that $(W,E)$ make an adjunction showing that there is a natural isomorphism between $\Hom$ sets in both categories.
		 
		 We want to construct for each $(X,Y)$ in $\displaystyle\prod_{X : \BB_{i-1}} (\Set/\Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,X))$ and $Z$ in $\BB_i$, an isomorphism $\phi_{XYZ}$.
		 
		 \[
			 \phi_{XYZ} : \Hom(W(X,Y),Z) \to \Hom((X,Y),E(Z))
		 \]
		 
		 I will give the construction of the isomorphisms and its inverse, the proofs are given in \autoref{apx:phi-WE-isnat}.
		 
	\paragraph{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 $R_{i-1}^i f \circ inj_1^{i-1} : X \to R_{i-1}^i Z$, with $R_{i-1}^i f$ being a morphism of $\BB_{i-1}$ from $R_{i-1}^i(W(X,Y)) = X \oplus_{i-1} L_0^{i-1}$ to $R_{i-1}^i Z$.
		
		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 D6.json
			% GENERATED LATEX
			\input{graphs/D6.tex}
			% END OF GENERATED LATEX
		\end{center}
		
	\paragraph{Constructing $\phi^{-1}_{XYZ}$}
		
		Now, we take $(g,h)$ a morphism from $(X,Y)$ to $E(Z)$.
		
		We define $\phi^{-1}_{XYZ}(g,h)$ as a morphism of $\BB_i$ from $W(X,Y)$ to $Z$, i.e. a morphism of $\BB_{i-1}$ from $X \oplus_{i-1} L_0^{i-1} \Hbar (X,Y)$ to $R_0^{i-1}(Z)$ that makes a certain diagram commute:
		\[
			\phi^{-1}_{XYZ}(g,h) := \left\{g ; \varepsilon_0^i \circ L_0^{i-1} \square \right\}
		\]
		
		Where $\square$ is a morphism $\Hbar (X,Y) \to R_0^i Z$ defined by the following diagram:
		
		\begin{center}
			% YADE DIAGRAM D7.json
			% GENERATED LATEX
			\input{graphs/D7.tex}
			% END OF GENERATED LATEX
		\end{center}
		
		This is indeed a morphism of $\BB_i$ from $W(X,Y)$ to $Z$ as it makes the following diagram commute
		
		\begin{center}
			% YADE DIAGRAM D8.json
			% GENERATED LATEX
			\input{graphs/D8.tex}
			% END OF GENERATED LATEX
		\end{center}
		
		We show in \autoref{apx:phi-WE-isnat} that $\phi_{XYZ}$ and $\phi_{XYZ}^{-1}$ do indeed make a natural isomorphism.
		
		
		
	\subsection{$F \vdash G$ make a reflexion}
		
	\subsection{Proof of H1 - Sum definition}
	
		We will define the sums of the form $X \oplus_i L_0^i Y$ in $\BB_i$.
		
		\[
			X \oplus_i L_0^i Y := \left(R_{i-1}^i \oplus_{i-1} L_0^{i-1} Y, (R_0^{i-1} \inj_1^{i-1})_\UU \circ \Cstr_i^X \circ (\inj_1^{i-1} \circ \dash)^{-1}\right)
		\]
		
		Here, $(\inj_1^{i-1} \circ \dash)^{-1}$ is the inverse of the isomorphism of hypothesis H3', and 
		
		The constructor goes as follows:
		\[
			\Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y) \equiv \Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,R_{i-1}^i X) \to (R_0^{i-1} X)_\UU \to (R_0^i (R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y))_\UU
		\]
		
		The first injector $X \to X \oplus_i L_0^i Y$ is defined as follows:
		\[
			\inj_1^i := \inj_1^{i-1} : R_{i-1}^i X \to R_{i-1}^i (X \oplus_i L_0^i Y) = R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y
		\]
		
		It is a morphism of $\BB_i$ as it makes the following diagram commute:
		
		\begin{center}
			% YADE DIAGRAM D4.json
			% GENERATED LATEX
			\input{graphs/D4.tex}
			% END OF GENERATED LATEX
		\end{center}
		
		
		The second injector is defined as follows:
		\[
			inj_2^i := (\varepsilon_i \oplus_i \id_{L_0^i Y}) \circ L_{i-1}^i \inj_2^{i-1}
		\]
		
		Where $\varepsilon_i$ is the counit of the adjunction $R_{i-1}^i \vdash L_{i-1}^i$, going from $L_{i-1}^i R_{i-1}^i X$ to $X$.
		
		This goes from $L_0^i Y = L_{i-1}^i L_0^{i-1} Y$ to $L_{i-1}^i(R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y)$, which is equivalent to $L_{i-1}^i R_{i-1}^i X \oplus_i L_0^i Y)$ as $L_{i-1}^i$ is a left-adjunct functor and therefore it preserves colimits; then goes to $X \oplus_i L_0^i Y$.
		
		We will now show that this definition is actually a definition of the coproduct in $\BB_i$.
		To that extent, we take two objects $X$ and $Z$ in $\BB_i$, $Y$ in $\TSet$ and two morphisms of $\BB_i$ $\varphi_1 : X \to Z$ and $\varphi_2 : L_0^i Y \to Z$.
		
		We define $\{\varphi_1 ; \varphi_2\}_{i	} = \{R_{i-1}^i \varphi_1 ; R_{i-1}^i \varphi_2 \circ \eta^i_{L_0^{i-1} Y}\}_{i-1}$ a morphism of $\BB_i$ as it makes the following diagram commute:
		
		\begin{center}
			% YADE DIAGRAM D5.json
			% GENERATED LATEX
			\input{graphs/D5.tex}
			% END OF GENERATED LATEX
		\end{center}
		
		
		\todo{Justifier $R_{i-1}^i(\varepsilon_i \oplus_i \id_{L_0^i Y}) = R_{i-1}^i \varepsilon_i \oplus_{i-1} \id_{L_0^{i-1} Y}$ (with H1 ?)}
		
	\subsection{Proof of H3}
	
		\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 D1.json
		% GENERATED LATEX
		\input{graphs/D1.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), λa.λ\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 ?}
	
	
		\subsection{$H$ functors}
	
	For every set $X$, we define the functor $H_X : (X/\Set) \to \TSet$
	\[
	H_X(Y,f) = \TSetObject{X}{f}{Y}
	\]
	
	Dually, we make another functor $\Hbar_X : (\Set/X) \to \TSet$
	\[
	\Hbar_X(Y,f) = \TSetObject{Y}{f}{X}
	\]
	
	The morphisms translate as-is, and composition and identity relies on that of $(X/\Set)$ or $(\Set/X)$.
	
	\todo{(small) Show that it is actually a functor (should be trivial), potentially add a diagram}
	
	
	\subsection{Overview}
	
	We use the specification of sorts definition of Fiore \cite{Fiore2008}.
	
	A specification of sorts is given by a sequence of functors $\Gamma_i : S_{i-1} \to \Set$. We construct the category $S_{i+1}$ by adding a single object $\alpha_{i+1}$ to the category $S_{i}$, 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$.
	
	We have define a sequence of direct categories $\emptyset = S_0 \subset S_1 \subset S_2 \subset \dots$ (with inclusions functors $I_i : S_{i+1} \to S_i$). We define the \enquote{final} direct category as $S = \bigcup S_i$
	
	This definition is an isomorphism, so we can define a GAT categorically as any locally finite direct category.
	
	Then the semantics of the GAT is described as the category of presheaves over $S$, written $[S, \Set]$.
	
	Altenkirsch has another way of constructing the semantics of a specification of sorts \cite{Altenkirch2018}, and he also describes a way to describe constructors.
	
	So we can construct the base category, which is that of families of sets.
	
	\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(\left\{g ; \varepsilon_0^i \circ L_0^{i-1} \square \right\}) \circ \inj_1^{i-1} = \left\{g ; \varepsilon_0^i \circ L_0^{i-1} \square \right\} \circ \inj_1^{i-1} = g
	\]
	
	The second component of $\phi_{XYZ} (\phi_{XYZ}^{-1}(g,h))$ follows the following diagram
	
	\begin{center}
		% YADE DIAGRAM D9.json
		% GENERATED LATEX
		\input{graphs/D9.tex}
		% END OF GENERATED LATEX
	\end{center}
	
	The diagram commutes as the following equality holds:
	\[
	\left(\left\{g ; \varepsilon_0^i \circ L_0^{i-1} \square \right\} \circ \inj^{i-1}_2\right)_\El = \left(\varepsilon_0^i \circ L_0^{i-1} \square\right)_\El = (\varepsilon_0^i)_\El \circ (L_0^{i-1} \square)_\El = \square_El = \pi_1 \circ h
	\]
	
	\todo{Justify $(\varepsilon_0^i)_\El = id_{\BB_i}$ and $(L_0^i(f))_\El = f_\El$}
	
	So, as the square is a pullback, we get the complete equality
	\[
	\phi_{XYZ} (\phi_{XYZ}^{-1}(g,h)) = (g,h)
	\]
	
	\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_1^{i-1} ; \varepsilon_0^i \circ L_0^{i-1} \square \right\}
	\]
	where $\square$ follows the following diagram
	
	\begin{center}
		% YADE DIAGRAM D10.json
		% GENERATED LATEX
		\input{graphs/D10.tex}
		% END OF GENERATED LATEX
	\end{center}
	
	We want to show that $\phi_{XYZ}^{-1} (\phi_{XYZ}(f))$. By definition of $\{;\}$ in $\BB_1$, it suffices to show that $\varepsilon_0^i \circ L_0^{i-1} \square = R_{i-1}^i f \circ \inj_1^{i-1}$.
	
	So it suffices to show that
	\[
	\square = R_0^{i-1}(R_{i-1}^i f \circ \inj_2^{i-1}) \circ \eta_0^{i-1} = R_0^i f \circ \left(R_0^{i-1} \inj_2^{i-1} \circ \eta_0^{i-1}\right) = R_0^i f \circ \inj_2^0
	\]
	
	The two required equalities are proved by the diagram above:
	
	\begin{align*}
		\square_\El = \left(R_0^i f \circ \inj_2^0\right)_\El \\
		\square_\UU = \left(R_0^i f \circ \inj_2^0\right)_\UU
	\end{align*}
	
	\todo{Expliciter à un endroit que $\Cstr^{W(X,Y)} = inj_2^\Set \circ \left(\inj_1^{i-1} \circ \dash\right)$ (déduit de la définition et de la forme de l'iso H3' et H1r=id)}
	
	\todo{Show $R_0^{i-1} \inj_2^{i-1} \circ \eta_0^{i-1} = \inj_2^0$}
	
	\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 D10.0.json
		% GENERATED LATEX
		\input{graphs/D10.0.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_{XYZ}(f \circ \ii \circ W(g,h))_1
		&=& R_{i-1}^i\left(f \circ \ii \circ (g \oplus L_0^{i-1} \Hbar(g,h))^+\right) \circ \inj_1^{i-1} \\
		&=& R_{i-1}^i f \circ R_{i-1}^i \ii \circ \left\{\inj_1^{i-1} \circ g; \dots\right\} \circ \inj_1^{i-1} \\
		&=& R_{i-1}^i f \circ R_{i-1}^i \ii \circ \inj_1^{i-1} \circ g \\
		&=& \left[E(f) \circ \phi_{X'Y'Z'}(\ii) \circ (g,h)\right]_1
	\end{array}\]
	
	The second components are defined as described by the following diagram
	
	\begin{center}
		% YADE DIAGRAM D11.json
		% GENERATED LATEX
		\input{graphs/D11.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 blue line. And that of $E(f) \circ \phi_{X'Y'Z'}(\ii) \circ (g,h)$ is defined by the circled path.
	As the diagram commutes and by pullback property, we get the equality.
	
	
\end{document}