Compare commits
3 Commits
d247b98bc5
...
e9da8a9107
| Author | SHA1 | Date | |
|---|---|---|---|
e9da8a9107
|
|||
|
b27dcbd2ca
|
|||
|
545dbd7553
|
@ -1,21 +1,12 @@
|
||||
@InProceedings{Fiore2008,
|
||||
|
||||
author={Fiore, Marcelo},
|
||||
|
||||
booktitle={2008 23rd Annual IEEE Symposium on Logic in Computer Science},
|
||||
|
||||
title={Second-Order and Dependently-Sorted Abstract Syntax},
|
||||
|
||||
year={2008},
|
||||
|
||||
volume={},
|
||||
|
||||
number={},
|
||||
|
||||
pages={57-68},
|
||||
|
||||
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},
|
||||
|
||||
doi={10.1109/LICS.2008.38}
|
||||
}
|
||||
|
||||
@ -24,7 +15,7 @@
|
||||
editor={"Baier, Christel and Dal Lago, Ugo"},
|
||||
title={"Quotient Inductive-Inductive Types"},
|
||||
booktitle={"Foundations of Software Science and Computation Structures"},
|
||||
year={"2018"},
|
||||
year = 2018,
|
||||
publisher={"Springer International Publishing"},
|
||||
address={"Cham"},
|
||||
pages={"293--310"},
|
||||
@ -40,7 +31,7 @@
|
||||
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
|
||||
ISBN = {978-3-95977-285-3},
|
||||
ISSN = {1868-8969},
|
||||
year = {2023},
|
||||
year = 2023,
|
||||
volume = {269},
|
||||
editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
|
||||
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
|
||||
@ -50,5 +41,38 @@
|
||||
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}
|
||||
}
|
||||
|
||||
@phdthesis{SestiniPhD,
|
||||
author = {Filippo Sestini},
|
||||
title = {Bootstrapping Extensionality},
|
||||
school = {University of Nottingham},
|
||||
year = 2023,
|
||||
month = mar
|
||||
}
|
||||
|
||||
@misc{AmbrusSzumiXie2sort,
|
||||
author = {Ambrus Kaposi},
|
||||
title = {Message to the Agda mailing list},
|
||||
howpublished = {\url{https://lists.chalmers.se/pipermail/agda/2019/011176.html}},
|
||||
year = 2019
|
||||
}
|
||||
|
||||
@misc{nlab:reflective_subcategory,
|
||||
author = {{nLab authors}},
|
||||
title = {reflective subcategory},
|
||||
howpublished = {\url{https://ncatlab.org/nlab/show/reflective+subcategory}},
|
||||
note = {\href{https://ncatlab.org/nlab/revision/reflective+subcategory/116}{Revision 116}},
|
||||
month = jul,
|
||||
year = 2024
|
||||
}
|
||||
@ -3,6 +3,10 @@
|
||||
|
||||
\input{./header.tex}
|
||||
|
||||
% po4a: environment remark
|
||||
% po4a: environment tikzpicture
|
||||
% po4a: environment property
|
||||
|
||||
\title{Categorical semantics of the reduction of GATs to two-sorted GATs.
|
||||
\\[1ex] \large Notes on my 4.5-month internship at the Laboratoire d'Informatique de l'École Polytechnique (Palaiseau, France)}
|
||||
\hypersetup{pdftitle={Categorical semantics of the reduction of GATs to two-sorted GATs}}
|
||||
@ -18,129 +22,98 @@
|
||||
\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 family of sets $\left(X_\Ty\left(\Gamma\right)\right)_{\Gamma \in _\Con}$
|
||||
\item A family of sets $\left(X_\Tm\left(\Delta,A\right)\right)_{\Delta\in X_\Con,\: A \in X_\Ty\left(\Delta\right)}$
|
||||
\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:
|
||||
|
||||
\[
|
||||
\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
|
||||
\]
|
||||
\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}
|
||||
|
||||
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).
|
||||
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}
|
||||
|
||||
A known process is that one can transform a specification of sorts, into a specification of sorts with two sorts and constructors.
|
||||
Sort declarations describe the sets that the model contains, whereas the constructors describe elements of these sets.
|
||||
|
||||
The two sorts are always the same:
|
||||
\paragraph{Two-sortification}
|
||||
|
||||
\[
|
||||
\mathcal{O} : \square
|
||||
\]
|
||||
\[
|
||||
\underline{\;\bullet\;} : \mathcal{O} \to \square
|
||||
\]
|
||||
There is a process that allows us to transform a GAT into a GAT with only two sorts. This process is used by Philippo Sestini in his thesis \cite{SestiniPhD} refering the work of Zongpu Szumi Xie \cite{AmbrusSzumiXie2sort}:
|
||||
|
||||
\begin{quote}
|
||||
Many instances of multi-sorted IITs [IITs are another type 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.
|
||||
\end{quote}
|
||||
|
||||
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}.
|
||||
The goal of this document is to prove semantically that this transformation makes sense. More specifically, we prove that this transformation is a left adjunct functor of a coreflection. This is enough to prove what Sestini conjectured, i.e. that the initial object in the 2-sort category creates back the initial object of the primary category \cite[5. General]{nlab:reflective_subcategory}.
|
||||
|
||||
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:
|
||||
We will now present this transformation. The sort specification of the transformed GAT is always the same, and contains two sort declarations (as planned):
|
||||
|
||||
\[ \Con : \mathcal{O} \\
|
||||
\]\[ \Ty : (\Gamma : \underline{\Con}) \to \mathcal{O} \\
|
||||
\]\[ \Tm : (\Gamma : \underline{\Con}) \to (A : \underline{\Ty \Delta}) \to \mathcal{O}
|
||||
\]
|
||||
\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}
|
||||
|
||||
It is known that this new sorts and constructors specification is equivalent to the former one.
|
||||
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)$.
|
||||
|
||||
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)*$.
|
||||
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:
|
||||
|
||||
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{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 : \underline{\Con}) \to \underline{\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 : \underline{\Con}) \to (A : \underline{\Ty\;\Gamma}) \to$ \newline
|
||||
$\qquad\underline{\Tm\;\Gamma A} \to \underline{\Tm\;\Gamma A} \to \underline{\Ty\;\Gamma}$ &
|
||||
$\dots$
|
||||
\end{tabular}
|
||||
|
||||
\paragraph{$\FamSet$ as functors}
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM B1.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/B1.tex}
|
||||
% 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]$.
|
||||
|
||||
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.
|
||||
|
||||
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.
|
||||
In the rest of the document, we will denote the simple category containing two elements and one non-identity arrow between them as $\TT$. The objects and arrow of this category are pictured below.
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM G0.json
|
||||
@ -149,115 +122,153 @@
|
||||
% 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.
|
||||
|
||||
\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.
|
||||
\end{remark}
|
||||
|
||||
Then, we recursively add constructors, constructing categories $\BB_1$,$\BB_2$, etc.
|
||||
|
||||
For the $i$-th constructor, we define the category $\BB_i$ as :
|
||||
The functors over this categories are equivalent to families of sets, using the following mapping :
|
||||
|
||||
\[
|
||||
\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{array}{l|l}
|
||||
X_\UU = X_0 & X_0 = X_\UU \\
|
||||
X_\El = \displaystyle\coprod_{A\in X_0}X_1(A) & X_1 = A \mapsto X_p^{-1}(\{A\})\\
|
||||
X_p = (A,B) \mapsto A &
|
||||
\end{array}
|
||||
\]
|
||||
|
||||
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.
|
||||
Therefore the categories of sorts of the transformed GATs will be built atop of the category $\TSet$ rather than atop of the category $\FamSet$ as it makes the formal proofs more elegant.
|
||||
|
||||
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.
|
||||
\paragraph{Goal}
|
||||
|
||||
The goal of this document is to make a relation between the category of models of the GAT $\CC$ 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 D1.json
|
||||
% YADE DIAGRAM G1-0.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/D1.tex}
|
||||
\input{graphs/G1-0.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
Identities and compositions are that of the category $\BB_{i-1}$, and categorical equalities are trivially derived from the diagram above.
|
||||
|
||||
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$.
|
||||
\subsection{Constructing the categories}
|
||||
|
||||
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.
|
||||
\[
|
||||
R_i^j = R_{i}^{i+1} \circ R_{i+1}^j = R_{i}^{j-1} \circ R_{j-1}^{j} = R_{i}^{i+1} \circ ... \circ R_{j-1}^{j}
|
||||
\]
|
||||
\[
|
||||
L_i^j = L_{j-1}^{j} \circ L_{i}^{j-1} = L_{i+1}^{j} \circ L_{i}^{i+1} = L_{j-1}^{j} \circ ... \circ L_{i}^{i+1}
|
||||
\]
|
||||
We will construct both categories $\CC$ and $\BB$ recursively, adding new sorts one by one.
|
||||
The categories $\CC_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 overall construction of the categories and of the adjunctions $F_i \vdash G_i$ is given below.
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM G1.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/G1.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
The first step of our recursion is the trivial adjunction $\lambda . \star \vdash \lambda . 1$ between the categories $\BB_0 = \TSet$ and $\CC_0 = 1$.
|
||||
|
||||
\subsubsection{Constructing $\CC_i$}
|
||||
|
||||
We construct the category $\CC_i$ as the following pair:
|
||||
\[
|
||||
\CC_i = (X : \CC_{i-1}) \times \Set^{\Hom(O_i,X)} \qquad\text{(this is a dependent coproduct)}
|
||||
\]
|
||||
where $O_i$ is a specific object of the category $\CC_{i-1}$, such that $\Hom(O_i,X)$ is the set of parameters for the construction of the new sort.
|
||||
|
||||
For example, for our type theory example, we first have
|
||||
\[
|
||||
O_1 = \star \in \operatorname{Obj}(\CC_0) = \operatorname{Obj}(1)
|
||||
\]
|
||||
so $\Hom(O_1,X) = 1$, which corresponds to the fact that $\Con$ takes no parameter.
|
||||
|
||||
Therefore $\CC_1 = 1 \times \Set^1 = \Set$
|
||||
|
||||
Then, we take the singleton object $O_2 = 1$ (this means, that types need \emph{one} context to be built), and so, for a set $X_\Con$, $\Hom(O_2,X_\Con) \cong X_\Con$, which corresponds to the fact that $\Ty$ take one $\Con$ as a parameter.
|
||||
|
||||
Therefore $\CC_2 = (X:\Set) \times \Set^X \cong \FamSet$.
|
||||
|
||||
Finally, we take the object $O_3 = (1, \lambda \star . 1)$ (this means that terms need \emph{one} context, and \emph{one} type of that context). With this object, for a pair $(X_\Con,X_\Ty)$ in $\CC_2$, we have $\Hom(O_3,(X_\Con,X_\Ty)) \cong \left(\Gamma: X_\Con, A: X_\Ty(\Gamma)\right)$.
|
||||
|
||||
The final category $\CC_3$ is composed of triples $(X_\Con: \Set, X_\Ty : X_\Con \to \Set, X_\Tm : (\Delta: X_\Con) \to X_\Ty(\Delta) \to \Set)$
|
||||
|
||||
\begin{remark}
|
||||
There is a way of getting the object $O_i$ from the syntax, which is given in \autoref{sec:CtoSSetFiore}.
|
||||
\end{remark}
|
||||
|
||||
\subsubsection{Constructing $\BB_i$}
|
||||
|
||||
\paragraph{The category} We construct the category $\BB_i$ as follows.
|
||||
|
||||
An object of $\BB_i$ is
|
||||
\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}O_i,X) \to (R_0^{i-1}X)_\UU$
|
||||
\newline
|
||||
where $O_i$ is the object of $\CC_{i-1}$ that describe the sort constructor being processed, and $G_{i-1}$ is the left part of the adjunction $\CC_{i-1} \to \BB_{i-1}$ that we are defining recursively at the same time.
|
||||
\end{itemize}
|
||||
|
||||
|
||||
A morphism $(X,\Cstr_i) \to (X',\Cstr'_i)$ of $\BB_i$ is a morphism $f : X \to X'$ in $\BB_{i-1}$ such that the following diagram commutes.
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM D1.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/D1.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
Identities and compositions are that of the category $\BB_{i-1}$, and categorical equalities are trivially derived from the diagram above.
|
||||
|
||||
\paragraph{The adjunction}
|
||||
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.
|
||||
\[\begin{array}{c}
|
||||
R_i^j = R_{i}^{i+1} \circ R_{i+1}^j = R_{i}^{j-1} \circ R_{j-1}^{j} = R_{i}^{i+1} \circ ... \circ R_{j-1}^{j}\\
|
||||
L_i^j = L_{j-1}^{j} \circ L_{i}^{j-1} = L_{i+1}^{j} \circ L_{i}^{i+1} = L_{j-1}^{j} \circ ... \circ L_{i}^{i+1}
|
||||
\end{array}\]
|
||||
|
||||
We will also denote $\eta_i^j : \mathbf{1} \to R_i^j L_i^j$ and $\varepsilon_i^j : L_i^j R_i^j \to \mathbf{1}$ to be the unit and counit of the adjunction $R_i^j \vdash L_i^j$.
|
||||
|
||||
\paragraph{The coproduct}
|
||||
For an object $X$ in $\BB_i$ and $Y$ in $\BB_0$, there is a coproduct $X \oplus_i L_0^i Y$ in the category $\BB_{i-1}$. We will denote as $\inj_1^i : X \to X \oplus L_0^iY$ (resp. $\inj_2^i : L_0^iY \to X \oplus L_0^iY$) the first (resp. second) injector of the coproduct of $\BB_i$. For every morphism $f : X \to Z$ and $g : L_0^iY \to Z$, we will denote with $\{f;g\}$ the unique morphism from $X \oplus L_0^iY$ to $Z$ such that $\{f;g\} \circ \inj^i_1 = f$ and $\{f;g\} \circ \inj^i_2 = g$.
|
||||
|
||||
We will also denote $\eta_i^j : \mathbf{1} \to R_i^j L_i^j$ and $\varepsilon_i^j : L_i^j R_i^j \to \mathbf{1}$ to be the unit and counit of the adjunction $R_i^j \vdash L_i^j$.
|
||||
\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 morphism $inj_1 : G_{i-1}O_i \to G_{i-1}O_i \oplus L_0^{i-1} y\UU$.
|
||||
\end{remark}
|
||||
|
||||
|
||||
\subsection{Some Hypotheses}
|
||||
|
||||
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$.
|
||||
\end{remark}
|
||||
|
||||
\subsubsection{Summary}
|
||||
|
||||
Here is a graph summarizing the categories and functors.
|
||||
We have constructed two chains of categories $\BB_0$,$\BB_1$,... and $S_0$,$S_1$,...
|
||||
|
||||
The categories $\BB_{i-1}$ and $\BB_{i}$ are in an adjunction written $R_{i-1}^i \vdash L_{i-1}^i$.
|
||||
|
||||
We will give in the next part the construction of the adjunction $F_i \vdash G_i$ at the step $i$. The functor $G_{i-1}$ is used in the definition of $\BB_i$, so the two recurrences have to be done at the same time.
|
||||
|
||||
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM G1.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/G1.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
|
||||
\subsection{Constructing the adjunction}
|
||||
|
||||
\subsubsection{Hypotheses}
|
||||
|
||||
In order to build and prove the adjunction, we will state hypotheses that we will progressively prove during our building of $\BB_i$, $F_i$, and $G_i$.
|
||||
In order to build and prove the adjunction, we will state some recurrence invariants that we will prove after having built objects.
|
||||
|
||||
\begin{property}[H1]
|
||||
\[
|
||||
\simpleArrow{R_{i-1}^i X \oplus L_0^{i-1} Y}{\left\{R_{i-1}^i \inj_1^i ; R_{i-1}^i \inj_2^i \circ \eta_{i-1}^i\right\}}{R_{i-1}^i(X \oplus_i L_0^i Y)}
|
||||
\]
|
||||
is an equivalence.
|
||||
\end{property}
|
||||
|
||||
\begin{property}[H1r]
|
||||
\[
|
||||
\simpleArrow{ R_{0}^i X \oplus_{i-1} Y}{\left\{R_{i-1}^i \inj_1^i ; \eta_{i-1}^i\right\}}{R_{i-1}^i(X \oplus_i L_0^i Y)}
|
||||
\]
|
||||
is an equivalence.
|
||||
is an isomorphism.
|
||||
|
||||
This property is proven easily by recursion over previous property H1.
|
||||
Its recursive version is the following isomorphism
|
||||
\[
|
||||
\simpleArrow{ R_{0}^i X \oplus_0 Y}{\left\{R_0^i \inj_1^i ; R_0^i \inj_2^i \circ \eta_0^i\right\}}{R_0^i(X \oplus_i L_0^i Y)}
|
||||
\]
|
||||
\end{property}
|
||||
|
||||
\begin{property}[H3]
|
||||
\[
|
||||
\simpleArrow{F_i X}{F(\inj_1^i)}{F_i(X \oplus L_0^i Y)}
|
||||
\]
|
||||
is an equivalence.
|
||||
\end{property}
|
||||
|
||||
\begin{property}[H3']
|
||||
\[
|
||||
\simpleArrow{\Hom(G_i\Gamma, X)}{(inj_1^i \circ \dash)}{\Hom(G_i\Gamma,X \oplus L_0^i Y)}
|
||||
\]
|
||||
is an equivalence.
|
||||
is an isomorphism.
|
||||
|
||||
This proven with the adjunction property of $F_i \vdash G_i$ and H3, as w have that
|
||||
We will often this equality along with the $F_i \vdash G_i$ adjunction (for an object $O$ in $\CC_i$)
|
||||
\[
|
||||
\Hom(G_i \Gamma, X) \cong \Hom(\Gamma, F_i X) \cong \Hom(\Gamma, F_i(X \oplus L_0^i Y)) \cong \Hom(G_i \Gamma, X \oplus L_0^i Y)
|
||||
\Hom(G_i O, X) \cong \Hom(O, F_i X) \cong \Hom(O, F_i(X \oplus L_0^i Y)) \cong \Hom(G_i O, X \oplus L_0^i Y)
|
||||
\]
|
||||
|
||||
This new isomorphism is the following:
|
||||
\[
|
||||
\simpleArrow{\Hom(G_i O, X)}{(inj_1^i \circ \dash)}{\Hom(G_i O,X \oplus L_0^i Y)}
|
||||
\]
|
||||
|
||||
\end{property}
|
||||
|
||||
\subsubsection{Decomposing the proof}
|
||||
\subsection{Constructing the functors}
|
||||
|
||||
In order to use all the power of the recurrence, we will build the $F_i \vdash G_i$ adjunction using the $F_{i-1} \vdash G_{i-1}$ adjunction, following the diagram below.
|
||||
|
||||
@ -268,25 +279,30 @@
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
The category $\left[S_i, \Set\right]$ is seen as the category $\left[S_{i-1},\Set\right]$ to which we have added an object along with morphisms described by $\Gamma_i$. The morphisms we added to the object $X$ have the shape of the slice category of the set $\Hom(\Gamma_i,X)$.
|
||||
|
||||
The first part $G_{i-1} \times \id \dashv F_{i-1} \times \id$ is proven and defined as an adjunction from the last step of the recurrence.
|
||||
|
||||
We will now define the two functors.
|
||||
The first part $G_{i-1} \times \id \dashv F_{i-1} \times \id$ is proven and defined as an adjunction from the previous step of the recurrence.
|
||||
|
||||
|
||||
\subsubsection{W definition}
|
||||
|
||||
We define a functor $W : \displaystyle\sum_{X : \BB_{i-1}} (\Set/\Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,X)) \to \BB_{i}$
|
||||
We define a functor $W : \left(X : \BB_{i-1}\right) \times \Set/\Hom_{\BB_{i-1}}(G_{i-1}O_i,X) \to \BB_{i}$
|
||||
|
||||
The action on objects is as follows:
|
||||
\[
|
||||
W(X,Y) := \left(X \oplus L_0^{i-1} \Hbar_{\Hom(G_{i-1}\Gamma_i,\dash)}(X,Y), \widetilde{\inj_2} \right)
|
||||
W(X,Y) := \left(X \oplus L_0^{i-1} \Hbar_{\Hom(G_{i-1}O_i,\dash)}(X,Y), \widetilde{\inj_2} \right)
|
||||
\]
|
||||
|
||||
With $\widetilde{\inj_2}$ being defined by
|
||||
Where $\Hbar_A(X,Y)$ is a functor $(X:C) \times (\Set/A(X)) \to \TSet$ with
|
||||
\[\begin{array}{c}
|
||||
\Hbar_A(X,Y)_\UU = A(X)\\
|
||||
\Hbar_A(X,Y)_\El = Y
|
||||
\end{array}\]
|
||||
|
||||
\todo{Réference de comment on crée le foncteur, pourquoi c'en est un, si c'est utile ...}
|
||||
|
||||
With $\widetilde{\inj_2}$ being defined by \inlinetodo{Changer les noms des hypothèses H3' et H1r}
|
||||
\[
|
||||
\begin{array}{lcl}
|
||||
\Hom(G_{i-1}\Gamma_i,X \oplus L_0^{i-1} \Hbar_\bullet(X,Y)) & \to^{\text{H3'}} & \Hom(G_{i-1}\Gamma_i,X)\\
|
||||
\Hom(G_{i-1}O_i,X \oplus L_0^{i-1} \Hbar_\bullet(X,Y)) & \to^{\text{H3'}} & \Hom(G_{i-1}O_i,X)\\
|
||||
& = & \Hbar_\bullet(X,Y)_\UU \\
|
||||
& \to^{\inj_2^0} & \left(R_0^{i-1}X \oplus \Hbar_\bullet(X,Y)\right)_\UU \\
|
||||
& \to^{\text{H1r}} & \left(R_0^{i-1}(X \oplus L_0^{i-1}\Hbar_\bullet(X,Y))\right)_\UU
|
||||
@ -295,7 +311,7 @@
|
||||
|
||||
The action on a morphism $(g,h)$ from $(X,Y)$ to $(X',Y')$ is the following:
|
||||
\[
|
||||
W(g,h) := \left(g \oplus L_0^{i-1} \Hbar_{\Hom(G_{i-1}\Gamma_i,\dash)}(g,h)\right)
|
||||
W(g,h) := \left(g \oplus L_0^{i-1} \Hbar_{\Hom(G_{i-1}O_i,\dash)}(g,h)\right)
|
||||
\]
|
||||
|
||||
It is indeed a morphism from $\BB_{i}$ as it makes the following diagram commute.
|
||||
@ -309,8 +325,9 @@
|
||||
|
||||
\subsubsection{E definition}
|
||||
|
||||
We define $E : \BB_{i} \to \displaystyle\sum_{X : \BB_{i-1}} (\Set/\Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,X))$
|
||||
We define $E : \BB_{i} \to \left(X : \BB_{i-1}\right) \times (\Set/\Hom_{\BB_{i-1}}(G_{i-1}O_i,X))$
|
||||
|
||||
The action on objects is
|
||||
\[
|
||||
E(X) = (R_{i-1}^i X, (A,h))
|
||||
\]
|
||||
@ -333,11 +350,11 @@
|
||||
\end{center}
|
||||
|
||||
|
||||
\subsubsection{Proof of the adjunction}
|
||||
\subsection{Proof of the adjunction}
|
||||
|
||||
We prove that $(W,E)$ make an adjunction showing that there is a natural isomorphism between $\Hom$ sets in both categories.
|
||||
|
||||
We want to construct for each $(X,Y)$ in $\displaystyle\prod_{X : \BB_{i-1}} (\Set/\Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,X))$ and $Z$ in $\BB_i$, an isomorphism $\phi_{XYZ}$.
|
||||
We want to construct for each $(X,Y)$ in $\displaystyle\prod_{X : \BB_{i-1}} (\Set/\Hom_{\BB_{i-1}}(G_{i-1}O_i,X))$ and $Z$ in $\BB_i$, an isomorphism $\phi_{XYZ}$.
|
||||
|
||||
\[
|
||||
\phi_{XYZ} : \Hom(W(X,Y),Z) \to \Hom((X,Y),E(Z))
|
||||
@ -345,7 +362,7 @@
|
||||
|
||||
I will give the construction of the isomorphisms and its inverse, the proofs are given in \autoref{apx:phi-WE-isnat}.
|
||||
|
||||
\paragraph{Constructing $\phi_{XYZ}$}
|
||||
\subsubsection{Constructing $\phi_{XYZ}$}
|
||||
|
||||
Let $f$ be in $\Hom(W(X,Y),Z)$.
|
||||
We want to construct $\phi_{XYZ}(f) : (X,Y) \to E(Z)$.
|
||||
@ -361,7 +378,7 @@
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
\paragraph{Constructing $\phi^{-1}_{XYZ}$}
|
||||
\subsubsection{Constructing $\phi^{-1}_{XYZ}$}
|
||||
|
||||
Now, we take $(g,h)$ a morphism from $(X,Y)$ to $E(Z)$.
|
||||
|
||||
@ -370,7 +387,7 @@
|
||||
\phi^{-1}_{XYZ}(g,h) := \left\{g ; \varepsilon_0^i \circ L_0^{i-1} \square \right\}
|
||||
\]
|
||||
|
||||
Where $\square$ is a morphism $\Hbar (X,Y) \to R_0^i Z$ defined by the following diagram:
|
||||
Where $\square$ is a morphism $\Hbar (X,Y) \to R_0^i Z$ in $\TSet$ defined by the following diagram:
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM D7.json
|
||||
@ -392,9 +409,15 @@
|
||||
|
||||
|
||||
|
||||
\subsection{$F \vdash G$ make a reflexion}
|
||||
\subsubsection{Properties of the adjunction}
|
||||
We have proven that $F_i \vdash G_i$ make a reflection, i.e. that $F_iG_i \cong \Id_{\CC_i}$.
|
||||
|
||||
\subsection{Proof of H1 - Sum definition}
|
||||
The proof is given in \autoref{apx:FG-refl}.
|
||||
|
||||
\subsection{Proof of the hypotheses}
|
||||
\subsubsection{Proof of H1}
|
||||
|
||||
\todo{Relire + réeexpliquer pourquoi ça prouve}
|
||||
|
||||
We will define the sums of the form $X \oplus_i L_0^i Y$ in $\BB_i$.
|
||||
|
||||
@ -448,9 +471,60 @@
|
||||
|
||||
\todo{Justifier $R_{i-1}^i(\varepsilon_i \oplus_i \id_{L_0^i Y}) = R_{i-1}^i \varepsilon_i \oplus_{i-1} \id_{L_0^{i-1} Y}$ (with H1 ?)}
|
||||
|
||||
\subsection{Proof of H3}
|
||||
\subsubsection{Proof of H3}
|
||||
|
||||
\subsection{Infinite construction of $\BB_i$}
|
||||
|
||||
\section{Misc}
|
||||
|
||||
\subsection{Fiore's Category - Fibration of the category of sorts}
|
||||
|
||||
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{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:
|
||||
|
||||
\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
|
||||
% GENERATED LATEX
|
||||
\input{graphs/B1.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
\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)
|
||||
\]
|
||||
@ -511,6 +585,8 @@
|
||||
|
||||
\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$.
|
||||
@ -525,6 +601,20 @@
|
||||
|
||||
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}
|
||||
|
||||
\section{Summary}
|
||||
|
||||
\lipsum[2-3]
|
||||
@ -645,4 +735,21 @@
|
||||
As the diagram commutes and by pullback property, we get the equality.
|
||||
|
||||
|
||||
\section{$F_i \vdash G_i$ reflection}
|
||||
\label{apx:FG-refl}
|
||||
|
||||
\todo{La preuve :/}
|
||||
|
||||
\end{document}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
@ -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}
|
||||
@ -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":{"kind":"normal","label":"\\Cstr^X","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":5,"label":{"kind":"normal","label":"R_0^{i-1} X_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"kind":"normal","label":"f \\circ \\dash","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":7,"label":{"kind":"normal","label":"\\Cstr^{X'}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Hom_{\\BB_{i-1}}(G_{i-1}O_i,X)","pos":[180,60],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^{i-1} X)_\\UU","pos":[450,60],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^{i-1} X')_\\UU","pos":[450,143],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom_{\\BB_{i-1}}(G_{i-1}O_i,X')","pos":[180,143],"zindex":-10000}}],"sizeGrid":120,"title":"1"}]},"version":12}
|
||||
File diff suppressed because one or more lines are too long
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"isPullshout":false,"label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":0,"id":5,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":6,"label":{"isPullshout":false,"label":"R_0^i(X)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":7,"label":{"isPullshout":false,"label":"\\Cstr^X_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3}],"nodes":[{"id":0,"label":{"isMath":true,"label":"A","pos":[100,117.8125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X)","pos":[100,317.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^i(X)_\\El","pos":[300,117.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"R_0^i(X)_\\UU","pos":[300,317.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":11}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":0,"id":5,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":6,"label":{"kind":"normal","label":"R_0^i(X)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":7,"label":{"kind":"normal","label":"\\Cstr^X_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3}],"nodes":[{"id":0,"label":{"isMath":true,"label":"A","pos":[100,117.8125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,R_{i-1}^i X)","pos":[100,195.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^i(X)_\\El","pos":[358,117.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"R_0^i(X)_\\UU","pos":[358,195.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":8,"label":{"isPullshout":false,"label":"","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":9,"label":{"isPullshout":false,"label":"R_0^i(X)_p","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":10,"label":{"isPullshout":false,"label":"h","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":11,"label":{"isPullshout":false,"label":"\\Cstr^X_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":12,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":13,"label":{"isPullshout":false,"label":"R_0^i(X')_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":4,"id":14,"label":{"isPullshout":false,"label":"h'","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":15,"label":{"isPullshout":false,"label":"\\Cstr^{X'}_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":0,"id":16,"label":{"isPullshout":false,"label":"!","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":1},"to":4},{"from":1,"id":17,"label":{"isPullshout":false,"label":"R_0^i(f)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":18,"label":{"isPullshout":false,"label":"\\dash \\circ R_{i-1}^i f","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.10000000000000003,"tail":"none"},"zindex":0},"to":7},{"from":2,"id":19,"label":{"isPullshout":false,"label":"R_0^i(f)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.6,"tail":"none"},"zindex":0},"to":6},{"from":14,"id":20,"label":{"isPullshout":true,"label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"double":false,"head":"","position":0,"tail":""},"zindex":0},"to":12},{"from":10,"id":21,"label":{"isPullshout":true,"label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"double":false,"head":"","position":0,"tail":""},"zindex":0},"to":8}],"nodes":[{"id":0,"label":{"isMath":true,"label":"A","pos":[125,125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"R_0^i(X)_\\El","pos":[375,125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^i(X)_\\UU","pos":[375,375],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X)","pos":[125,375],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"A'","pos":[243,200.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^i(X')_\\El","pos":[493,200.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"R_0^i(X')_\\UU","pos":[493,450.8125],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X')","pos":[243,450.8125],"zindex":-10000}}],"sizeGrid":250,"title":"1"}]},"version":11}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":8,"label":{"kind":"normal","label":"","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":9,"label":{"kind":"normal","label":"R_0^i(X)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":10,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":11,"label":{"kind":"normal","label":"\\Cstr^X_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":12,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":13,"label":{"kind":"normal","label":"R_0^i(X')_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":4,"id":14,"label":{"kind":"normal","label":"h'","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":15,"label":{"kind":"normal","label":"\\Cstr^{X'}_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":0,"id":16,"label":{"kind":"normal","label":"!","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":1},"to":4},{"from":1,"id":17,"label":{"kind":"normal","label":"R_0^i(f)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":18,"label":{"kind":"normal","label":"\\dash \\circ R_{i-1}^i f","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.10000000000000003,"tail":"none"},"zindex":0},"to":7},{"from":2,"id":19,"label":{"kind":"normal","label":"R_0^i(f)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":0},"to":6},{"from":14,"id":20,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":12},{"from":10,"id":21,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":8}],"nodes":[{"id":0,"label":{"isMath":true,"label":"A","pos":[125,115],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"R_0^i(X)_\\El","pos":[403,115],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^i(X)_\\UU","pos":[403,297],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,R_{i-1}^i X)","pos":[125,297],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"A'","pos":[249,190.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^i(X')_\\El","pos":[521,190.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"R_0^i(X')_\\UU","pos":[521,372.8125],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,R_{i-1}^i X')","pos":[249,372.8125],"zindex":-10000}}],"sizeGrid":250,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"isPullshout":false,"label":"","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":7,"label":{"isPullshout":false,"label":"(R_0^i Z)_p","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":8,"label":{"isPullshout":false,"label":"","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":9,"label":{"isPullshout":false,"label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":10,"label":{"isPullshout":false,"label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":11,"label":{"isPullshout":false,"label":"\\dash \\circ R_{i-1}^i f \\circ \\inj_1","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":4,"id":12,"label":{"isPullshout":false,"label":"\\left[R_{i-1}^i f \\circ \\inj_2\\right]_\\El","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":4,"id":13,"label":{"isPullshout":false,"label":"\\phi_{XYZ}(f)_2","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":0}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(z)","pos":[300,300],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[500,300],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[500,500],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i Z)","pos":[300,500],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"A","pos":[100,100],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X)","pos":[100,300],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":11}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"","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":7,"label":{"kind":"normal","label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":8,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":9,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":10,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":11,"label":{"kind":"normal","label":"\\dash \\circ R_{i-1}^i f \\circ \\inj_1","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.10000000000000003,"tail":"hook"},"zindex":8},"to":3},{"from":4,"id":12,"label":{"kind":"normal","label":"\\left[R_{i-1}^i f \\circ \\inj_2\\right]_\\El","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":4,"id":13,"label":{"kind":"normal","label":"\\phi_{XYZ}(f)_2","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":0},"to":0}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(z)","pos":[292,174],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[492,174],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[492,304],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,R_{i-1}^i Z)","pos":[292,304],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"A","pos":[100,100],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,X)","pos":[101,224.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"isPullshout":false,"label":"h","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":7,"label":{"isPullshout":false,"label":"\\pi_1","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":8,"label":{"isPullshout":false,"label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":9,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":10,"label":{"isPullshout":false,"label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":0,"id":11,"label":{"isPullshout":false,"label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":12,"label":{"isPullshout":false,"label":"g \\circ \\dash","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":13,"label":{"isPullshout":false,"label":"\\square_\\El","style":{"alignment":"left","bend":-0.10000000000000003,"color":"blue","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":5,"id":14,"label":{"isPullshout":false,"label":"\\square_\\UU","style":{"alignment":"right","bend":0.10000000000000003,"color":"blue","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3}],"nodes":[{"id":0,"label":{"isMath":true,"label":"Y","pos":[130,130],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"E(Z)","pos":[390,130],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[650,130],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[650,390],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i Z)","pos":[390,390],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X)","pos":[130,390],"zindex":-10000}}],"sizeGrid":260,"title":"1"}]},"version":11}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"h","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":7,"label":{"kind":"normal","label":"\\pi_1","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":8,"label":{"kind":"normal","label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":9,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":10,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":0,"id":11,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":12,"label":{"kind":"normal","label":"g \\circ \\dash","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":13,"label":{"kind":"normal","label":"\\square_\\El","style":{"alignment":"left","bend":-0.2,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":5,"id":14,"label":{"kind":"normal","label":"\\square_\\UU","style":{"alignment":"right","bend":0.10000000000000003,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":9,"id":15,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":7}],"nodes":[{"id":0,"label":{"isMath":true,"label":"Y","pos":[130,130],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"E(Z)","pos":[390,130],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[608,130],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[608,234],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,R_{i-1}^i Z)","pos":[390,234],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,X)","pos":[130,234],"zindex":-10000}}],"sizeGrid":260,"title":"1"}]},"version":12}
|
||||
@ -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":0,"id":8,"label":{"isPullshout":false,"label":"\\text{H3'}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":true,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":9,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":true,"head":"none","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":10,"label":{"isPullshout":false,"label":"\\inj_2^0","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":11,"label":{"isPullshout":false,"label":"\\text{H1r}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":true,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":12,"label":{"isPullshout":false,"label":"R_0^{i-1}\\left\\{g;\\eta_0^i \\circ L_0^{i-1} \\square \\right\\}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":13,"label":{"isPullshout":false,"label":"(\\varepsilon_0^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":14,"label":{"isPullshout":false,"label":"(R_0^{i-1} \\inj_2^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":6,"id":15,"label":{"isPullshout":false,"label":"R_0^{i-1}(\\eta_0^i \\circ L_0^{i-1} \\square)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":16,"label":{"isPullshout":false,"label":"\\square_\\UU \\circ \\Cstr^Z \\circ (g \\circ \\dash)","style":{"alignment":"right","bend":0.1,"color":"black","dashed":false,"double":false,"head":"default","position":0.20000000000000004,"tail":"none"},"zindex":0},"to":5},{"from":0,"id":17,"label":{"isPullshout":false,"label":"\\left\\{g;\\eta_0^i \\circ L_0^{i-1} \\square \\right\\} \\circ \\dash","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":18,"label":{"isPullshout":false,"label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":1,"id":19,"label":{"isPullshout":false,"label":"g \\circ \\dash","style":{"alignment":"left","bend":0,"color":"red","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":7}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X \\oplus L_0^{i-1}\\Hbar(X,Y))","pos":[210,70],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X)","pos":[334,198.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\Hbar(X,Y)_\\UU","pos":[426,70.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X \\oplus \\Hbar(X,Y)\\right]_\\UU","pos":[620.9999999999999,67.8125],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}\\left(X \\oplus L_0^{i-1}\\Hbar(X,Y)\\right)","pos":[901,67.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[901,347.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\left[R_0^{i-1}L_0^{i-1}\\Hbar(X,Y)\\right]_\\UU","pos":[704,204.625],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i Z)","pos":[210,350],"zindex":0}}],"sizeGrid":140,"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":0,"id":8,"label":{"kind":"normal","label":"\\text{H3'}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":9,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":10,"label":{"kind":"normal","label":"\\inj_2^0","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":11,"label":{"kind":"normal","label":"\\text{H1r}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":12,"label":{"kind":"normal","label":"R_0^{i-1}\\left\\{g;\\eta_0^i \\circ L_0^{i-1} \\square \\right\\}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":13,"label":{"kind":"normal","label":"(\\varepsilon_0^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":14,"label":{"kind":"normal","label":"(R_0^{i-1} \\inj_2^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":6,"id":15,"label":{"kind":"normal","label":"R_0^{i-1}(\\eta_0^i \\circ L_0^{i-1} \\square)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.7,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":16,"label":{"kind":"normal","label":"\\square_\\UU \\circ \\Cstr^Z \\circ (g \\circ \\dash)","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":5},{"from":0,"id":17,"label":{"kind":"normal","label":"\\left\\{g;\\eta_0^i \\circ L_0^{i-1} \\square \\right\\} \\circ \\dash","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":18,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":1,"id":19,"label":{"kind":"normal","label":"g \\circ \\dash","style":{"alignment":"left","bend":0,"color":"red","dashed":false,"head":"default","kind":"normal","position":0.4,"tail":"none"},"zindex":0},"to":7}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,X \\oplus L_0^{i-1}\\Hbar(X,Y))","pos":[210,64],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,X)","pos":[329,129.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\Hbar(X,Y)_\\UU","pos":[410,64.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X \\oplus \\Hbar(X,Y)\\right]_\\UU","pos":[604.9999999999999,61.8125],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}\\left(X \\oplus L_0^{i-1}\\Hbar(X,Y)\\right)","pos":[853,61.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[853,303.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\left[R_0^{i-1}L_0^{i-1}\\Hbar(X,Y)\\right]_\\UU","pos":[688,198.625],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,R_{i-1}^i Z)","pos":[210,306],"zindex":0}}],"sizeGrid":140,"title":"1"}]},"version":12}
|
||||
1
Report/graphs/G1-0.json
Normal file
1
Report/graphs/G1-0.json
Normal 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":3,"label":{"kind":"normal","label":"F","style":{"alignment":"right","bend":0.20000000000000004,"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":"G","style":{"alignment":"right","bend":0.20000000000000004,"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":"L","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":0,"id":6,"label":{"kind":"normal","label":"R","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":7,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":6,"id":8,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":5}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\BB","pos":[300,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\CC","pos":[500,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\TSet","pos":[300,300],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
@ -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":0,"id":7,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":true,"head":"none","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":8,"label":{"isPullshout":false,"label":"G_{i-1} \\times \\id","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":9,"label":{"isPullshout":false,"label":"F_{i-1} \\times \\id","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":2,"id":10,"label":{"isPullshout":false,"label":"W","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":11,"label":{"isPullshout":false,"label":"E","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":12,"label":{"isPullshout":false,"label":"G_i","style":{"alignment":"right","bend":0.5,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":13,"label":{"isPullshout":false,"label":"F_i","style":{"alignment":"right","bend":-0.30000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.6,"tail":"none"},"zindex":0},"to":0}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\left[S_i,\\Set\\right]","pos":[176,99.8125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\left(X : \\left[S_{i-1},\\Set\\right]\\right) \\times \\left.\\Set\\middle/\\Hom(\\Gamma_i,X)\\right.","pos":[500,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\left(X : \\BB_{i-1}\\right) \\times \\left.\\Set\\middle/\\Hom(G_{i-1}\\Gamma_i,X)\\right.","pos":[500,197.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\BB_i","pos":[500,300],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\dashv","pos":[499,150.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"\\dashv","pos":[500,251.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\top","pos":[284,260.8125],"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":0,"id":4,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":5,"label":{"kind":"normal","label":"G_{i-1} \\times \\id","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":6,"label":{"kind":"normal","label":"F_{i-1} \\times \\id","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":2,"id":7,"label":{"kind":"normal","label":"W","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":8,"label":{"kind":"normal","label":"E","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":9,"label":{"kind":"normal","label":"G_i","style":{"alignment":"right","bend":0.6,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":10,"label":{"kind":"normal","label":"F_i","style":{"alignment":"right","bend":-0.4,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":6,"id":11,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":8,"id":12,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":10,"id":13,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":9}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\CC_i","pos":[176,73.8125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\left(X : \\CC_{i-1}\\right) \\times \\left.\\Set\\middle/\\Hom(O_i,X)\\right.","pos":[386,74],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\left(X : \\BB_{i-1}\\right) \\times \\left.\\Set\\middle/\\Hom(G_{i-1}\\Gamma_i,X)\\right.","pos":[386,171.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\BB_i","pos":[386,274],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
@ -1,5 +1,4 @@
|
||||
% Loading packages
|
||||
\usepackage{autofe}
|
||||
% Loading packages
|
||||
\usepackage{hyperref}
|
||||
\usepackage{bookmark}
|
||||
\hypersetup{
|
||||
@ -103,13 +102,15 @@
|
||||
\newcommand\BB{{\ensuremath{\mathcal{B}}}}
|
||||
\newcommand\TT{{\ensuremath{\mathcal{T}}}}
|
||||
\newcommand\UU{{\ensuremath{\mathcal{U}}}}
|
||||
\newcommand\CC{{\ensuremath{\mathcal{C}}}}
|
||||
\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}}}}
|
||||
@ -117,6 +118,7 @@
|
||||
|
||||
\DeclareMathOperator{\inj}{inj}
|
||||
\DeclareMathOperator{\id}{id}
|
||||
\DeclareMathOperator{\Id}{\mathcal{I}d}
|
||||
|
||||
\newcommand\TSet{{\ensuremath{\left[\TT,\Set\right]}}}
|
||||
\newcommand\TSetObject[3]{{\ensuremath{
|
||||
@ -150,7 +152,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
6
Report/yade-config.json
Normal file
@ -0,0 +1,6 @@
|
||||
{
|
||||
"watchedFile": "M2Report.tex",
|
||||
"baseDir": "graphs",
|
||||
"externalOutput": true,
|
||||
"preambleFile": "yade-preamble.tex"
|
||||
}
|
||||
@ -2,6 +2,7 @@
|
||||
\newcommand\BB{{\ensuremath{\mathcal{B}}}}
|
||||
\newcommand\TT{{\ensuremath{\mathcal{T}}}}
|
||||
\newcommand\UU{{\ensuremath{\mathcal{U}}}}
|
||||
\newcommand\CC{{\ensuremath{\mathcal{C}}}}
|
||||
\newcommand\El{{\ensuremath{\operatorname{\mathcal{E}l}}}}
|
||||
\newcommand\ii{{\ensuremath{\mathbf{i}}}}
|
||||
\newcommand\Cstr{{\ensuremath{\operatorname{\mathcal{C}str}}}}
|
||||
|
||||
859
Report/yade.sty
859
Report/yade.sty
File diff suppressed because it is too large
Load Diff
Loading…
x
Reference in New Issue
Block a user