Removing examples from the proof

Report/M2Report.tex

@@ -110,24 +110,403 @@
 		% END OF GENERATED LATEX
 	\end{center}
 	
+	\section{Examples}
+	\label{sec:Examples}
+	
+	Before making the formal proof, we will study our construction on three examples.
+	
+	\paragraph{Structure of the proof}
+	The formal proof will be 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 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)
+	\end{itemize}
+	
+	We will now present those objects on three specific examples in order to help getting an understanding of the logic behind the formal proof.
+	
+	\subsection{The empty sort specification}
+	
+		\label{sec:EmptySortSpec}
+	
+		Our first example is the empty sort specification. As our proof will we an induction on the number of sorts, its first step will always be creating the objects for this empty sort specification.
+		
+		\paragraph{Category of models of the empty sort specification}
+		
+			The category of models of the empty sort specification will simply be $\one$, the category with only one object $\star$ and one trivial morphism (i.e. the terminal category of $\Cat$). This is because the empty sort specification only has one model. We will denote this category as $\CC_0$.
+			
+		\paragraph{Category of models of the transformed GAT}
+			
+			The transformed GAT for the empty sort specification is the sort specification $(\mathcal{O},\El)$ (no constructors as there are no sort in the initial sort specification):
+			\vspace{.5ex}
+			\begin{center}
+				\renewcommand\arraystretch{1}
+				\begin{tabular}{|l|}
+					\hline
+					$\UU : \Set$ \\
+					$\El : \mathcal{O} \to \Set$ \\
+					\hline
+				\end{tabular}
+			\end{center}
+			\vspace{.5ex}
+			
+			The usual way of defining the category of models of this sort specification is by taking the category of families of sets $\FamSet$, whose objects are pairs of a set $X$ and a family of sets indexed by $X$ : $(Y_x)_{x\in 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$ with an equivalence we will see later (\autoref{SetXSetXEquivalence})
+			
+			With this formalisation, a model of this sort specification is a functor $X : \TT \to \Set$, such that
+			\begin{itemize}
+				\item $X_\UU$ is the set of the \enquote{sort objects}
+				\item For each sort object $A \in X_\UU$, the set of objects corresponding to the sort object is $X_p^{-1}(\{A\}) \subset X_\El$
+			\end{itemize}
+			
+			We will denote this category of models of the empty sort specification as $\BB_0$.
+			
+		\paragraph{Functors}
+			
+			We want to show that there is a coreflection between those two categories $\BB_0$ and $\CC_0$ as follows:
+			
+			\begin{center}
+				% YADE DIAGRAM AdjunctionLevel0.json
+				% GENERATED LATEX
+				\input{graphs/AdjunctionLevel0.tex}
+				% END OF GENERATED LATEX
+			\end{center}
+			
+			$F_0 : \TSet \to \one$ is simply the terminal functor of $\Cat$, i.e. the functor sending all objects to $\star$, the only object of $\one$, and all morphisms to $\id_\star$.
+			
+			$G_0 : \one \to \TSet$ is the functor that sends the only object of $\one$ to the initial object of $\TSet$: $0_\TSet$ (i.e. such that $G_0$ preserves colimits)
+			
+			We can check that those two functors create an adjunction, as 
+			\[
+				\Hom(G_0 \star,X) = \Hom(0_\TSet,X) \cong \one \cong \Hom(\star,F_0 X)
+			\]
+			
+			We also have that they create a coreflection, as $F_0G_0$ goes from $\one$ to $\one$, and so $F_0G_0 = \Id_\one$ as $\one$ is terminal in $\Cat$. So $F_0G_0$ is an isofunctor.
+			
+	\subsection{Type theory example}
+		
+		We will take as a first example the sort specification of type theory presented in the introduction. The sort specification and its transformation are as follows:
+		
+		\vspace{1ex}
+		\begin{center}
+		\renewcommand\arraystretch{1}
+		\begin{tabular}{|l|l|}
+			\hline
+			& $\UU : \Set$ \\
+			& $\El : \mathcal{O} \to \Set$ \\
+			$\Con : \Set$ & $\Con : \mathcal{O}$\\
+			$\Ty : (\Gamma : \Con) \to \Set$ & $\Ty : (\Gamma : \underline{\Con}) \to \mathcal{O}$\\
+			$\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set$ & $\Tm : (\Delta : \underline{\Con}) \to (A : \underline{\Ty\;\Delta}) \to \mathcal{O}$ \\
+			\hline
+		\end{tabular}
+		\end{center}
+		\vspace{1ex}
+		
+		We will build the following objects, step by step, adding one sort at a time:
+		
+		\begin{center}
+			% YADE DIAGRAM TypeTheoryConstruction.json
+			% GENERATED LATEX
+			\input{graphs/TypeTheoryConstruction.tex}
+			% END OF GENERATED LATEX
+		\end{center}
+		
+		Where the categories $\CC_i$ are the categories of models of the sort specification limited to the $i$ first sort declarations, and $\BB_i$ are the categories of models of the transformed GAT limited to the $i$ first sort declarations. For example, $\CC_2$ is the category of models of the two first sorts of the sort specification ($\Con$,$\Ty$). $\BB_0$,$\CC_0$,$F_0$, and $G_0$ have been defined in the last subsection.
+		
+		The $R^i_{i-1}$ functors between the categories are forgetful functors that forgets about the added sorts.
+		
+		I will only give here the explanation of functors $F_3$ and $G_3$, omitting the intermediate functors $F_1$,$G_1$,$F_2$,$G_2$. Their construction is given in the complete proof.
+		
+		\paragraph{Category of models}
+		
+			We have seen in the introduction a description of a model of the type theory sort specification. We will rebuild the category of those models inductively, adding one sort at a time.
+			
+			In order to construct those categories in a generic way, we will define functors $H_X : \CC_{X-1} \to \Set$ that will describe the \enquote{parameters} of the sort declaration.
+			
+			\[
+			\boxed{\Con : \Set}
+			\]
+			We begin with the following functor, corresponding to the sort declaration above
+			\[
+				H_\Con(\star) = 1 \in \Set
+			\]
+			
+			This functor means that $\Con$ takes no parameter i.e. there is only \emph{one} way of constructing a $\Con$.
+			
+			We build $\CC_1$ to be a pair of 
+			\begin{itemize}
+				\item An object $X_0$ of $\CC_0$
+				\item A family of sets $X_\Con$ indexed by $H_\Con(x) = 1$
+			\end{itemize}
+			
+			As there is only one object in $\CC_0$ and that a family of sets indexed by $1$ is simply a set, we have that this category $\CC_1$ is isomorphic to $\Set$ (i.e. the category of sets).
+			This 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 $\Ty$ takes one parameter of type $\Con$ i.e. There is exactly one $\Ty$ sort for every $\Con$ there is in the model.
+			
+			Again, we build $\CC_\Ty$ to be a pair of
+			\begin{itemize}
+				\item A model $X_\Con$ from $\CC_1$
+				\item A family of sets $X_\Ty$ indexed by $H_\Ty(X_\Con) = X_\Con$
+			\end{itemize}
+			
+			This category is, as expected, the category $\FamSet$ of families of sets i.e. objects are pairs of a set $X_\Con$ and of a family indexed by $X_\Con$: $(X_\Ty(\Gamma))_{\Gamma\in X_\Con}$.
+			
+			\[
+				\boxed{\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set}
+			\]
+			
+			The functor $\CC_2 \to \Set$ we will use here is defined as follows:
+			\[
+				H_\Tm(X_\Con,X_\Ty) = \coprod_{\Delta \in \Con}X_\Ty(\Delta) \in \Set
+			\]
+			
+			$\coprod$ denotes the coproduct or disjoint union in $\Set$. This functor means that $\Tm$ takes one parameter $\Delta$ of sort $\Con$ and one parameter of sort $\Ty\;\Delta$, i.e. there is exactly one $\Tm$ for every pair of a $\Con$ called $\Delta$ in the model, and of a $\Ty$ associated to $\Delta$ in the model.
+			
+			We build $\CC_3$ to be a pair of
+			\begin{itemize}
+				\item A model $(X_\Con,X_\Ty)$ from $\CC_2$
+				\item A family of sets $X_\Tm$ indexed by $H_\Tm(\Con)$
+			\end{itemize}
+			
+			This category is isomorphic to the category composed of triples of
+			\begin{itemize}
+				\item A set $X_\Con$
+				\item A family of sets indexed by $X_\Con$ : $\left(X_\Ty(\Gamma)\right)_{\Gamma \in X_\Con}$
+				\item A family of sets indexed by $(\Delta : X_\Con)$ and $X_\Ty(\Delta)$ :
+				$\left(\left(X_\Tm(\Delta,A)\right)_{A \in X_\Ty(\Delta)}\right)_{\Delta \in X_\Con}$
+			\end{itemize}
+			
+		\paragraph{Category of models of the transformed GAT}
+		
+			We have also seen in the introduction how was constructed the category of models of the transformed GAT. We will reconstruct it sort by sort.
+			
+			\[
+				\boxed{\begin{array}{c}
+					\mathcal{O} : \Set \\
+					\El : \mathcal{O} \to \Set
+				\end{array}}
+			\]
+			
+			We have seen in previous subsection that the category of models of this GAT is $\BB_0 = \TSet$. We will only add new \emph{constructors} to these models, and no new sorts.
+			
+			\[
+				\boxed{\Con : \mathcal{O}}
+			\]
+			
+			We are adding a constructor to the model. This constructor takes no parameters, which means we want to select one sort out of our model to be the $\Con$ sort. And we recall that the sorts of a model $X : \TSet$ are the elements of $X_\UU$.
+			
+			Therefore a model of the above GAT with only one constructor is a model $X : \TSet$ along with an object $\Cstr^X_\Con \in X_\UU$. An object of $\BB_1$ is a pair of
+			\begin{itemize}
+				\item A functor $X : \TT \to \Set$
+				\item An element $\Cstr^X_\Con \in X_\UU$
+			\end{itemize}
+			
+			A morphism $f$ from $(X,\Cstr^X_\Con)$ to $(X',\Cstr^{X'}_\Con)$ is simply a morphism of $\TSet$ from $X$ to $X'$ that respects the constructor, i.e. that is such that
+			\[
+				f_\UU(\Cstr^X_\Con) = \Cstr^{X'}_\Con
+			\]
+			
+			\[
+				\boxed{\Ty : \underline{\Con} \to \mathcal{O}}
+			\]
+			
+			Now the constructor we are adding takes one parameter. It means that for every element of $\El$ associated with $\Con$, there is an object in $\mathcal{O}$.
+			
+			This constructor translates into an object
+			\[
+				\Cstr^X_\Ty : X_p^{-1}(\Cstr^X_\Con) \to X_\UU
+			\]
+			
+			The codomain of this constructor means \enquote{Every object of $X_\El$ that are associated to the $\Con$ object of $X_\UU$ i.e. the object $\Cstr^X_\Con$}
+			This codomain is quite verbose, but we have another way of expressing it. In the final proof, we will have already constructed the functor $F_1 : \BB_1 \to \CC_1$, and we had a functor $H_\Ty : \CC_1 \to \Set$ that described the parameters of the sort declaration of $\Ty$ for the category $\CC_1$. It turns out that $H_\Ty \circ F_1 : \BB_1 \to \Set$ describes exactly the codomain expressed above.
+			\[
+				(H_\Ty \circ F_1) (X,\Cstr^X_\Con) = X_p^{-1}\left(\Cstr^X_\Con\right)
+			\]
+			
+			The fact that $H_X \circ F_{X-1}$ describes exactly the codomain of the constructor we want to add will hold for every sort declaration we can add.
+			
+			Therefore, the category $\BB_2$ consists of a pair of
+			\begin{itemize}
+				\item A model $(X,\Cstr^X_\Con)$ from $\BB_1$
+				\item A constructor $\Cstr^X_\Ty : H_iF_{i-1}(X,\Cstr^X_\Con) \to X_\UU$
+			\end{itemize}
+			
+			One again, a morphism $f$ from $(X,\Cstr^X_\Con,\Cstr^X_\Ty)$ to $(X',\Cstr^{X'}_\Con,\Cstr^{X'}_\Ty)$ is simply a morphism of $\BB_1$ from $(X,\Cstr^X_\Con)$ to $(X',\Cstr^{X'}_\Con)$ that does respect the $\Cstr_\Ty$ constructor, i.e. that verifies, for every $\Gamma$ in $H_iF_{i-1}(X,\Cstr^X_\Con)$ that
+			\[
+				f_\UU(\Cstr^X_\Ty(\Gamma)) = \Cstr^{X'}_\Ty(f_\El(\Gamma))
+			\]
+			
+			\[
+				\boxed{\Tm : (\Delta : \underline{\Con}) \to (A : \underline{\Ty\;\Delta}) \to \mathcal{O}}
+			\]
+			
+			This one is made like the others, a model of $\BB_3$ is a pair of
+			\begin{itemize}
+				\item A model $(X,\Cstr^X_\Con,\Cstr^X_\Ty)$ of $\BB_2$
+				\item A constructor $\Cstr^X_\Tm$ that goes from $H_\Tm F_2 X$ to $X_\UU$
+			\end{itemize}
+			
+			And morphism are restricted with the $\Tm$ constructor rule that states that for every $(\Delta,A)$ in $H_iF_{i-1}(X,\Cstr^X_\Con,\Cstr^X_\Ty)$
+			\[
+				f_\UU(\Cstr^X_\Tm(\Delta,A)) = \Cstr^{X'}_\Tm(f_\El(\Delta),f_\El(A))
+			\]
+			
+		\paragraph{Constructing $G_3$}
+		
+			We want to make functors connecting those two categories
+			\[
+				\begin{array}{l|l}
+					Y : \mathbf{\CC_3} & X : \mathbf{\BB_3} \\\hline
+					& X : \TSet\\
+					Y_\Con : \Set & \Cstr^X_\Con : X_\UU \\
+					\left(Y_\Ty(\Gamma)\right)_{\Gamma \in Y_\Con} &
+					\Cstr^X_\Ty : H_\Ty F_{1} (X,\Cstr^X_\Con) \to X_\UU \\
+					\left(\left(Y_\Tm(\Delta,A)\right)_{A \in Y_\Ty(\Delta)}\right)_{\Delta \in Y_\Con} &
+					\Cstr^X_\Tm : H_\Tm F_{2} (X,\Cstr^X_\Con,\Cstr^X_\Ty) \to X_\UU \\
+				\end{array}
+			\]
+			
+			Let's first look at the first component of the «result» $X = G_3(Y)$. It will be a functor of $\TSet$. We recall how $\TSet$ corresponds to the sort specification $(\mathcal{O},\El)$:
+			\begin{itemize}
+				\item $X_\UU$ is the set of all sorts
+				\item $X_\El$ is the set of all objects of those sorts
+				\item $X_p$ sends an object of a sort to the sort it corresponds to
+			\end{itemize}
+			
+			Therefore, we will construct $X_\UU$ to be the disjoint union of all the indices of the sets inside $Y$, $X_\El$ will be the disjoint union of all the sets inside $Y$, and $X_p$ will keep track of what is the index of a set.
+			
+			\[\begin{array}{ccccccc}
+				
+				X_\El & = &
+				Y_\Con & \oplus &
+				\displaystyle\coprod_{\Gamma \in Y_\Con}Y_\Ty(\Gamma) & \oplus &
+				\displaystyle\coprod_{\Delta \in Y_\Con}\coprod_{A \in Y_\Ty(\Delta)}Y_\Ty(\Delta,A) \\
+				\labeledupdownarrow{p}&&\labeledupdownarrow{}&&\labeledupdownarrow{\operatorname{proj}_1}&&\labeledupdownarrow{\operatorname{proj}_{2,1}}\\
+				X_\UU & = &
+				1 & \oplus &
+				Y_\Con & \oplus&
+				\displaystyle\coprod_{\Delta \in Y_\Con}Y_\Ty(\Delta)
+			\end{array}\]
+			where $\operatorname{proj}_1 : \coprod_{a\in A}B(a) \to A$ is the first projector of the coproduct, and $\operatorname{proj}_{2,1}$ get the index $ \coprod_{a \in A}B(a)$ of a double coproduct $\coprod_{a \in A}\coprod_{b\in B(a)} C(a,b)$
+			\vspace{.2ex}
+			
+			Now, the constructors only have to give the right sort according to their arguments. So
+			\[\begin{array}{lcl}
+				\Cstr^X_\Con &=& \inj_1(\star)\\
+				\Cstr^X_\Ty(\Gamma) &=& \inj_2(\Gamma) \\
+				\Cstr^X_\Tm(\Delta,A) &=& \inj_3(\Delta,A)
+			\end{array}\]
+			
+			where $\inj_i$ is the $i$-th injector of the direct sum $\oplus$.
+			
+			\begin{remark}
+				With this functor, every element of $X_\UU$ is reached by some constructor. And therefore, every object of $X_\El$ points to a sort that is reached by some constructor.
+			\end{remark}
+			
+			\todo{Parler des morphismes ? Est-ce nécessaire ?}
+			
+		\paragraph{Constructing $F_i$}
+			
+			We will now create an object $Y = F_i X$ of $\CC_3$ from an object $X$ of $\BB_3$.
+			
+			\begin{itemize}
+				\item $Y_\Con$ should be the set of all objects of sort $\Con$. In the transformed GAT, it means all objects of $\El$ which have been created with the sort $\Cstr^X_\Con$. Therefore we have
+				\[
+					Y_\Con = X_p^{-1}(\left\{\Cstr^X_\Con\right\}) \subseteq X_\El
+				\]
+				\item $Y_\Ty(\Gamma)$ should be the set of all objects of sort $\Ty\;\Gamma$, which means all objects of $\El$ which have been created with the sort $\Cstr^X_\Ty(\Gamma)$. Therefore we have, for every $\Gamma$ in $Y_\Con$
+				\[
+					Y_\Ty(\Gamma) = X_p^{-1}(\{\Cstr^X_\Ty(\Gamma)\})
+				\]
+				This is well-defined, as
+				\[
+					\Gamma : Y_\Con = X(p)^{-1}(\{\Cstr^X_\Con\}) = H_\Ty(X(p)^{-1}(\{\Cstr^X_\Con\})) = H_\Ty F_1(X,\Cstr^X_\Con)
+				\]
+				\item In the same way, we define
+				\[
+					Y_\Tm(\Delta,A) = X_p^{-1}(\Cstr^X_\Tm(\Delta,A))
+				\]
+				which is also well-defined
+			\end{itemize}
+			
+			\begin{remark}
+				We can see that the $F_3$ functor does not take into account elements of $X_\UU$ that are not \enquote{created} by one of the constructors, nor does it take into account the elements of $X_\El$ that are associated with those elements of $X_\UU$.
+				
+				This will later justify that when one adds elements to the base object $X$ of a model of $\BB_i$, then the image model by $F_i$ is unchanged, i.e. $F_i \inj_\tl^i$ is an isomorphism.
+			\end{remark}
+			
+		\paragraph{An adjunction}
+			
+			I will not do the proof that $F_3 \vdash G_3$, but i will give moral reasons of why the adjunction holds.
+			
+			An adjunction would be described by the following isomorphism:
+			\[
+				\Hom_{\BB_3}\left(G_3Y,X\right) \simeq \Hom_{\CC_3}\left(Y,F_3X\right)
+			\]
+			
+			Recall that sorts of $G_3Y$ are all in the domain of some constructor, so therefore, a morphism of $\Hom_{\BB_3}(G_3Y,X)$ only acts on constructible sorts.
+			Also, the only sorts that remain in $F_3X$ are the one that were reached by some constructor of $X$, therefore a morphism of $\Hom_{\CC_3}(Y,F_3X)$ only acts on constructible sorts.
+			
+			Therefore, both morphism are only descriptions of actions on constructible sorts into constructible sorts. That's how we create the isomorphism.
+		
+		\paragraph{A coreflection}
+		
+			If we look at $F_3G_3 Y$ for a model $Y$ of $\CC_3$, we remark that
+			\[\begin{array}{lcl}
+				F_3G_3(Y)_\Con &=& G_3(Y)_p^{-1}(\{\Cstr^{G_3(Y)}_\Con\})\\
+				&=& G_3(Y)_p^{-1}(\{\inj_1 \star\}) \\
+				&=& Y_\Con
+			\end{array}\]
+			and
+			\[\begin{array}{lcl}
+				F_3G_3(Y)_\Ty(\Gamma) &=& G_3(Y)_p^{-1}(\{\Cstr^{G_3(Y)}_\Ty(\Gamma)\})\\
+				&=& G_3(Y)_p^{-1}(\{\inj_2 \Gamma\}) \\
+				&=& \operatorname{proj}_1^{-1}(\Gamma) \\
+				&=& \left\{(\Gamma',A) \in \coprod_{\Gamma' \in Y_\Con}Y_\Ty(\Gamma') \middle| \Gamma' = \Gamma\right\}\\
+				&\simeq& Y_\Ty(\Gamma)
+			\end{array}\]
+			and finally, with the same method, we get that
+			\[
+				F_3G_3(Y)_\Tm(\Delta,A) \simeq Y_\Tm(\Delta,A)
+			\]
+			
+			And therefore $F_3G_3 \cong \Id_{\CC_3}$.
+			
+	\subsection{Another sort specification}
+	\todo{L'exemple, ou sinon remplacer toutes les occurences de «trois» par «deux»}
+		
 	\section{Constructing the coreflection}
 	
-		\paragraph{Structure of the proof}
+		The proof will take form of an induction on the number of sorts taken into account. At each induction step, we will build the following objects:
 		
-		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)$. 
+			\item A forgetful functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$. 
 			
-			Those functors compose themselves into a functor $R_0^i : \BB_i \to \BB_0$, that also creates limits:
+			Those functors compose themselves into a functor $R_0^i : \BB_i \to \BB_0$:
 			\[
-				R_0^i := R^1_0 \circ \dots \circ R_{i-1}^i
+			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}
@@ -138,7 +517,7 @@
 				\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)\]
@@ -146,7 +525,7 @@
 			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$
@@ -189,9 +568,10 @@
 		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}
+		\label{SetXSetXEquivalence}
 		
 		When the category $\mathcal{C}$ is $\Set$, we have the equivalence 
-		\[\Set/X \simeq \Set^X\]
+		\[\Set/X \cong \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
@@ -211,10 +591,9 @@
 		
 		Morphisms are translated using the same logic.
 		
-		\paragraph{Category of models of the two-sort sort specification}
+		This equivalence justifies that we used $\TSet$, the category of presheaves over $\TT$ instead of $\FamSet$ to describe the category of models of the sort specification $(\mathcal{O},\El)$ in \autoref{sec:EmptySortSpec}.
-		\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:
+		We recall that the category $\TT$ is as follows
-			
 		\begin{center}
 			% YADE DIAGRAM CategoryTT.json
 			% GENERATED LATEX
@@ -224,13 +603,7 @@
 		
 		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
+		The categories of models of the transformed GATs will be built atop of this category $\BB_0 = \TSet$.
-		\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}
 		
@@ -241,16 +614,16 @@
 		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$
+			This functor can be constructed using the formal construction of the Grothendieck construction of $\TSet \simeq (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$.
+		In this subsection, we will recall objects built in \autoref{sec:EmptySortSpec}, and build some other objects corresponding to the empty sort specification i.e. the first step of our induction.
 		
 		\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 $\CC_0$ is $\one$, the category with only one object $\star$ and one trivial morphism (i.e. the terminal category of $\Cat$)
-			\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 $\BB_0$ is $\TSet$, the category of models of the $(\mathcal{O},\El)$ sort specification.
 			\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$
@@ -268,13 +641,9 @@
 		\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.
+		In order to construct the categories, we need some object describing the sorts we are adding to the categories. This object is a given 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. They are such that, for $X : \CC_{i-1}$ a model, they describe the set $H_iX$ of parameter range for the added sort. We gave an example of those functors in section \nameref{sec:Examples} if you want to understand how they work. There is also a way of obtaining them directly from the syntax, described in section \nameref{sec:HiFromSyntax}.
 		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:
@@ -285,38 +654,6 @@
 		
 		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.
@@ -475,7 +812,7 @@
 		
 		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}
+		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 the introduction of this section.
 		
 		\[
 			\phi^{-1}_{XYZ}(g,h) := \left\{g ; \square \right\}
@@ -545,7 +882,6 @@
 		\]
 		
 		It is a morphism of $\BB_i$ as it makes the following diagram commute:
-		
 		\begin{center}
 			% YADE DIAGRAM TlInj1MorphismOfBi.json
 			% GENERATED LATEX
@@ -1111,6 +1447,11 @@
 
 
 
+
+
+
+
+
 
 
 

Report/graphs/AdjunctionLevel0.json

@@ -0,0 +1 @@
+{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":2,"label":{"kind":"normal","label":"F_0","style":{"alignment":"right","bend":0.10000000000000003,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":3,"label":{"kind":"normal","label":"G_0","style":{"alignment":"right","bend":0.10000000000000003,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":2,"id":4,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":3}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\TSet = \\BB_0","pos":[300,97],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\CC_0 = \\one","pos":[572,97],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}

Report/graphs/TypeTheoryConstruction.json

@@ -0,0 +1 @@
+{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":8,"label":{"kind":"normal","label":"F_3","style":{"alignment":"right","bend":0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":9,"label":{"kind":"normal","label":"G_3","style":{"alignment":"right","bend":0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":1,"id":10,"label":{"kind":"normal","label":"F_2","style":{"alignment":"right","bend":0.10000000000000003,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":11,"label":{"kind":"normal","label":"G_2","style":{"alignment":"right","bend":0.10000000000000003,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":5,"id":12,"label":{"kind":"normal","label":"G_1","style":{"alignment":"right","bend":0.10000000000000003,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":13,"label":{"kind":"normal","label":"F_1","style":{"alignment":"right","bend":0.10000000000000003,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":6,"id":14,"label":{"kind":"normal","label":"F_0","style":{"alignment":"right","bend":0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":15,"label":{"kind":"normal","label":"G_0","style":{"alignment":"right","bend":0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":0,"id":16,"label":{"kind":"normal","label":"R^3_2","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":17,"label":{"kind":"normal","label":"R^2_1","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":18,"label":{"kind":"normal","label":"R^1_0","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":0,"id":19,"label":{"kind":"normal","label":"R^3_0","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":13,"id":20,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":12},{"from":10,"id":21,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":11},{"from":8,"id":22,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":14,"id":23,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":15}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\BB_3","pos":[225,45],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\BB_2","pos":[225,135],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\BB_1","pos":[225,225],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\CC_3","pos":[405,45],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\CC_2","pos":[405,135],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"\\CC_1","pos":[405,225],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\BB_0","pos":[225,315],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"\\CC_0","pos":[405,315],"zindex":0}}],"sizeGrid":90,"title":"1"}]},"version":12}

Report/header.tex

@@ -146,6 +146,11 @@
 		\path[->] (0) edge["${\scriptstyle #2}$", pos=0.5, fore, black,=>, ] (1); 
 	\end{tikzpicture}
 }
+\newcommand\labeledupdownarrow[1]{
+\begin{tikzpicture} 
+	\path[->] (0,1) edge["${\scriptstyle #1}$", pos=0.5, fore, black,=>, ] (0,0); 
+\end{tikzpicture}
+}
 
 \newcommand\diagram[1]{\begin{tcolorbox}\begin{center}\vspace{1.5cm}\Huge \texttt{\textbf{#1}}\vspace{1.5cm}\end{center}\end{tcolorbox}}
 
@@ -161,4 +166,8 @@
 \titleformat{\subparagraph}[runin]{\normalfont\normalsize\bfseries}{}{0em}{\subparaghaphboxedcontent}
 \titlespacing*{\subparagraph}{0pt}{3.25ex plus 1ex minus .2ex}{0.5em}
 
+% Fixing Yade green
+\definecolor{green}{RGB}{11,102,35}
+
+
 \addbibresource{Bilibibio.bib}