diff --git a/Report/Bilibibio.bib b/Report/Bilibibio.bib index a6cb63d..e9b3781 100644 --- a/Report/Bilibibio.bib +++ b/Report/Bilibibio.bib @@ -50,5 +50,15 @@ doi = {10.4230/LIPIcs.TYPES.2022.10}, annote = {Keywords: type theory, proof assistants, very dependent types} } - +@article{CartmellGATs, + title = {Generalised algebraic theories and contextual categories}, + journal = {Annals of Pure and Applied Logic}, + volume = {32}, + pages = {209-243}, + year = {1986}, + issn = {0168-0072}, + doi = {https://doi.org/10.1016/0168-0072(86)90053-9}, + url = {https://www.sciencedirect.com/science/article/pii/0168007286900539}, + author = {John Cartmell} +} diff --git a/Report/M2Report.tex b/Report/M2Report.tex index d77a0e9..1610f42 100644 --- a/Report/M2Report.tex +++ b/Report/M2Report.tex @@ -18,91 +18,132 @@ \tableofcontents \newpage - - \section{Introduction} - - \lipsum[7-9] - - \section{Content} - - Plan - - \begin{enumerate} - \item Présentation de ce qu'est un GAT, simple exemple - \item Présentation de la 2-sortification d'un GAT - \item Présentation de la catégorification de Fiore - \item Présentation de la catégorification de Altenkirsch -> Construction des $\BB_i$ récursive - \item Schéma de construction récursif de l'adjonction - \item Formulation de H1 et H3 - \item (ANNEXE?) Def de W et de E - \item (ANNEXE?) Preuve de l'adjonction / de la reflexion - \item (ANNEXE?) Preuve des propriétés - \item Définition infinie de $\BB_i$ -> Foncteur $R_0^iG_i$ -> Reflexions sur les catégories pas directes - \end{enumerate} - - + \section{Sort specification} - A Generalized Algebraic Theory (or GAT) and inductive-inductive types are syntaxes describing models. - Both are composed of a sort specification, and eventually a list of constructors. - In this document, we will not ask ourselves about the specificities of both syntaxes. A \enquote{vague} interpretation of them is enough to understand the constructions that follows. + A Generalized Algebraic Theory (or GAT), first introduced by Cartmell \cite{CartmellGATs}, is a syntactic specification of an algebraic structure. From a GAT, one can define a category of models describing the models of the algebraic structure. + A GAT starts with a sort specification i.e. a list of sort declarations, eventually followed by a list of constructors. + In this document, we will not ask ourselves about the specific syntax of GATs, a \enquote{vague} definition is enough. - A sort specification is a list of \emph{sort constructors} that are defined with \emph{parameters} with $\Set$ as its codomain. + \paragraph{Sort specification} - Here is an example of a classical sort specification for Type Theory. + A sort specification is a list of \emph{sort declarations} that are defined with \emph{parameters} with $\Set$ as its codomain. - \[ \Con : \Set \\ - \]\[ \Ty : (\Gamma : \Con) \to \Set \\ - \]\[ \Tm : (\Gamma : \Delta) \to (A : \Ty \Delta) \to \Set - \] - This specification is to be read as follows: + We give an example of a classical sort specification for Type Theory. On the right column we give the interpretation of the sort declaration on models. - \begin{center} - There is one sort that is $\Con$ - - For every element $\Gamma$ of the sort $\Con$, there is a sort $\Ty \Gamma$ - - For every element $\Gamma$ of the sort $\Con$, and every element $A$ of the sort $\Ty \Gamma$, there is a sort $\Tm \Gamma\;F$ - \end{center} + \vspace{1em} + \renewcommand\arraystretch{1.5} + \begin{tabular}{l|p{.5\textwidth}} + $\Con : \Set$ & A set of contexts\\ + $\Ty : (\Gamma : \Con) \to \Set$ & For each context $\Gamma$, a set of types in this context\\ + $\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set$ & For each context $\Gamma$ and each type $A$ in this context, a set of terms of this type. + \end{tabular} + \vspace{1em} - We can also add constructors to a sort specification. + A model of this category is a triple + \begin{itemize} + \item A set $X_\Con : \Set$ + \item A function $X_\Ty : X_\Con \to \Set$ + \item A function $X_\Tm : \displaystyle\coprod_{\Gamma : X_\Con} X_\Ty(\Gamma) \to \Set$ + \end{itemize} + + \paragraph{Constructor specification} + We can also add constructors to a sort specification to make a complete GAT. For example, for the previous sort specification, one can add the following constructors: + \vspace{1em} + \renewcommand\arraystretch{1.5} + \begin{tabular}{p{.37\textwidth}|p{.6\textwidth}} + $\operatorname{unit} : (\Gamma : \Con) \to \Ty\;\Gamma$ & In any context $\Gamma$, a type of $\Ty\;\Gamma$ called unit.\\ + + $\operatorname{eq}: (\Gamma : \Con) \to (A : \Ty\;\Gamma) \to$ + + $\qquad\Tm\;\Gamma A \to \Tm\;\Gamma A \to \Ty\;\Gamma$ & In any context $\Gamma$ and type $A$ in this context, for every terms $t$,$u$ of the type $A$, we have a type $\operatorname{eq} \Gamma A t u$ describing the equality of the terms. + \end{tabular} + \vspace{1em} + + This adds to the previous model two functions that \enquote{points} one element of the sets + \begin{itemize} + \item For each $\Gamma \in X_\Con$, an element $\operatorname{unit}\;\Gamma \in X_\Ty(\Gamma)$ + \item For each $\Gamma \in X_\Con$, for each $A \in X_\Ty(\Gamma)$, for each elements $u,v \in X_\Tm(\Gamma,A)$, an element $\operatorname{eq}\;\Gamma\;A\;u\;v \in X_\Ty(\Gamma)$ + \end{itemize} + + Sort declarations describe the sets that the model contains, whereas the constructors describe elements of these sets. + + \paragraph{Two-sortification} + + There is a process that allows us to transform a GAT into a GAT with only two sorts. This process is applied for example by Philippo Sestini \inlinetodo{manque une citation}, who asserts that one can build back an initial model + + this transformation preserves the existence of the initial model. + + The goal of this document is to prove semantically that this transformation creates an adjunction, and more precisely a reflective adjunction between the categories of models (and therefore preserving the existence of an initial model). + + We will now present this transformation. The sort specification of the GAT is always the same, and contains two sort declarations (as planned): + + \vspace{1em} + \begin{tabular}{p{0.37\textwidth}|p{0.5\textwidth}} + $\mathcal{O} : \Set$ & The set of sorts \\ + $\underline{\;\bullet\;} : \mathcal{O} \to \Set$ & For every sort object $o$ in the set of sorts, a set called $\underline{o}$ of objects corresponding to the sort object. + \end{tabular} + \vspace{1em} + + Category of models of this two-sort specification are intuitively the category of families of set $\FamSet$, composed of pairs $\left(X_0:\Set,X_1: X_0 \to \Set\right)$ (or $\coprod_{X : \Set}\Set$ in type theory). + + Then, we replace all occurrences of $\Set$ to $\mathcal{O}$, and we apply underline to every parameter. For example, the Type Theory GAT presented above becomes that which follows: + + \begin{tabular}{p{0.4\textwidth}|p{0.5\textwidth}} + $\Con : \mathcal{O}$ & One sort object is called \enquote{$\Con$} \\ + $\Ty : (\Gamma : \underline{\Con}) \to \mathcal{O}$ & + For each object $\Gamma$ corresponding to the sort object $\Con$, another sort object called \enquote{$\Ty\;\Gamma$} \\ + $\Tm : (\Gamma : \underline{\Con}) \to (A : \underline{\Ty\;\Delta}) \to \mathcal{O}$ & + For each object $\Gamma$ corresponding to the sort object $\Con$, + and for every object $A$ corresponding to the sort object $\Ty\;\Gamma$, another sort object called \enquote{$\Tm\;\Gamma\;A$}\\ + $\operatorname{unit} : (\Gamma : \Con) \to \Ty\;\Gamma$ & + For each object $\Gamma$ corresponding to the sort object $\Con$, an object called \enquote{$\operatorname{unit} \Gamma$} corresponding to the sort object $\Ty\;\Gamma$\\ + $\operatorname{eq}: (\Gamma : \Con) \to (A : \Ty\;\Gamma) \to$ \newline + $\qquad\Tm\;\Gamma A \to \Tm\;\Gamma A \to \Ty\;\Gamma$ & + $\dots$ + \end{tabular} + + \paragraph{Fiore's categories} + 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]$. + + One can understand the correspondance between those categories and sort specifications as follows: + \begin{itemize} + \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} + 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 \[ - \operatorname{unit} : (\Gamma : \Con) \to \Ty \Gamma - \] - \[ - \verb*|_| = \verb*|_|: (\Gamma : \Con) \to (A : \Ty \Gamma) \to \Tm \Gamma A \to \Tm \Gamma A \to \Ty \Gamma + \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 ?} - Constructors construct terms and not sorts. A sort specification with or without constructor describes a class of models, which are in the intuitive sense of a model (a model implements \enquote{sort constructors}, regular constructors). + For example the category version of the specification of sorts of Type Theory given above is defined as: - A known process is that one can transform a specification of sorts, into a specification of sorts with two sorts and constructors. - - The two sorts are always the same: - - \[ - \mathcal{O} : \square - \] - \[ - \underline{\;\bullet\;} : \mathcal{O} \to \square - \] - - Where $\mathcal{O}$ describes the \enquote{sort of sorts}, and $\underline{\;\bullet\;}$ give for every \enquote{sort object} the sort of the \enquote{objects of that sort}. - - Then, we replace all occurrences of $\Set$ to $\mathcal{O}$, and we apply underline to every sort constructor parameter. For example, the first Type Theory of sort specification becomes that which follows: - - \[ \Con : \mathcal{O} \\ - \]\[ \Ty : (\Gamma : \underline{\Con}) \to \mathcal{O} \\ - \]\[ \Tm : (\Gamma : \underline{\Con}) \to (A : \underline{\Ty \Delta}) \to \mathcal{O} - \] - - It is known that this new sorts and constructors specification is equivalent to the former one. - - Fiore \cite{Fiore2008} describes \emph{sort specifications} as countable simple direct categories. To every object, we associate a sort, which is built using parameters pointing out of them. We often write this category $S$, and for a sort $a$ in it, the parameters needed to construct the sort are indexed by $(a/S)*$. - - As an example, here is the category version of the above specification of sorts. We also add the equality $\Gamma \circ A = \Delta$. This equality describes that the $\Gamma$-parameter i.e. the first parameter of the $\Ty$ sort constructor is the variable $\Delta$. Without this equality, $\Gamma \circ A$ would be another arrow going from $\Tm$, and therefore another parameter on type $\Con$. + \begin{itemize} + \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: \begin{center} % YADE DIAGRAM B1.json @@ -111,36 +152,10 @@ % END OF GENERATED LATEX \end{center} - The category of models over a specification of sorts is then the category of presheaves over the category of Fiore $\left[S,\Set\right]$. + \paragraph{Fiore's category of the 2-sorts specification} - Altenkirsch \cite{Altenkirch2018} has another method to directly construct the category of models of a specification of sorts. His method is more general, but it does not give a \enquote{Tiny and simple} category as Fiore does. - The other advantage of Altenkirsch's method is that they give a way of also describing the models of a constructor specification. + If compute the small category associated to the two-sort specification described above, we obtain the simple category with two objects and one arrow between them. We call this category $\TT$ and write the objects as follows: - What we will do is to try to make an adjunction between Fiore's category of models $\left[S,\Set\right]$, and Altenkirsch's category of models of the two-sorted GAT. - - We will describe how the two categories are constructed in detail. - - \subsection{Constructing the categories} - - We will construct both categories $S$ and $\BB$ recursively, addings new sorts one by one. - - \subsubsection{Fiore's category} - - At the same time, we construct the simple category recursively $\emptyset = S_0,S_1,S_2,...$. - - In order to construct the $i$-th sort, we use a finite functor $\Gamma_i : \left[S_{i-1} \to \Set\right]$ describing entirely the sort constructor. - This functor is to be understood as $\Gamma_i(a)$ is the set of parameters of type $a$ for our new sort. In the above example, we would have $\Gamma_\Ty(\Con) = \{"\Gamma"\} = 1$ and $\Gamma_\Tm(\Con) = \{\Delta\}$,$\Gamma_\Tm(\Ty) = \{"A"\}$,$\Gamma_\Tm(\Gamma) = \left["A" \mapsto "\Delta"\right]$. - - Then, to construct $S_i$, we add one object $i$ to $S_{i-1}$, along with morphisms $x : i \to a$ for every $x \in \Gamma_i(a)$ for every $a$ in $S_{i-1}$. We also add equalities - $s \circ x = x'$ for every $s : b \to a$ and $x \in \Gamma_i(a)$ and $x' \in \Gamma_i(b)$ where $\Gamma_i(s)(x') = x$. - - \begin{remark} - We have that $\Hom_{S_i}(a,b) = \Gamma_b(a)$ or $(a/S_i)* \equiv \Gamma_a$.TODO C'est sûr la deuxième partie ? - \end{remark} - - \subsubsection{Altenkirsch's category} - - To start our series of category, we need the category of models of the two-sort specification of sorts ($\mathcal{O}$ and $\underline{\;\bullet\;}$). We do it Fiore's way and we get a simple category that we name $\TT$ with two elements and only one non-trivial arrow between them. \begin{center} % YADE DIAGRAM G0.json @@ -149,24 +164,73 @@ % END OF GENERATED LATEX \end{center} - The category of models $\TSet$ is also written $\BB_0$ as it is the first step of Altenkirsch's method of adding constructors. + The category of presheaves over this category is equivalent to the category $\FamSet$. + + \paragraph{Goal} + + The goal of this document is to make a relation between the category of models of the GAT $\left[S,\Set\right]$ and the category of models of the two-sortified GAT $\BB$. This relation will be an adjunction $F \vdash G$ that we will prove to be a coreflection. + + The category $\BB$ is built with an adjunction $R \vdash L$ to the category of models of the simple two-sort specification of sorts $\TSet$. + + \begin{center} + % YADE DIAGRAM G1-0.json + % GENERATED LATEX + \input{graphs/G1-0.tex} + % END OF GENERATED LATEX + \end{center} + + \subsection{Constructing the categories} + + We will construct both categories $S$ and $\BB$ recursively, adding new sorts one by one. + The categories $S_i$ are described as in Fiore's paper \cite{Fiore2008}, and the categories $\BB_i$ are constructed atop of the category $\TSet$ with a method inspired by the category of models described by Altenkirch et al. \cite{Altenkirch2018}. + + The first step of our recursion is the trivial adjunction $\lambda . \star \vdash \lambda . 1$ between the categories $\TSet = \BB_0$ and $\left[S_0,\Set\right] = \left[\emptyset,\Set\right] = 1$. + + Then we construct the category $S_i$ as a full supercategory of $S_{i-1}$ (and so we have a ff injection functor $I_i : S_{i-1} \to S_i$). + + We construct at the same time the category $\BB_i$ along with an adjunction $R_{i-1}^i \vdash L_{i-1}^i$ with $\BB_{i-1}$. + + The construction is summarized in the following diagram: + + \begin{center} + % YADE DIAGRAM G1.json + % GENERATED LATEX + \input{graphs/G1.tex} + % END OF GENERATED LATEX + \end{center} + + + \subsubsection{Fiore's category} + + 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} - Following Altenkirsch's construction of category of models for a sort specification, we end up on the category of families of sets $(X : \Set, Y : X \to \Set)$. - This category is equivalent to $\TSet$ which allows us to give a clearer definition of functors. + 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} + \subsubsection{2sort category} + + To start our series of categories, we use the category of models of the two-sort specification of sorts $\BB_0 := \TSet$. + Then, we recursively add constructors, constructing categories $\BB_1$,$\BB_2$, etc. - For the $i$-th constructor, we define the category $\BB_i$ as : + For the $i$-th constructor, we define the objects of $\BB_i$ as pairs of - \[ - \BB_i := \left(X : \BB_{i-1}, \Cstr_i : \Hom_{\BB_{i-1}} (G_{i-1}\Gamma_i,X) \to (R_0^{i-1}X)_\UU \right) - \] + \begin{itemize} + \item an object $X$ of $\BB_{i-1}$ + \item a \enquote{sort constructor} $\Cstr_i$ as a function $\Hom_{\BB_{i-1}} (G_{i-1}\Gamma_i,X) \to (R_0^{i-1}X)_\UU$ + \newline + where $\Gamma_i$ is the functor $S_{i-1} \to \Set$ that describe the sort constructor being processed, and $G_{i-1}$ is the left part of the adjunction $\left[S_{i-1}, \Set\right] \to \BB_{i-1}$ that we are defining recursively at the same time. + \end{itemize} - where $\Gamma_i$ is the functor $S_{i-1} \to \Set$ that describe the sort constructor being processed, and $G_{i-1}$ is the left part of the adjunction $\left[S_{i-1}, \Set\right] \to \BB_{i-1}$ that we are defining recursively at the same time. - A morphism $(X,\Cstr_i) \to (X',\Cstr'_i)$ in $\BB_i$ is a morphism $f : X \to X'$ in $\BB_{i-1}$ such that the following diagram commutes. + Morphisms $(X,\Cstr_i) \to (X',\Cstr'_i)$ in $\BB_i$ are morphisms $f : X \to X'$ in $\BB_{i-1}$ such that the following diagram commutes. \begin{center} % YADE DIAGRAM D1.json @@ -176,7 +240,7 @@ \end{center} Identities and compositions are that of the category $\BB_{i-1}$, and categorical equalities are trivially derived from the diagram above. - +seeing We also define a functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$ that sends objects and morphisms to their first component. This functor is a \emph{right adjunct} of another functor we call $L_{i-1}^i$. As we can compose the adjunctions $R_0^1$,$R_1^2$,...,$R_{i-1}^i$, we will create the two following syntactic sugars for the composed adjunctions. @@ -194,7 +258,7 @@ We know that this category has a coproduct, that we will denote $\oplus_i$ or just $\oplus$ when there is no ambiguity. We will also denote as $\inj_1^i : X \to X \oplus Y$ (resp. $\inj_2^i : Y \to X \oplus Y$) the first (resp. second) injector of the coproduct of $\BB_i$. For every morphisms $f : X \to Z$ and $g : Y \to Z$, we will denote with $\{f;g\}$ the unique morphism from $X \oplus Y$ to $Z$ such that $\{f;g\} \circ \inj^i_1 = f$ and $\{f;g\} \circ \inj^i_2 = g$. \begin{remark} - This adjunction and the existence of a coproduct comes from seeing $\BB_i$ being a category of algebras in $\BB_{i-1}$ over the arrow $inj_1 : G_{i-1}\Gamma_i \to G_{i-1}\Gamma_i \oplus L_0^{i-1} y\UU$. + This adjunction and the existence of a coproduct comes from seeing $\BB_i$ being a category of algebras in $\BB_{i-1}$ over the morphism $inj_1 : G_{i-1}\Gamma_i \to G_{i-1}\Gamma_i \oplus L_0^{i-1} y\UU$. \end{remark} \subsubsection{Summary} @@ -208,12 +272,6 @@ - \begin{center} - % YADE DIAGRAM G1.json - % GENERATED LATEX - \input{graphs/G1.tex} - % END OF GENERATED LATEX - \end{center} \subsection{Constructing the adjunction} @@ -392,7 +450,7 @@ - \subsection{$F \vdash G$ make a reflexion} + \subsection{$F \vdash G$ make a reflection} \subsection{Proof of H1 - Sum definition} diff --git a/Report/graphs/B1.json b/Report/graphs/B1.json index d7d4d66..3d21311 100644 --- a/Report/graphs/B1.json +++ b/Report/graphs/B1.json @@ -1 +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\\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":3,"label":{"isPullshout":false,"label":"\\Gamma","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":2,"id":4,"label":{"isPullshout":false,"label":"A","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":2,"id":5,"label":{"isPullshout":false,"label":"\\Delta","style":{"alignment":"right","bend":0.10000000000000003,"color":"black","dashed":false,"double":false,"head":"default","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":11} \ No newline at end of file +{"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":{"isPullshout":false,"label":"\\Gamma","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":2,"id":5,"label":{"isPullshout":false,"label":"A","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":2,"id":6,"label":{"isPullshout":false,"label":"\\Delta","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"double":false,"head":"default","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":11} \ No newline at end of file diff --git a/Report/graphs/D1.json b/Report/graphs/D1.json index 011e918..5b4efb6 100644 --- a/Report/graphs/D1.json +++ b/Report/graphs/D1.json @@ -1 +1 @@ -{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}\n\\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{---}\\;}}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"isPullshout":false,"label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":5,"label":{"isPullshout":false,"label":"R_0^i X_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"isPullshout":false,"label":"f \\circ \\dash","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":7,"label":{"isPullshout":false,"label":"\\Cstr^{X'}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Hom(G_{a-1},R_{a-1}^i(X))","pos":[180,60],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^iX)_\\UU","pos":[420,60],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i X')_\\UU","pos":[420,300],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(G_{a-1},R_{a-1}^i( X'))","pos":[180,300],"zindex":-10000}}],"sizeGrid":120,"title":"1"}]},"version":11} \ No newline at end of file +{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}\n\\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{---}\\;}}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"isPullshout":false,"label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":5,"label":{"isPullshout":false,"label":"R_0^i X_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"isPullshout":false,"label":"f \\circ \\dash","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":7,"label":{"isPullshout":false,"label":"\\Cstr^{X'}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Hom(G_{a-1},R_{a-1}^i(X))","pos":[180,60],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^iX)_\\UU","pos":[450,60],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i X')_\\UU","pos":[450,143],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(G_{a-1},R_{a-1}^i( X'))","pos":[180,143],"zindex":-10000}}],"sizeGrid":120,"title":"1"}]},"version":11} \ No newline at end of file diff --git a/Report/graphs/G1-0.json b/Report/graphs/G1-0.json new file mode 100644 index 0000000..9f360bb --- /dev/null +++ b/Report/graphs/G1-0.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\\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":5,"label":{"isPullshout":false,"label":"F","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":6,"label":{"isPullshout":false,"label":"G","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":2,"id":7,"label":{"isPullshout":false,"label":"L","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":0,"id":8,"label":{"isPullshout":false,"label":"R","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\BB","pos":[300,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\left[S,\\Set\\right]","pos":[500,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\TSet","pos":[300,300],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\vdash","pos":[301,203.8125],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\bot","pos":[395,100.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":11} \ No newline at end of file diff --git a/Report/header.tex b/Report/header.tex index 81a7413..40f41bc 100644 --- a/Report/header.tex +++ b/Report/header.tex @@ -1,5 +1,4 @@ -% Loading packages -\usepackage{autofe} +% Loading packages \usepackage{hyperref} \usepackage{bookmark} \hypersetup{ @@ -105,11 +104,12 @@ \newcommand\UU{{\ensuremath{\mathcal{U}}}} \newcommand\El{{\ensuremath{\operatorname{\mathcal{E}l}}}} \newcommand\ii{{\ensuremath{\mathbf{i}}}} -\newcommand\Con{{\ensuremath{\operatorname{Con}\;}}} -\newcommand\Ty{{\ensuremath{\operatorname{Ty}\;}}} -\newcommand\Tm{{\ensuremath{\operatorname{Tm}\;}}} +\newcommand\Con{{\ensuremath{\operatorname{Con}}}} +\newcommand\Ty{{\ensuremath{\operatorname{Ty}}}} +\newcommand\Tm{{\ensuremath{\operatorname{Tm}}}} \newcommand\Cstr{{\ensuremath{\operatorname{\mathcal{C}str}}}} \newcommand\Set{{\ensuremath{\operatorname{\mathcal{S}et}}}} +\newcommand\FamSet{{\ensuremath{\operatorname{\mathcal{F}am\mathcal{S}et}}}} \newcommand\Hom{{\ensuremath{\operatorname{\mathcal{H}om}}}} \newcommand\this{{\ensuremath{\operatorname{\texttt{this}}}}} \newcommand\Hbar{{\ensuremath{\overline{H}}}} @@ -150,7 +150,7 @@ \newcommand\diagram[1]{\begin{tcolorbox}\begin{center}\vspace{1.5cm}\Huge \texttt{\textbf{#1}}\vspace{1.5cm}\end{center}\end{tcolorbox}} \newcommand\todo[1]{\begin{tcolorbox}[colback=red!20!white,colframe=red!85!black,boxrule=4pt] #1 \end{tcolorbox}} - +\newcommand\inlinetodo[1]{\colorbox{orange}{#1}} % Création des environnements spécifiques au document diff --git a/Report/yade-config.json b/Report/yade-config.json new file mode 100644 index 0000000..1d0252d --- /dev/null +++ b/Report/yade-config.json @@ -0,0 +1,6 @@ +{ + "watchedFile": "M2Report.tex", + "baseDir": "graphs", + "externalOutput": true, + "preambleFile": "yade-preamble.tex" +}