Modification de la synthèse selon les commentaires

Y a juste un paquet qui foutait le zbeul

Report/Bilibibio.bib

@@ -1,56 +1,76 @@
-@InProceedings{Fiore2008,
+@inproceedings{Fiore2008,
-	author={Fiore, Marcelo},
+	author       = {Marcelo P. Fiore},
-	booktitle={2008 23rd Annual IEEE Symposium on Logic in Computer Science}, 
+	title        = {Second-Order and Dependently-Sorted Abstract Syntax},
-	title={Second-Order and Dependently-Sorted Abstract Syntax}, 
+	booktitle    = {Proceedings of the Twenty-Third Annual {IEEE} Symposium on Logic in
-	year={2008},
+	Computer Science, {LICS} 2008, 24-27 June 2008, Pittsburgh, PA, {USA}},
-	volume={},
+	pages        = {57--68},
-	number={},
+	publisher    = {{IEEE} Computer Society},
-	pages={57-68},
+	year         = {2008},
-	keywords={Algebra;Computer science;Mathematical model;Logic functions;Laboratories;MONOS devices;Sorting;abstract syntax;second-order syntax;dependently-sorted syntax;alpha-equivalence;variable binding;substitution;metavariable;meta-substitution;categorical algebra},
+	url          = {https://doi.org/10.1109/LICS.2008.38},
-	doi={10.1109/LICS.2008.38}
+	doi          = {10.1109/LICS.2008.38},
+	timestamp    = {Fri, 24 Mar 2023 00:01:50 +0100},
+	biburl       = {https://dblp.org/rec/conf/lics/Fiore08.bib},
+	bibsource    = {dblp computer science bibliography, https://dblp.org}
 }
 
-@InProceedings{Altenkirch2018,
+@inproceedings{Altenkirch2018,
-	author={"Altenkirch, Thorsten and Capriotti, Paolo and Dijkstra, Gabe and Kraus, Nicolai and Nordvall Forsberg, Fredrik"},
+	author       = {Thorsten Altenkirch and
-	editor={"Baier, Christel and Dal Lago, Ugo"},
+	Paolo Capriotti and
-	title={"Quotient Inductive-Inductive Types"},
+	Gabe Dijkstra and
-	booktitle={"Foundations of Software Science and Computation Structures"},
+	Nicolai Kraus and
-	year = 2018,
+	Fredrik Nordvall Forsberg},
-	publisher={"Springer International Publishing"},
+	editor       = {Christel Baier and
-	address={"Cham"},
+	Ugo Dal Lago},
-	pages={"293--310"},
+	title        = {Quotient Inductive-Inductive Types},
-	abstract={"Higher inductive types (HITs) in Homotopy Type Theory allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotient types, and allow to define types with non-trivial higher equality types, such as spheres, suspensions and the torus. However, there are also interesting uses of HITs to define types satisfying uniqueness of equality proofs, such as the Cauchy reals, the partiality monad, and the well-typed syntax of type theory. In each of these examples we define several types that depend on each other mutually, i.e. they are inductive-inductive definitions. We call those HITs quotient inductive-inductive types (QIITs). Although there has been recent progress on a general theory of HITs, there is not yet a theoretical foundation for the combination of equality constructors and induction-induction, despite many interesting applications. In the present paper we present a first step towards a semantic definition of QIITs. In particular, we give an initial-algebra semantics. We further derive a section induction principle, stating that every algebra morphism into the algebra in question has a section, which is close to the intuitively expected elimination rules."},
+	booktitle    = {Foundations of Software Science and Computation Structures - 21st
-	isbn={"978-3-319-89366-2"}
+	International Conference, {FOSSACS} 2018, Held as Part of the European
+	Joint Conferences on Theory and Practice of Software, {ETAPS} 2018,
+	Thessaloniki, Greece, April 14-20, 2018, Proceedings},
+	series       = {Lecture Notes in Computer Science},
+	volume       = {10803},
+	pages        = {293--310},
+	publisher    = {Springer},
+	year         = {2018},
+	url          = {https://doi.org/10.1007/978-3-319-89366-2\_16},
+	doi          = {10.1007/978-3-319-89366-2\_16},
+	timestamp    = {Sun, 04 Aug 2024 19:40:23 +0200},
+	biburl       = {https://dblp.org/rec/conf/fossacs/AltenkirchCDKF18.bib},
+	bibsource    = {dblp computer science bibliography, https://dblp.org}
 }
 
 @InProceedings{Munchhausen,
-	author =	{Altenkirch, Thorsten and Kaposi, Ambrus and \v{S}inkarovs, Artjoms and V\'{e}gh, Tam\'{a}s},
+	author       = {Thorsten Altenkirch and
-	title =	{{The M\"{u}nchhausen Method in Type Theory}},
+	Ambrus Kaposi and
-	booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
+	Artjoms Sinkarovs and
-	pages =	{10:1--10:20},
+	Tam{\'{a}}s V{\'{e}}gh},
-	series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
+	editor       = {Delia Kesner and
-	ISBN =	{978-3-95977-285-3},
+	Pierre{-}Marie P{\'{e}}drot},
-	ISSN =	{1868-8969},
+	title        = {The M{\"{u}}nchhausen Method in Type Theory},
-	year =	2023,
+	booktitle    = {28th International Conference on Types for Proofs and Programs, {TYPES}
-	volume =	{269},
+	2022, June 20-25, 2022, LS2N, University of Nantes, France},
-	editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
+	series       = {LIPIcs},
-	publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
+	volume       = {269},
-	address =	{Dagstuhl, Germany},
+	pages        = {10:1--10:20},
-	URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.10},
+	publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
-	URN =		{urn:nbn:de:0030-drops-184534},
+	year         = {2022},
-	doi =		{10.4230/LIPIcs.TYPES.2022.10},
+	url          = {https://doi.org/10.4230/LIPIcs.TYPES.2022.10},
-	annote =	{Keywords: type theory, proof assistants, very dependent types}
+	doi          = {10.4230/LIPICS.TYPES.2022.10},
+	timestamp    = {Mon, 31 Jul 2023 17:17:51 +0200},
+	biburl       = {https://dblp.org/rec/conf/types/AltenkirchKSV22.bib},
+	bibsource    = {dblp computer science bibliography, https://dblp.org}
 }
 @article{CartmellGATs,
-	title = {Generalised algebraic theories and contextual categories},
+	author       = {John Cartmell},
-	journal = {Annals of Pure and Applied Logic},
+	title        = {Generalised algebraic theories and contextual categories},
-	volume = {32},
+	journal      = {Ann. Pure Appl. Log.},
-	pages = {209-243},
+	volume       = {32},
-	year = 1986,
+	pages        = {209--243},
-	issn = {0168-0072},
+	year         = {1986},
-	doi = {https://doi.org/10.1016/0168-0072(86)90053-9},
+	url          = {https://doi.org/10.1016/0168-0072(86)90053-9},
-	url = {https://www.sciencedirect.com/science/article/pii/0168007286900539},
+	doi          = {10.1016/0168-0072(86)90053-9},
-	author = {John Cartmell}
+	timestamp    = {Fri, 21 Feb 2020 21:18:13 +0100},
+	biburl       = {https://dblp.org/rec/journals/apal/Cartmell86.bib},
+	bibsource    = {dblp computer science bibliography, https://dblp.org}
 }
 
 @phdthesis{SestiniPhD,

Report/M2Report.tex

@@ -89,7 +89,7 @@
 		$\dots$
 	\end{tabular}
 	
-	This process is useful when studying GATs, as it allows to restrict a study to GATs with only two sorts without loss of generality. Filippo Sestini noticed that in his thesis \cite{SestiniPhD}, although they didn't prove it.
+	This process is useful when studying GATs, as it allows to restrict a study to GATs with only two sorts without loss of generality. Filippo Sestini noticed that in his thesis \cite{SestiniPhD}:
 	
 	\begin{quote}
 		Many instances of multi-sorted IITs [IITs are a variant of GATs] can be reduced to equivalent two-sorted IITs, via a systematic reduction method originally observed by Zongpu (Szumi) Xie. We are not aware of a formal proof of this construction for arbitrary IITs, but we conjecture that it does apply to all instances of induction-induction and	consequently that it shows two-sorted IITs are enough to represent any specifiable IIT.
@@ -104,9 +104,9 @@
 	The category $\BB$ is equipped with a forgetful functor $R$ to $\BB_0$, the category of models of the two-sort sort specification $(\mathcal{O},\El)$.
 	
 	\begin{center}
-		% YADE DIAGRAM G1-0.json
+		% YADE DIAGRAM GlobalConstructionSimple.json
 		% GENERATED LATEX
-		\input{graphs/G1-0.tex}
+		\input{graphs/GlobalConstructionSimple.tex}
 		% END OF GENERATED LATEX
 	\end{center}
 	
@@ -156,9 +156,9 @@
 		
 		Here is a figure that describes the recursive construction of some of the above objects
 		\begin{center}
-			% YADE DIAGRAM G1.json
+			% YADE DIAGRAM GlobalRecursiveConstruction.json
 			% GENERATED LATEX
-			\input{graphs/G1.tex}
+			\input{graphs/GlobalRecursiveConstruction.tex}
 			% END OF GENERATED LATEX
 		\end{center}
 	
@@ -234,14 +234,14 @@
 		
 		\paragraph{$K$ functor}
 		
-		We define a helper functor $K : (X:C) \times (\Set/A(X)) \to \TSet$ defined as follows
+		We define a helper functor $K_A : (X:C) \times (\Set/A(X)) \to \TSet$ defined as follows
 		\[
-		K_X(X,(Y,f)) = \TSetObject{Y}{f}{A(X)}
+		K_A(X,(Y,f)) = \TSetObject{Y}{f}{A(X)}
 		\]
 		The morphisms are translated as-is.
 		
 		\begin{remark}
-			This functor can be constructed using the formal construction of the Grothendieck construction as a pullback in the category of categories $\Cat$
+			This functor can be constructed using the formal construction of the Grothendieck construction of $\TSet \cong (X: \Set) \times (\Set/X)$ as a pullback in the category of categories $\Cat$
 		\end{remark}
 	
 	\subsection{Initialization}
@@ -283,6 +283,8 @@
 		\]
 		and where $H_i$ is the specific functor described above.
 		
+		This way of constructing the category has formerly been described by Altenkirsch and al. \cite{Altenkirch2018}, with the only difference of the equivalence $\Set/H_i(X) \simeq \Set^{H_i(X)}$.
+		
 		\paragraph{An example of $H_i$ functors}
 		Let us now give an example of those $H_i$ objects for our type theory example.
 		
@@ -305,7 +307,6 @@
 		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}
 		\]
@@ -333,9 +334,9 @@
 		A morphism $X \to X'$ of $\BB_i$ is a morphism $f : R_{i-1}^iX \to R_{i-1}^iX'$ in $\BB_{i-1}$ such that the following diagram commutes.
 		
 		\begin{center}
-			% YADE DIAGRAM D1.json
+			% YADE DIAGRAM BiMorphismDiagram.json
 			% GENERATED LATEX
-			\input{graphs/D1.tex}
+			\input{graphs/BiMorphismDiagram.tex}
 			% END OF GENERATED LATEX
 		\end{center}
 		
@@ -350,9 +351,9 @@
 		The adjunction $F_i \vdash G_i$ is built using the two functors from the adjunction $F_{i-1} \vdash G_{i-1}$ defined in the previous induction step. We use them to define the first part of the adjunction, and we compose them with two adjoint functors $W$ and $E$ that we will define in this section. The overall construction for this induction step is as follows:
 		
 		\begin{center}
-			% YADE DIAGRAM G2.json
+			% YADE DIAGRAM InductionStepDiagram.json
 			% GENERATED LATEX
-			\input{graphs/G2.tex}
+			\input{graphs/InductionStepDiagram.tex}
 			% END OF GENERATED LATEX
 		\end{center}
 		
@@ -402,9 +403,9 @@
 		It is indeed a morphism of $\BB_{i}$ as it makes the following diagram commute.
 		
 		\begin{center}
-			% YADE DIAGRAM D2.json
+			% YADE DIAGRAM WghMorphismOfBi.json
 			% GENERATED LATEX
-			\input{graphs/D2.tex}
+			\input{graphs/WghMorphismOfBi.tex}
 			% END OF GENERATED LATEX
 		\end{center}
 	
@@ -419,18 +420,18 @@
 		Where $(A,h)$ is defined as the following pullback:
 		
 		\begin{center}
-			% YADE DIAGRAM D3a.json
+			% YADE DIAGRAM EDefinitionPullback.json
 			% GENERATED LATEX
-			\input{graphs/D3a.tex}
+			\input{graphs/EDefinitionPullback.tex}
 			% END OF GENERATED LATEX
 		\end{center}
 		
 		The action on a morphism $f$ from $X$ to $X'$ is defined as $E(f) = (R_{i-1}^i f, !)$, with $!$ being the only morphism making the following diagram commute (thanks to the pullback property):
 		
 		\begin{center}
-			% YADE DIAGRAM D3b.json
+			% YADE DIAGRAM EDefinitionMorphism.json
 			% GENERATED LATEX
-			\input{graphs/D3b.tex}
+			\input{graphs/EDefinitionMorphism.tex}
 			% END OF GENERATED LATEX
 		\end{center}
 		 
@@ -463,11 +464,12 @@
 		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
+			% YADE DIAGRAM PhiXYZSndComponentPullback.json
 			% GENERATED LATEX
-			\input{graphs/D6.tex}
+			\input{graphs/PhiXYZSndComponentPullback.tex}
 			% END OF GENERATED LATEX
-		\end{center}
+		
+\end{center}
 		
 	\subsubsection{Constructing $\phi^{-1}_{XYZ}$}
 		
@@ -484,20 +486,22 @@
 		Where $\square$ is a morphism $K_{H_iF_{i-1}} (X,Y) \to R_0^i Z$ in $\TSet$ defined by the following diagram:
 		
 		\begin{center}
-			% YADE DIAGRAM D7.json
+			% YADE DIAGRAM PhiXYZ-1Square.json
 			% GENERATED LATEX
-			\input{graphs/D7.tex}
+			\input{graphs/PhiXYZ-1Square.tex}
 			% END OF GENERATED LATEX
-		\end{center}
+		
+\end{center}
 		
 		Finally, we check that $\phi^{-1}_{XYZ}(g,h)$ is a morphism of $\BB_i$ from $W(X,Y)$ to $Z$, i.e. that it makes the following diagram commute:
 		
 		\begin{center}
-			% YADE DIAGRAM D8.json
+			% YADE DIAGRAM PhiXYZ-1MorphismOfBi.json
 			% GENERATED LATEX
-			\input{graphs/D8.tex}
+			\input{graphs/PhiXYZ-1MorphismOfBi.tex}
 			% END OF GENERATED LATEX
-		\end{center}
+		
+\end{center}
 	
 		In order to complete this proof, we need to show that
 		\begin{itemize}
@@ -516,7 +520,7 @@
 		
 		The proof is that statement is given in \autoref{apx:FG-refl}.
 			
-	\subsection{Inductive step: $\tl^i$}
+	\subsection{Inductive step: Constructing $\tl^i$}
 	
 		\label{sec:coproductConstr}
 		
@@ -543,9 +547,9 @@
 		It is a morphism of $\BB_i$ as it makes the following diagram commute:
 		
 		\begin{center}
-			% YADE DIAGRAM D4.json
+			% YADE DIAGRAM TlInj1MorphismOfBi.json
 			% GENERATED LATEX
-			\input{graphs/D4.tex}
+			\input{graphs/TlInj1MorphismOfBi.tex}
 			% END OF GENERATED LATEX
 		\end{center}
 		
@@ -563,9 +567,9 @@
 		We define $\{g ; h\}_i = \{R_{i-1}^i g ; h\}_{i-1}$. This is a morphism of $\BB_i$ as it makes the following diagram commute:
 		
 		\begin{center}
-			% YADE DIAGRAM D5.json
+			% YADE DIAGRAM TlUniversalMorphismIsOfBi.json
 			% GENERATED LATEX
-			\input{graphs/D5.tex}
+			\input{graphs/TlUniversalMorphismIsOfBi.tex}
 			% END OF GENERATED LATEX
 		\end{center}
 		
@@ -602,58 +606,170 @@
 
 		And we know from the previous induction step that $F_{i-1}\inj_\tl^{i-1}$ is an isomorphism. Therefore, $F_i\inj_\tl^i$ is an isomorphism.
 	
-	\section{Misc}
+	\section{Other Properties}
 	
+	\subsection{Fibration of the category $\CC_i$}
 	
+	In the formal proof, we defined $\CC_i$ as an inductive Grothendieck construction as in Altenkirsch and al. papers \cite{Altenkirch2018}.
 	
-	\subsection{Fiore's Category - Fibration of the category of sorts}
+	But there is an other way \cite{Fiore2008} of building the category $\CC_i$ which is equivalent to the one presented above.
 	
-	Fiore \cite{Fiore2008} describes \emph{sort specifications} as countable simple direct categories (i.e. countable categories where all the arrows follow an unique direction and hom-sets are finite). The models of a GAT then are the presheaves over that category $S$: $\left[S,\Set\right]$.
+	With this other method, a sort specification is described by a countable simple direct category $S$ (i.e. a countable category where all the arrows follow an unique direction, and $\Hom$-sets are finite). The models of the sort specification are therefore the presheaves over the category $S$ called $\left[S,\Set\right]$.
 	
-	One can understand the correspondance between those categories and sort specifications as follows:
+	\paragraph{Constructing $S$ as a sequence}
-	\begin{itemize}
+	In order to fall back on the definition we gave in the formal proof, we will build the final countable simple direct category $S$ as a sequence $\emptyset = S_0,S_1,\dots,S_i$ where $S_i$ is the category describing the sort specification limited to the $i$ first sort declarations.
-		\item An object of the category is a sort of the specification.
-		\item An arrow $x$ from an object $s$ to an object $s'$ is a parameter of the sort declaration of $s$ of the for $(x : s' \dots)$.
-		\item The parameter $y$ of a parameter $x$ of a sort specification (i.e. the sort declaration parameter has the form $(x: s' \dots \left[y=z\right] \dots)$) is given by $z = x \circ y$.
-	\end{itemize}
 	
-	\begin{remark}
+	The input data describing the GAT will be a sequence of finite functors $\Gamma_i : S_{i-1} \to \Set$.
-		We ignore in this definition identity arrows, and we will do so in the rest of this document. Identities are the only arrows that are not «directed» in the direct category.
-		
-		Interpreting the identity arrow would mean having a parameter of type $s$ to construct the sort $s$. which loops in a self-dependency.
-		
-		You can assume in the rest of the document that the formalizations \enquote{all arrows} or \enquote{the arrows} pointing to/from exclude identity arrows.
-	\end{remark}
 	
-	\todo{Éventuellement changer tous les paramètres par la forme complète, exemple 
+	We will then construct the category $S_i$ by adding a single object $\alpha_i$ to the category $S_{i-1}$, along with morphisms $f : \alpha_j \to \alpha_{i+1}$ for $f \in \Gamma_{i+1}(\alpha_j)$ and $j \leq i$. The morphisms follow the composition condition, describing that every pair of morphisms $f : \alpha_j \to \alpha_{i+1}$ and $g : \alpha_k \to \alpha_{i+1}$ (i.e. $f\in\Gamma_{i+1}(\alpha_k)$ and $g\in\Gamma_{i+1}(\alpha_j)$) and for every morphism of $S_{i}$ $h : \alpha_j \to \alpha_k$, we have $\Gamma_{i+1}(h)(f) \circ f = g$.
-		\[
-		\operatorname{eq}: (\Gamma : \Con) \to (A : \Ty \left[\Gamma=\Gamma\right]) \to \Tm \left[\Gamma=\Gamma\right] \left[A=A\right] \to \Tm \left[\Gamma=\Gamma\right] \left[A=A\right] \to \Ty \left[\Gamma=\Gamma\right]
-		\]
-		C'est bien plus verbeux et en pratique pas utilisé, mais permet de mieux voir la «composition» dans la catégorie de Fiore.}
-	\todo{Est-ce qu'on fait une notation \enquote{arrow*} pour dire «flèche qui n'est pas l'identité» pour plus de rigueur ?}
 	
-	For example the category version of the specification of sorts of Type Theory given above is defined as:
+	Avec le formalisme de la construction de Grothendieck, on peut formaliser la construction de la nouvelle catégorie comme cela:
+	\[
+		S_i = S_{i-1} \times 
+	\]
 	
-	\begin{itemize}
+	The final category is simply $S = \bigcup S_i$.
-		\item There is three objects called $\Con$,$\Ty$, and $\Tm$.
-		\item The arrows are defined as
-		\begin{itemize}
-			\item There is no arrow going out of $\Con$
-			\item There is one arrow going out of $\Ty$: $\Gamma$ pointing to $\Con$.
-			\item There is two arrows going out of $\Tm$: $\Delta$ pointing to $\Con$ and $\Gamma$ pointing to $\Ty$.
-		\end{itemize} 
-		\item The $\Gamma$ parameter of $\Ty$ in the parameter $A$ of $\Tm$ is $\Delta$. Therefore, we have $\Delta = A \circ \Gamma$.
-	\end{itemize}
 	
-	The category is pictured below:
+	In our type theory example, the category $S$ is constructed as follows:
 	
 	\begin{center}
-		% YADE DIAGRAM B1.json
+	\begin{tabular}{c|c|c}
-		% GENERATED LATEX
+		$\boxed{\Con : \Set}$ &
-		\input{graphs/B1.tex}
+		$\boxed{\Ty : (\Gamma : \Con) \to \Set}$ &
-		% END OF GENERATED LATEX
+		$\boxed{\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set}$ \\
+		$S_1 = \qquad \Con$	&
+		$S_2 = \qquad \Con \leftarrow \Ty$ &
+		$S_3 = \qquad \Con \leftarrow \Ty \leftarrow \Tm$ \\
+		$\left[S_1,\Set\right] \simeq \CC_1$ &
+		$\left[S_2,\Set\right] \simeq \CC_2$ &
+		$\left[S_3,\Set\right] \simeq \CC_3$
+	\end{tabular}
 	\end{center}
 	
+	\begin{remark}
+		This definition is reversable (up to the order of the sorts), and therefore, one can define a sequence of $\Gamma_i$ functors from any countable simple direct category.
+	\end{remark}
+	
+	\paragraph{Falling back on the formal proof}
+	
+		In the formal proof, we used categories $\CC_i$ and functors $H_i : \CC_i \to \Set$. We now undertand that the categories $\CC_i$ are defined on top of the categories $S_i$ with $\CC_i := \left[S_i,\Set\right]$.
+		
+		In the same way, the functors $H_i : \CC_{i-1} \to \Set$ are defined on top of the functors $\Gamma_i$ with the following relation:
+		\[
+			H_i(X) := \Hom_{\left[S_{i-1},\Set\right]}\left(\Gamma_i,X\right)
+		\]
+	
+	\subsection{Creating semantics object from the syntax}
+		\label{sec:HiFromSyntax}
+		
+		In this part, we will see how the functors $\Gamma_i$ given above can be constructed from the syntax of a sort specification. The previous subsection gives us a way of constructing the $H_i$ functors from the $\Gamma_i$ functors, and thus one can make the complete proof with the definition below.
+		
+		\paragraph{Verbose sort specification}
+		We will take a verbose version of a sort specification, where when \enquote{implementing} a sort, we gave the name of the parameter and the name of the term. For example, our type theory example becomes the following verbose version:
+		
+		\begin{center}
+		\renewcommand\arraystretch{1.5}
+		\begin{tabular}{l}
+			$\Con : \Set$\\
+			$\Ty : (\Gamma : \Con) \to \Set$ \\
+			$\Tm : (\Delta : \Con) \to (A : \Ty \left[\Gamma \mapsto \Delta\right]) \to \Set$
+		\end{tabular}
+		\end{center}
+		\vspace{1em}
+		The only sort declaration that changes is that of $\Tm$ as it is the only one for which one of its parameter is a sort with parameters.
+		
+		With that verbose definition, a generic sort specification is a list of sort declarations indexed by $\mathbb{T}$, the fully ordered set of all sorts. The sort declarations are as follow, for a sort $T \in \mathbb{T}$
+		
+		\[
+			T : \left[x_a^T : U_T(a) \left[x^{U_T(a)}_{b} \mapsto x^T_{v_T(a,b)}\right]_{b\leq I_{U_T(a)}}\right]_{a \leq I_T} \to \Set
+		\]
+		
+		Where
+		\begin{itemize}
+			\setlength\itemsep{-.2em}
+			\item $I_T$ is the number of parameters of the sort $T$
+			\item $x^T_a$ is the $a$-th parameter of the sort $T$
+			\item $U_T(a)$ is the sort of the $a$-th parameter of the sort $T$ (we have $U_T(a) < T$)
+			\item $I_{U_T(a)}$ is the number of parameters of the sort $U_T(a)$ i.e. the number of arguments we have to give to make an object of sort $U_T(a)$
+			\item $x^{U_T(a)}_b$ is the $b$-th parameter of the sort $U_T(a)$
+			\item $v_T(a,b)$ is the index of the parameter of the sort $T$ given as the $b$-th parameter of the $a$-th parameter of the sort $T$ (we have $v_T(a,b) < a$)
+			\item The types of parameters have to be respected, therefore we must have the equality
+			\[
+				U_T(v_T(a,b)) = U_{U_T(a)}(b)
+			\]
+		\end{itemize}
+		
+		For example, for the above sort declaration, we would have
+		\begin{itemize}
+			\setlength\itemsep{-.2em}
+			\item $\mathbb{T} = \left\{\Con < \Ty < \Tm\right\}$
+			\item $I_\Con = 0$, $I_\Ty = 1$, $I_\Tm = 2$
+			\item $x^\Ty_1 = "\Gamma"$, $x^\Tm_1 = "\Delta"$, $x^\Tm_2 = "A"$
+			\item $U_\Ty(1) = \Con$, $U_\Tm(1) = \Con$, $U_\Tm(2) = \Ty$
+			\item $v_\Tm(2,1) = 1$ such that $x^\Tm_{v_\Tm(2,1)} = "\Delta"$ (associated to $x^\Ty_{b=1} = "\Gamma"$)
+		\end{itemize}
+		
+		\paragraph{Describing the category $S$}
+			
+			We will then describe what is the category $S$ corresponding to a given sort specification $(\mathbb{T},I,U,v)$
+			
+			Its objects are simply the sorts, i.e. the elements of $\mathbb{T}$.
+			
+			Morphisms from a sort $T_x$ to a different sort $T_y$ are described by $U$ and correspond to the parameters of the sort $T_x$ that are of sort $T_y$. In other words:
+			
+			\[
+				\Hom_{S}(T_x,T_y) = \left\{x^{T_x}_a\middle| a \leq I_{T_x} \text{ and } U_{T_x}(a) = T_y\right\}
+			\]
+			
+			We can see that the category is direct, because of the rule $U_T(a) < T$ i.e. if $T_x < T_y$ then $\Hom_S(T_x,T_y) = \emptyset$.
+			For every sort $T$, we define $\Hom_S(T,T)$ to contain only the identity morphism $\id_T$, for which composition rules are already defined.
+			
+			Composition is described by $v$, corresponding to\enquote{parameters of parameters}.
+			Let's take two morphisms $x^{T_x}_b : T_x \to T_y$ and $x^{T_y}_a : T_y \to T_z$. Their composition is defined by
+			\[
+				x^{T_y}_a \circ x^{T_x}_b = x^{T_x}_{v_{T_x}(a,b)}
+			\]
+			
+			This composition is well-defined as 
+			\[
+				U_{T_x}(v_{T_x}(a,b)) = U_{U_{T_x}(a)}(b) = U_{T_y}(b) = T_z
+			\]
+			
+			For our type theory example, the category $S$ is as follows
+			
+			\begin{center}
+				% YADE DIAGRAM TyThExampleSCat.json
+				% GENERATED LATEX
+				\input{graphs/TyThExampleSCat.tex}
+				% END OF GENERATED LATEX
+			\end{center}
+		
+		\paragraph{Creating the functor $\Gamma_i$}
+		
+			We know we can create the functors $\Gamma_i$ directly from a complete category $S$, but we will look more in detail what those functors mean related to the syntax.
+			
+			If we are given the category $S_{i-1}$ with objects corresponding to the $i-1$ sorts already defined.
+			
+			We want to build a finite functor $\Gamma_i : S_{i-1} \to \Set$ corresponding to the following sort declaration of a new sort $T_i$
+		
+			We will build $\Gamma_i$ as follows:
+			
+			\[
+				\Gamma_i(T_x) = \left\{x^{T_i}_a\middle| a \leq I_{T_i} \text{ and } U_{T_i}(a) = T_x\right\}
+			\]
+			
+			\[
+				\Gamma_i(x_b^{T_x} : T_x \to T_y)(x^{T_i}_a \in \Gamma_i(T_x)) = x^{T_i}_{v_{T_i}(a,b)}
+			\]
+			
+			This definition is redundant with that of the last paragraph, but it has the advantage of directly creating the functor $\Gamma_i$ that are used to create the functors $H_i$ and all the rest of the proof.
+	
+	\subsection{Non-recursive definitions}
+	
+	\subsubsection{Redefinition of $\BB_i$}
+	\subsubsection{Redefinition of $G_i$ and $F_i$}
+	\subsubsection{Non-direct base category}
+	
 	\subsection{Infinite construction of $\BB_i$}
 	\[
 	\BB_i := \left(X : \TSet, \Cstr : (a : S_{i-1}) \to \Hom_{\BB_{a-1}}(G_{a-1}\Gamma_a,R_{a-1}^i(\this)) \to X(\UU)\right)
@@ -661,9 +777,9 @@
 	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
+		% YADE DIAGRAM BiMorphismDiagram.json
 		% GENERATED LATEX
-		\input{graphs/D1.tex}
+		\input{graphs/BiMorphismDiagram.tex}
 		% END OF GENERATED LATEX
 	\end{center}
 	
@@ -695,46 +811,6 @@
 	
 	\todo{Show that those are the same functors as those defined recursively. Prove the adjunction/reflection infinitely ?}
 	
-	
-	\subsection{Adding 2-transformation of constructors}
-	\label{sec:constructors2trans}
-	\todo{Describe the process}
-	
-	\subsection{Overview}
-	
-	\subsubsection{$\CC$ as presheaf category}
-	\label{sec:CtoSSetFiore}
-	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.
-	
-	
-	In order to construct the $i$-th sort, we use a finite functor $\Gamma_i : S_{i-1} \to \Set$ describing entirely the sort declaration.
-	
-	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$.\inlinetodo{C'est sûr la deuxième partie ?}
-		
-		This equality allows us to construct the $\Gamma_i$ functors from the final $S$ category.
-	\end{remark}
-	
-	\subsection{Consructing the $H_i$ functors from the syntax}
-	\label{sec:HiFromSyntax}
-	
 	\section{Summary}
 		
 		\lipsum[2-3]
@@ -767,11 +843,12 @@
 	The second component of $\phi_{XYZ} (\phi_{XYZ}^{-1}(g,h))$ follows the following diagram
 	
 	\begin{center}
-		% YADE DIAGRAM D9.json
+		% YADE DIAGRAM CompositionSecondComponent.json
 		% GENERATED LATEX
-		\input{graphs/D9.tex}
+		\input{graphs/CompositionSecondComponent.tex}
 		% END OF GENERATED LATEX
-	\end{center}
+	
+\end{center}
 	
 	
 	\todo{Justifier que la partie du haut commute, i.e. que \[
@@ -790,9 +867,9 @@
 	where $\square$ follows the following diagram
 	
 	\begin{center}
-		% YADE DIAGRAM D10.json
+		% YADE DIAGRAM CompositionSquareConstruction.json
 		% GENERATED LATEX
-		\input{graphs/D10.tex}
+		\input{graphs/CompositionSquareConstruction.tex}
 		% END OF GENERATED LATEX
 	\end{center}
 	
@@ -810,9 +887,9 @@
 	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
+		% YADE DIAGRAM NaturalityDiagram.json
 		% GENERATED LATEX
-		\input{graphs/D10.0.tex}
+		\input{graphs/NaturalityDiagram.tex}
 		% END OF GENERATED LATEX
 	\end{center}
 	
@@ -831,9 +908,9 @@
 	The second components are defined as described by the following diagram
 	
 	\begin{center}
-		% YADE DIAGRAM D11.json
+		% YADE DIAGRAM NaturalityDoublePullbackDefinition.json
 		% GENERATED LATEX
-		\input{graphs/D11.tex}
+		\input{graphs/NaturalityDoublePullbackDefinition.tex}
 		% END OF GENERATED LATEX
 	\end{center}
 	
@@ -861,35 +938,35 @@
 	
 	Where $(A,h)$ is the pullback defined as
 	\begin{center}
-		% YADE DIAGRAM E1.json
+		% YADE DIAGRAM ReflectionFGPullback.json
 		% GENERATED LATEX
-		\input{graphs/E1.tex}
+		\input{graphs/ReflectionFGPullback.tex}
 		% END OF GENERATED LATEX
 	\end{center}
 	
 	We can extend this pullback with the two isomorphisms $\en_0^i$ and $H_iF_{i-1}(\inj_\tl^{i-1})$ in another pullback. This new pullback is over the injection morphism $\inj_2$ of the coproduct of $\TSet$, so the new pullback object is the second component of the $\bullet \oplus B$ i.e. $B$.
 	
 	\begin{center}
-		% YADE DIAGRAM E2.json
+		% YADE DIAGRAM ReflectionFGExtendedPullback.json
 		% GENERATED LATEX
-		\input{graphs/E2.tex}
+		\input{graphs/ReflectionFGExtendedPullback.tex}
 		% END OF GENERATED LATEX
 	\end{center}
 	
 	The first component of the isomorphism is the following isomorphism, where $\eta_{i-1}^{FG}$ if the counit of the adjunction $F_{i-1} \vdash G_{i-1}$, that we know to be an isomorphism from the induction hypothesis.
 	
 	\begin{center}
-		% YADE DIAGRAM E3.json
+		% YADE DIAGRAM ReflectionFGIsomorphismFirst.json
 		% GENERATED LATEX
-		\input{graphs/E3.tex}
+		\input{graphs/ReflectionFGIsomorphismFirst.tex}
 		% END OF GENERATED LATEX
 	\end{center}
 	
 	And the second component is made using the isomorphism constructed by the pullback, that makes the diagram commute.
 	\begin{center}
-		% YADE DIAGRAM E4.json
+		% YADE DIAGRAM ReflectionFGIsomorphismSecond.json
 		% GENERATED LATEX
-		\input{graphs/E4.tex}
+		\input{graphs/ReflectionFGIsomorphismSecond.tex}
 		% END OF GENERATED LATEX
 	\end{center}
 	
@@ -999,6 +1076,27 @@
 
 
 
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
 
 
 

Report/graphs/B1.json

@@ -1 +0,0 @@
-{"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\\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":1,"id":4,"label":{"kind":"normal","label":"\\Gamma","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":2,"id":5,"label":{"kind":"normal","label":"A","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":2,"id":6,"label":{"kind":"normal","label":"\\Delta","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Con","pos":[100,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Ty","pos":[300,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\Tm","pos":[500,100],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\circlearrowleft","pos":[302,76.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}

Report/graphs/TyThExampleSCat.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":2,"id":3,"label":{"kind":"normal","label":"\"A\"","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":4,"label":{"kind":"normal","label":"\"\\Gamma\"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":2,"id":5,"label":{"kind":"normal","label":"\"\\Delta\" \\;=\\; \\Gamma \\circ A","style":{"alignment":"right","bend":0.10000000000000003,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Con","pos":[100,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Ty","pos":[300,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\Tm","pos":[500,100],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}

Report/header.tex

@@ -1,11 +1,9 @@
 % Loading packages
 \usepackage{ae}
 \usepackage[T1]{fontenc}
-\usepackage[USenglish]{babel}
+\usepackage[english]{babel}
 \usepackage{fontspec}
 \usepackage{alphabeta}
-\usepackage{polyglossia}
-\usepackage{hyperref}
 \usepackage{bookmark}
 \hypersetup{
 	colorlinks=true,
@@ -27,7 +25,6 @@
 \usepackage{tcolorbox}
 \usepackage{mdframed}
 \usepackage{proof}
-\usepackage{biblatex}
 \usepackage{xparse}
 \usepackage{cprotect}
 \usepackage{titlesec}
@@ -45,6 +42,8 @@
 \usepackage{newunicodechar}
 \usepackage{txfonts}
 \usepackage{yade}
+\usepackage[backend=biber,style=numeric]{biblatex}
+\usepackage{hyperref}
 
 \usepackage[textheight=0.75\paperheight]{geometry}
 
@@ -162,5 +161,4 @@
 \titleformat{\subparagraph}[runin]{\normalfont\normalsize\bfseries}{}{0em}{\subparaghaphboxedcontent}
 \titlespacing*{\subparagraph}{0pt}{3.25ex plus 1ex minus .2ex}{0.5em}
 
-
 \addbibresource{Bilibibio.bib}

Report/synthese.tex

@@ -1,3 +1,4 @@
+% !TeX spellcheck = fr_FR
 \documentclass[11pt]{article}
 
 \usepackage[francais]{babel}
@@ -24,55 +25,32 @@
 	
 	\subsection*{Le contexte général}
 	
-	Les théories algébriques généralisées (ou GAT) sont des objects syntaxiques introduits en 1986 par Cartmell qui permettent la description d'objects algébriques, comme une généralisation des types inductifs de théorie des types.
+	Les théories algébriques généralisées (ou GAT) sont des objects syntaxiques introduits en 1986 par Cartmell qui permettent la description de structures algébriques, que l'on peut voir comme une généralisation des types inductifs de la théorie des types. Par exemple, on peut décrire les modèles d'une théorie des types à l'aide d'un GAT.
 	
 	Un GAT est constitué d'une liste de \enquote{sortes} décrivant les ensembles, généralement suivie d'une liste de \enquote{constructeurs}.
 	
-	\question{De quoi s'agit-il ?} 
-	\question{D'où vient-il ?}
-	\question{Quels sont les travaux déjà accomplis dans ce domaine dans le monde ?}
-	
 	\subsection*{Le problème étudié}
 	
-	Il existe un processus qui permet de transformer n'importe quel GAT en un GAT avec seulement deux sortes. Cette transformation a été utilisée par Philippo Sestini dans sa thèse, afin de restreindre son sujet d'étude. Cependant, il n'a pas été prouvé que cette transformation ne réduisait pas la généralité de sa thèse.
+	Il existe un processus qui permet de transformer n'importe quel GAT en un GAT avec seulement deux sortes. Cette transformation a notamment été exploitée par Filippo Sestini dans sa thèse, afin de restreindre son sujet d'étude. Cependant, il n'a pas été prouvé que cette transformation ne réduisait pas la généralité de sa thèse.
-	
-	\question{Quelle est la question que vous avez abordée ?}
-	\question{Pourquoi est-elle importante, à quoi cela sert-il d'y répondre ?}
-	\question{Est-ce un nouveau problème ?}
-	\question{Si oui, pourquoi êtes-vous le premier chercheur de l'univers à l'avoir posée ?}
-	\question{Si non, pourquoi pensiez-vous pouvoir apporter une contribution originale ?}
 	
 	\subsection*{La contribution proposée}
 	
-		Durant ce stage, j'ai recherché à formaliser sémantiquement cette transformation. J'ai commencé par l'appliquer à des exemples, trouver des propriétés sur ces exemple, pour ensuite formaliser dans la théorie des catégorie la transformation, et prouver formellement les propriétés que j'avais remarquées sur les exemples.
+	Durant ce stage, j'ai chercher à formaliser sémantiquement cette transformation. C'est à dire que je me suis intéressé directement aux catégories des modèles sans m'attacher à l'aspect syntaxique des GATs. Je me suis restreint à l'étude des \enquote{spécification de sortes}, c'est à dire aux GATs constitués uniquement d'une liste de sortes, sans constructeurs. J'ai commencé par appliquer la transformation sur des exemples simples, afin d'identifier des propriétés qui la justifient, le tout dans un cadre catégorique. Ensuite, j'ai énoncé et prouvé formellement ces propriétés dans leur plus grande généralité.
-	
-	\question{Qu'avez vous proposé comme solution à cette question ? 
-	Attention, pas de technique, seulement les grandes idées ! 
-	Soignez particulièrement la description de la démarche \emph{scientifique}.}
 	
 	\subsection*{Les arguments en faveur de sa validité}
 	
-		La preuve a été faite sémantiquement en essayant à chaque étape de généraliser les objets utilisés au maximum. Les constructions des objets sont basées sur des papiers déjà publiés, qui sont cités dans ce rapport.
+	La preuve a été faite sémantiquement en essayant à chaque étape de généraliser les objets utilisés au maximum. Les constructions des objets sont basées sur des papiers déjà publiés, qui sont cités dans ce rapport.
 		
-		La construction proposées et les propriétés établies prouvent également la conjecture établie par Philippo Sestini dans sa thèse.
+	La construction proposées et les propriétés établies prouvent également la conjecture établie par Philippo Sestini dans sa thèse.
 	
-	\question{Qu'est-ce qui montre que cette solution est une bonne solution ?}
-	\question{Des expériences, des corollaires ?}
-	\question{Commentez la \emph{robustesse} de votre proposition : 
-	comment la validité de la solution dépend-elle des hypothèses de travail ?}
 	
 	\subsection*{Le bilan et les perspectives}
 	
-		Nous avons formalisé la transformation sémantiquement, ce qui permet de gagner en généralité.
+	Nous avons formalisé la transformation sémantiquement, ce qui permet de gagner en généralité et de s'abstraire de l'aspect syntaxique des GATs.
-		Cette tranformation a été prouvée, et permet notamment de restreindre une étude aux seuls GATs à deux sortes.
+	Cette tranformation a été prouvée, et permet notamment de justifier une restriction d'une étude aux seuls GATs à deux sortes.
-		
+	
-		Cette transformation met en correspondanc de façon intéressante les \enquote{déclarations de sortes} et les \enquote{constructeurs}, ce qui permetterai évenuellement de les recouper dans une même notion.
+	Une prochaine étape serait de rajouter les constructeurs de termes à notre formalisation, en décrivant leur transformation et en adaptant les propriétés prouvées pour le cas des spécifications de sortes.
-		
+	
-		Nous avons également de quoi réfléchir à une généralisation des GATs qui décriraient par exemple des types mutuellement inductif, mais aussi d'autres objets plus \enquote{exotiques}. Il y a du travail à les étudier, et à observer l'effet de la transformation sur ces objets.
+	Nous avons également de quoi réfléchir à une généralisation des GATs qui décriraient par exemple des sortes définies l'une mutuellement contenue dans l'autre, et d'autres sortes plus \enquote{exotiques}. Il y a du travail à les étudier, et à observer l'effet de la transformation sur ces objets.
-		
-	\question{Et après ? En quoi votre approche est-elle générale ?}
-	\question{Qu'est-ce que votre contribution a apporté au domaine ?}
-	\question{Que faudrait-il faire maintenant ?}
-	\question{Quelle est la bonne \emph{prochaine} question ?}
 	
 \end{document}