Ajout d'une partie exemples

Report/M2Report.tex

@@ -110,50 +110,408 @@
 		% END OF GENERATED LATEX
 	\end{center}
 	
-	\section{Constructing the coreflection}
+	\section{Example}
 	
-		\paragraph{Structure of the proof}
+	Before making the formal proof, we will construct and explain the objects on two examples.
+	\subsection{Structure of the proof}
+	
+	We will formalize the transformation for \emph{sort specifications} (i.e. lists of sort declarations).
+	
+	This 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 forgetful functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$. 
 		
-		We will formalize the transformation for \emph{sort specifications} (i.e. lists of sort declarations).
+		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
+		\]
+		\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}
 		
-		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}).
+		\begin{center}
+			% YADE DIAGRAM TlUniversal.json
+			% GENERATED LATEX
+			\input{graphs/TlUniversal.tex}
+			% END OF GENERATED LATEX
+		\end{center}
 		
-		At the $i$-th recursion step, we will build the following objects :
+		where $\en_0^i$ is the following composition:
-		\begin{itemize}
+		
-			\setlength\itemsep{-1ex}
+		\[\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)\]
-			\item The category of models of the GAT $\CC_i$
+		
-			\item The category of models of the transformed GAT $\BB_i$
+		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.
-			\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)$. 
+		
+		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}
+	
+	\subsection{The empty sort specification}
+	
+		Our proof will we an induction on the number of sorts, and so the first step will be creating the objects for the empty sort specification.
+		
+		Therefore we will build the following objects
+		
+		\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$.
 			
-			Those functors compose themselves into a functor $R_0^i : \BB_i \to \BB_0$, that also creates limits:
+		\paragraph{Category of models of the transformed GAT}
-			\[
+			
-				R_0^i := R^1_0 \circ \dots \circ R_{i-1}^i
+			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}
-			\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:
+			\begin{center}
-			\label{sec:tlUniversalProperty}
+				\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 TlUniversal.json
+				% YADE DIAGRAM CategoryTT.json
 				% GENERATED LATEX
-				\input{graphs/TlUniversal.tex}
+				\input{graphs/CategoryTT.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)\]
+			This category is equivalent to the catgegory $\FamSet$ with an equivalence we will see later\inlinetodo{Insérer la référence}
 			
-			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.
+			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 $\Gamma \in X_\UU$, the set of objects corresponding to the sort object is $X_p^{-1}(\{\Gamma\}) \subset X_\El$
+			\end{itemize}
 			
-			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$.
+			We will denote this category of models of the empty sort specification as $\BB_0$.
-			 
+			
-			\item A functor $F_i : \BB_i \to \CC_i$
+			We notice that the category $\BB_0$ has a coproduct that we will denote as $\tl^0$. The two injectors of this coproduct will be denoted as $\inj_1^0$ and $\inj_2^0$.
-			\item A functor $G_i : \CC_i \to \BB_i$
+			
-			\item An adjunction between them $F_i \vdash G_i$
+		\paragraph{Functors}
-			\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}$
+			We want to show that there is a reflection between those two categories $\BB_0$ and $\CC_0$ as follows:
-		\end{itemize}
+			
+			\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$ (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 how was a model of the type theory sort specification. We will rebuild that 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$. Well, it turns out that $H_\Ty \circ F_1 : \BB_1 \to \Set$ describes exactly the codomain expressed above.
+			
+			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, morphism $f$ from $(X,\Cstr^X_\Con,\Cstr^X_\Ty)$ to $(X',\Cstr^{X'}_\Con,\Cstr^{X'}_\Ty)$ are simply morphisms of $\BB_1$ from $(X,\Cstr^X_\Con)$ to $(X',\Cstr^{X'}_\Con)$ that 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} \\
+					& 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 indice 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_{\Gamma \in Y_\Con}Y_\Ty(\Gamma)
+			\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$.
+			
+			\todo{Parler des morphismes ? Est-ce nécessaire ?}
+			
+		\paragraph{Constructing $F_i$}
+			
+			Now we will try to 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.
+			
+			Morphisms of $\BB_3$ from $G_3Y$ to $X$ are morphisms of $\TSet$ that respect constructors. It means that 
+		
+		\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(Y)_p^{-1}(\{\Cstr^{G(Y)}_\Con\})\\
+				&=& G(Y)_p^{-1}(\{\inj_1 \star\}) \\
+				&=& Y_\Con
+			\end{array}\]
+			and
+			\[\begin{array}{lcl}
+				F_3G_3(Y)_\Ty(\Gamma) &=& G(Y)_p^{-1}(\{\Cstr^{G(Y)}_\Ty(\Gamma)\})\\
+				&=& G(Y)_p^{-1}(\{\inj_2 \Gamma\}) \\
+				&=& 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 \equiv \Id_{\CC_3}$.
+		
+	\section{Constructing the coreflection}
+	
 		Here is a figure that describes the recursive construction of some of the above objects
 		\begin{center}
 			% YADE DIAGRAM GlobalRecursiveConstruction.json
@@ -189,6 +547,7 @@
 		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\]
@@ -545,7 +904,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 +1469,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}