Mysaa/M2Internship
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Changed intro to be more understandable

Browse Source
This commit is contained in:
Samy Avrillon 2024-07-16 17:09:22 +02:00
parent d247b98bc5
commit 545dbd7553
Signed by: Mysaa
GPG Key ID: 0220AC4A3D6A328B
7 changed files with 201 additions and 126 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
Report/Bilibibio.bib
View File

@ -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}
}

288
Report/M2Report.tex
View File

@ -19,90 +19,131 @@
\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$
\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}
For every element $\Gamma$ of the sort $\Con$, there is a sort $\Ty \Gamma$
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}
For every element $\Gamma$ of the sort $\Con$, and every element $A$ of the sort $\Ty \Gamma$, there is a sort $\Tm \Gamma\;F$
\end{center}
We can also add constructors to a sort specification.
\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 :
\[
\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)
\]
For the $i$-th constructor, we define the objects of $\BB_i$ as pairs of
\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}
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}

2
Report/graphs/B1.json
View File

@ -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}
{"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}

2
Report/graphs/D1.json
View File

@ -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}
{"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}

1
Report/graphs/G1-0.json Normal file
View File

@ -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}

10
Report/header.tex
View File

@ -1,5 +1,4 @@
% Loading packages
\usepackage{autofe}
\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

6
Report/yade-config.json Normal file
View File

@ -0,0 +1,6 @@
{
"watchedFile": "M2Report.tex",
"baseDir": "graphs",
"externalOutput": true,
"preambleFile": "yade-preamble.tex"
}