Changed introduction

Report/M2Report.tex

@@ -23,10 +23,10 @@
 	
 	\newpage
 
-	\section{Sort specification}
+	\section{Introduction}
 	
 	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.
+	A GAT typically 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.
 	
 	\paragraph{Sort specification}
@@ -46,9 +46,9 @@
 	
 	A model of this category is a triple
 	\begin{itemize}
-		\item A set $X_\Con : \Set$
+		\item A set $X_\Con$ of contexts
-		\item A family of sets $\left(X_\Ty\left(\Gamma\right)\right)_{\Gamma \in _\Con}$
+		\item A family of sets $\left(X_\Ty\left(\Gamma\right)\right)_{\Gamma \in _\Con}$ of types, indexed by contexts
-		\item A family of sets $\left(X_\Tm\left(\Delta,A\right)\right)_{\Delta\in X_\Con,\: A \in X_\Ty\left(\Delta\right)}$
+		\item A family of sets $\left(X_\Tm\left(\Delta,A\right)\right)_{\Delta\in X_\Con,\: A \in X_\Ty\left(\Delta\right)}$ of terms, indexed by contexts and types.
 	\end{itemize}
 	
 	\paragraph{Constructor specification}
@@ -58,87 +58,62 @@
 	\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{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$
+		$\operatorname{tt}: (\Gamma : \Con) \to \Tm\;\Gamma\;(\operatorname{unit}\;\Gamma)$ & In any context $\Gamma$, we have a term whose type is the $\operatorname{unit}$ of this context ($\operatorname{unit}\;\Gamma$).
-		
-		$\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)$
+		\item For each $\Gamma \in X_\Con$, an element $\operatorname{tt}\;\Gamma \in X_\Tm(\Gamma,\operatorname{unit}\;\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 used by Philippo Sestini in his thesis \cite{SestiniPhD} refering the work of Zongpu Szumi Xie \cite{AmbrusSzumiXie2sort}:
+	There is a process that allows us to transform a GAT into a GAT with only two sorts.
-		
+	The sort specification of the transformed GAT is always the same, and contains these two sort declarations:
-	\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}
-	
-	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}.
-	
-	We will now present this transformation. The sort specification of the transformed 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 \\
+		$\UU : \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.
+		$\El : \mathcal{O} \to \Set$ & For every sort object $o$ in the set of sorts, a set called $\El(o)$ of objects corresponding to the sort object. We will write this set $\underline{o}$ rather than $\El(o)$.
 	\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)$.
+	Then, we replace all occurrences of $\Set$ to $\mathcal{O}$, and we apply $\El$ to every parameter. For example, the Type Theory GAT presented above becomes that which follows:
-	
-	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$} \\
+		$\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$}\\
+		and for every object $A$ corresponding to the sort object $\Ty\;\Gamma$, another sort object called "$\Tm\;\Gamma\;A$"\\
-		$\operatorname{unit} : (\Gamma : \underline{\Con}) \to \underline{\Ty\;\Gamma}$ &
+		$\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$\\
+		For each object $\Gamma$ corresponding to the sort object $\Con$, an object called "$\operatorname{unit} \Gamma$" corresponding to the sort object $\Ty\;\Gamma$\\
-		$\operatorname{eq}: (\Gamma : \underline{\Con}) \to (A : \underline{\Ty\;\Gamma}) \to$ \newline
+		$\operatorname{tt}: (\Gamma : \underline{\Con}) \to \underline{\Tm\;(\operatorname{unit}\;\Gamma)}$ &
-		$\qquad\underline{\Tm\;\Gamma A} \to \underline{\Tm\;\Gamma A} \to \underline{\Ty\;\Gamma}$ &
 		$\dots$
 	\end{tabular}
 	
-	\paragraph{$\FamSet$ as functors}
+	This process has been observed by Zongpu Szumi Xie \cite{AmbrusSzumiXie2sort}, and Philippo Sestini used it in his thesis \cite{SestiniPhD}:
 	
-	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{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.
-	\begin{center}
+	\end{quote}
-		% YADE DIAGRAM G0.json
-		% GENERATED LATEX
-		\input{graphs/G0.tex}
-		% END OF GENERATED LATEX
-	\end{center}
-	
-	The functors over this categories are equivalent to families of sets, using the following mapping :
-	
-	\[
-	\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}
-	\]
-	
-	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.
 	
 	\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 goal my internship was to formally study this transformation, and to try to find a relation between the semantics of a GAT and its two-sorted version.
 	
-	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$.
+	We managed to construct a coreflection between a category of models and the category of models of the transformed GAT.
+	The existence of this coreflection is enough to prove what Sestini conjectured.
+	
+	We will give a formal definition of this coreflection in next section. It will consist of an adjunction $F \vdash G$ between the category $\CC$ of the models of the GAT and the category $\BB$ of the models of the two-sortified GAT, where G is full and faithful.
+	The category $\BB$ will be built with a forgetful functor $R$ to $\BB_0$, the category of models of the two-sort sort specification $(\mathcal{O},\El)$. This forgetful $R$ functor is a composition of monadic functors, one for each sort constructor.
 	
 	\begin{center}
 		% YADE DIAGRAM G1-0.json
@@ -147,29 +122,104 @@
 		% END OF GENERATED LATEX
 	\end{center}
 	
+	\section{Construction of the coreflection}
+	
+		\subsection{Preliminaries}
+		
+		\paragraph{Category of models of the two-sort sort specification}
+		
+		The usual way of defining the category of models of the two-sort specification $\BB_0$ is by taking the category of families of sets. However, in order to have more elegant constructions, we will use a the category of models of the two-sort specification the category $\TSet$ of presheaves over the category with one arrow.
+		
+		In the rest of the document, we will denote this category with one arrow as $\TT$. The objects and arrow of this category are pictured below.
+		
+		\begin{center}
+			% YADE DIAGRAM G0.json
+			% GENERATED LATEX
+			\input{graphs/G0.tex}
+			% END OF GENERATED LATEX
+		\end{center}
+		
+		With this formalisation, a model of the two-sort GAT is a functor $X : \TSet$, such that
+		\begin{itemize}
+			\item $X_\UU$ is the set of the \enquote{sort objects}
+			\item For each sort object $\Gamma \in X_\UU$, the set of objects corresponding to the sort object is $X_p^-1(\{\Gamma\}) \subset X_\El$
+		\end{itemize}
+		
+		Therefore the categories of models of the transformed GATs will be built atop of this category $\BB_0 = \TSet$.
+		
+		\paragraph{Grothendieck Construction} 
+		For a category $\mathcal{C}$ and a functor $F : \mathcal{C} \to \Cat$, the Grothendieck construction is a category whose objects are pairs of
+		\begin{itemize}
+			\item $X$ an object of $\mathcal{C}$
+			\item an object of $F(X)$
+		\end{itemize}
+		
+		The morphism $(X,Y) \to (X',Y')$ is therefore a pair of a morphism $f : X \to X'$ in $\mathcal{C}$ and a morphism $g : F(f)(Y) \to Y'$ in $H(X')$.
+		
+		We will denote this category $(X : \mathcal{C}) \times F(X)$ as its objects are pairs. It can some times be found written as $\int^\mathcal{C} F$ or $\sqint^\mathcal{C} F$
+		
+		\paragraph{Slice category}
+		For a category $\mathcal{C}$ and $X$ an object in that category, the slice category (or over category) $\mathcal{C}/A$ is a category whose objects are pairs of
+		\begin{itemize}
+			\item $Y$ an object of $\mathcal{C}$
+			\item an arrow $X \to Y$ of $\mathcal{C}$
+		\end{itemize}
+		
+		A morphism $(Y,f) \to (Y',f')$ is a morphism $g : Y \to Y'$ such that $g \circ f = f'$.
+		
+		We can deduce a functor $\left(\mathcal{C}/\dash\right) : \mathcal{C} \to \Cat$ from this construction.
+		
+		If the category $\mathcal{C}$ is $\Set$, we have that $\Set/X \cong \Set^X$.
+		
+		We will often concatenate the two method above to create from a category $\mathcal{C}$ and a functor $H : \mathcal{C} \to \Set$ a new category $(X : \mathcal{C}) \times \left(\Set\middle/H(X)\right)$.
+		
+		\paragraph{$\Hbar$ functor}
+		
+		Where $\Hbar_A$ is a functor $(X:C) \times (\Set/A(X)) \to \TSet$ defined as
+		\[
+		\Hbar_X(X,(Y,f)) = \TSetObject{Y}{f}{A(X)}
+		\]
+		The morphisms are translated as-is.
+		
+		\begin{remark}
+			This functor can be constructed using the property of the Grothendieck construction
+		\end{remark}
+		
 	\subsection{Constructing the categories}
 	
-		We will construct both categories $\CC$ and $\BB$ recursively, adding new sorts one by one.
+		We will construct both categories $\CC$ and $\BB$ recursively, adding new sorts one by one for each constructor. At each recursion step, we will build the categories, the adjunction, and keep some invariants that will be stated in \autoref{sec:hypotheses}.
-		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}.
+		
+		At the i-th recursion step, we will build the category $\CC_i$ which is the category of models of the $i$ first sorts of the sort specification. $\BB_i$ will samewise be the category of models of the 2-sorted $i$ first sorts of the sort specification.
 		
 		The overall recursive 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$.
 		
+		The functors $R_{i-1}^i$ are the forgetful monadic functors that forget about the $i$-th sort contsructor. They have a left adjoint denoted $L_{i-1}^i$.
+		As we can compose the adjunctions $R_0^1$,$R_1^2$,...,$R_{i-1}^i$, we will use the two following adjunctions
+		\[\begin{array}{c}
+			R_0^i = R_{0}^{i-1} \circ R_{i-1}^{i} = R_{0}^{1} \circ ... \circ R_{i-1}^{i}\\
+			L_0^i = L_{i-1}^{i} \circ L_{0}^{i-1} = L_{i-1}^{i} \circ ... \circ L_{0}^{1}
+		\end{array}\]
+		
+		\begin{remark}
+			There is also an adjunction chain between $\CC_0$,$\dots$,$\CC_{i-1}$,$\CC_i$, but we don't use it in the proof.
+		\end{remark}
+		
 		\subsubsection{Constructing $\CC_i$}
 		
 		We construct the category $\CC_i$ as the following pair:
 		\[
 			\CC_i = (X : \CC_{i-1}) \times \left(\Set\middle/\Hom(O_i,X)\right)
 		\]
-		where for any category $\mathcal{C}$ and $X$ an object of $\mathcal{C}$, $(\mathcal{C}/X)$ it the slice category (or over category) of arrows pointing out of $X$ (its objects $(Y,f)$ are arrows $f : X \to Y$ and its morphisms are morphisms creating commutative triangles).\inlinetodo{Assez clair ?} \inlinetodo{On ne voit pas que $(\Set/A(X)) \cong \Set^{A(X)}$}
-		
 		and 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.
-		\todo{Comment indiquer que la paire est dépendante ?}
 		
 		I will give now an example of those $O_i$ objects for our type theory example. We begin with
 		\[
@@ -216,13 +266,7 @@
 		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$.
+		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 adjoint} 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$.
 		
@@ -234,17 +278,19 @@
 		\end{remark}
 	
 	
-	\subsection{Some Hypotheses}
+	\subsection{Induction Hypotheses}
 	
 		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]
+			
+			The canonical morphism
 			\[
 			\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 isomorphism.
+			that we will denote as $\en_{i-1}^i$ is an isomorphism.
 			
-			Its recursive version is the following isomorphism
+			Its recursive version is the following isomorphism, denoted as $\en_0^i$
 			\[
 			\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)}
 			\]
@@ -291,16 +337,6 @@
 		W(X,Y) := \left(X \oplus L_0^{i-1} \Hbar_{\Hom(G_{i-1}O_i,\dash)}(X,Y), \widetilde{\inj_2} \right)
 		\]
 		
-		Where $\Hbar_A$ is a functor $(X:C) \times (\Set/A(X)) \to \TSet$ defined as
-		\[
-		\Hbar_X(X,(Y,f)) = \TSetObject{Y}{f}{A(X)}
-		\]
-		The morphisms are translated as-is.
-		
-		\begin{remark}
-			This functor can be constructed as a lax colimit seeing elements of $A(X)/\Set$ as lax cocones over the diagram $\left[1 \xrightarrow{A(X)} \Set\right]$ in $\Cat$, and seeing elements of $\TSet$ as lax cocones over the diagram with no arrow $\left[\Set \quad \Set\right]$. \inlinetodo{Vérifier ça}
-		\end{remark}
-		
 		With $\widetilde{\inj_2}$ being defined by \inlinetodo{Changer les noms des hypothèses H3' et H1r}
 		\[
 		\begin{array}{lcl}
@@ -351,7 +387,6 @@
 			% END OF GENERATED LATEX
 		\end{center}
 		 
-		 
 	\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.
@@ -456,7 +491,7 @@
 		
 		Where $\varepsilon_i$ is the counit of the adjunction $R_{i-1}^i \vdash L_{i-1}^i$, going from $L_{i-1}^i R_{i-1}^i X$ to $X$.
 		
-		This goes from $L_0^i Y = L_{i-1}^i L_0^{i-1} Y$ to $L_{i-1}^i(R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y)$, which is equivalent to $L_{i-1}^i R_{i-1}^i X \oplus_i L_0^i Y)$ as $L_{i-1}^i$ is a left-adjunct functor and therefore it preserves colimits; then goes to $X \oplus_i L_0^i Y$.
+		This goes from $L_0^i Y = L_{i-1}^i L_0^{i-1} Y$ to $L_{i-1}^i(R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y)$, which is equivalent to $L_{i-1}^i R_{i-1}^i X \oplus_i L_0^i Y)$ as $L_{i-1}^i$ is a left-adjoint functor and therefore it preserves colimits; then goes to $X \oplus_i L_0^i Y$.
 		
 		We will now show that this definition is actually a definition of the coproduct in $\BB_i$.
 		To that extent, we take two objects $X$ and $Z$ in $\BB_i$, $Y$ in $\TSet$ and two morphisms of $\BB_i$ $\varphi_1 : X \to Z$ and $\varphi_2 : L_0^i Y \to Z$.
@@ -754,6 +789,15 @@
 
 
 
+
+
+
+
+
+
+
+
+
 
 
 

Report/graphs/B1.json

@@ -1 +1 @@
-{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":1,"id":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}
+{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":1,"id":4,"label":{"kind":"normal","label":"\\Gamma","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":2,"id":5,"label":{"kind":"normal","label":"A","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":2,"id":6,"label":{"kind":"normal","label":"\\Delta","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Con","pos":[100,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Ty","pos":[300,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\Tm","pos":[500,100],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\circlearrowleft","pos":[302,76.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}

Report/graphs/D10.0.json

@@ -1 +1 @@
-{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"isPullshout":false,"label":"\\phi_{XYZ}","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":"E(f) \\circ \\dash \\circ (g,h)","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 \\circ W(g,h)","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":"\\phi_{X'Y'Z'}","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(W(X,Y),Z)","pos":[300,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Hom((X,Y),E(Z))","pos":[700,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\Hom((X',Y'),E(Z'))","pos":[700,300],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(W(X',Y'),Z')","pos":[300,300],"zindex":-10000}}],"sizeGrid":200,"title":"1"}]},"version":11}
+{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"\\phi_{XYZ}","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":"E(f) \\circ \\dash \\circ (g,h)","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 \\circ W(g,h)","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":"\\phi_{X'Y'Z'}","style":{"alignment":"left","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(W(X,Y),Z)","pos":[300,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Hom((X,Y),E(Z))","pos":[700,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\Hom((X',Y'),E(Z'))","pos":[700,300],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(W(X',Y'),Z')","pos":[300,300],"zindex":-10000}}],"sizeGrid":200,"title":"1"}]},"version":12}

Report/graphs/D10.json

@@ -1 +1 @@
-{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":10,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":11,"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":12,"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":13,"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":14,"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":15,"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":16,"label":{"isPullshout":false,"label":"(\\inj_1^{i-1} \\circ \\dash)","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":17,"label":{"isPullshout":false,"label":"R_{i-1}^i f","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":18,"label":{"isPullshout":false,"label":"\\square_\\El = \\left[R_{i-1}^i f \\circ \\inj_2^{i-1}\\right]","style":{"alignment":"left","bend":-0.1,"color":"blue","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":5,"id":19,"label":{"isPullshout":false,"label":"\\square_\\UU","style":{"alignment":"right","bend":0.2,"color":"blue","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":5,"id":20,"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":7},{"from":7,"id":21,"label":{"isPullshout":false,"label":"(\\inj_2^0)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":8,"id":22,"label":{"isPullshout":false,"label":"\\text{H1'}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":true,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":9,"id":23,"label":{"isPullshout":false,"label":"(R_0^i f)_\\UU","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":6,"id":24,"label":{"isPullshout":false,"label":"\\Cstr^{W(X,Y)}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":13,"id":25,"label":{"isPullshout":true,"label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"double":false,"head":"","position":0,"tail":""},"zindex":0},"to":11}],"nodes":[{"id":0,"label":{"isMath":true,"label":"Y","pos":[80,80],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"E(Z)","pos":[692,79.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[880,80],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[880,240],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i Z)","pos":[692,239.8125],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X)","pos":[80,240],"zindex":-10000}},{"id":6,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X \\oplus L_0^{i-1} \\Hbar Y)","pos":[400,240],"zindex":-10000}},{"id":7,"label":{"isMath":true,"label":"(\\Hbar Y)_\\UU","pos":[80,400],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X \\oplus (\\Hbar Y)\\right]_\\UU","pos":[400,400],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"\\left[R_0^i(W(X,Y))\\right]_\\UU","pos":[720,400],"zindex":0}}],"sizeGrid":160,"title":"1"}]},"version":11}
+{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":10,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":11,"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":12,"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":13,"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":14,"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":15,"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":16,"label":{"kind":"normal","label":"(\\inj_1^{i-1} \\circ \\dash)","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":17,"label":{"kind":"normal","label":"R_{i-1}^i f","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":18,"label":{"kind":"normal","label":"\\square_\\El = \\left[R_{i-1}^i f \\circ \\inj_2^{i-1}\\right]","style":{"alignment":"left","bend":-0.1,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":5,"id":19,"label":{"kind":"normal","label":"\\square_\\UU","style":{"alignment":"right","bend":0.2,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":5,"id":20,"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":7},{"from":7,"id":21,"label":{"kind":"normal","label":"(\\inj_2^0)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":8,"id":22,"label":{"kind":"normal","label":"\\text{H1'}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":9,"id":23,"label":{"kind":"normal","label":"(R_0^i f)_\\UU","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":6,"id":24,"label":{"kind":"normal","label":"\\Cstr^{W(X,Y)}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":13,"id":25,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":11}],"nodes":[{"id":0,"label":{"isMath":true,"label":"Y","pos":[80,80],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"E(Z)","pos":[692,79.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[880,80],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[880,240],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i Z)","pos":[692,239.8125],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X)","pos":[80,240],"zindex":-10000}},{"id":6,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X \\oplus L_0^{i-1} \\Hbar Y)","pos":[400,240],"zindex":-10000}},{"id":7,"label":{"isMath":true,"label":"(\\Hbar Y)_\\UU","pos":[80,400],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X \\oplus (\\Hbar Y)\\right]_\\UU","pos":[400,400],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"\\left[R_0^i(W(X,Y))\\right]_\\UU","pos":[720,400],"zindex":0}}],"sizeGrid":160,"title":"1"}]},"version":12}

Report/graphs/D4.json

@@ -1 +1 @@
-{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"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":7,"label":{"isPullshout":false,"label":"(R_0^{i-1} (\\inj_1^{i-1})_\\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":8,"label":{"isPullshout":false,"label":"\\inj_1^{i-1} \\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":4,"id":9,"label":{"isPullshout":false,"label":"R_0^{i-1}(\\inj_1^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":10,"label":{"isPullshout":false,"label":"(\\inj_1^{i-1} \\circ \\dash)^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.20000000000000004,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":11,"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":4},{"from":0,"id":12,"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":5},{"from":4,"id":13,"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":3,"id":14,"label":{"isPullshout":false,"label":"\\Cstr^{X \\oplus L_0^i Y}","style":{"alignment":"left","bend":0.1,"color":"green","dashed":true,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X)","pos":[220.5,73.5],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[951,73.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\oplus L_0^{i-1} Y))_\\UU","pos":[955.5,367.5],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X \\oplus_{i-1} L_0^{i-1} Y)","pos":[220.5,367.5],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[718,301.8125],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X)","pos":[448,300.8125],"zindex":-10000}}],"sizeGrid":147,"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":6,"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":7,"label":{"kind":"normal","label":"(R_0^{i-1} (\\inj_1^{i-1})_\\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":8,"label":{"kind":"normal","label":"\\inj_1^{i-1} \\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":4,"id":9,"label":{"kind":"normal","label":"R_0^{i-1}(\\inj_1^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":10,"label":{"kind":"normal","label":"(\\inj_1^{i-1} \\circ \\dash)^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.20000000000000004,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":11,"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":4},{"from":0,"id":12,"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":5},{"from":4,"id":13,"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":3,"id":14,"label":{"kind":"normal","label":"\\Cstr^{X \\oplus L_0^i Y}","style":{"alignment":"left","bend":0.1,"color":"green","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X)","pos":[220.5,73.5],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[951,73.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\oplus L_0^{i-1} Y))_\\UU","pos":[955.5,367.5],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X \\oplus_{i-1} L_0^{i-1} Y)","pos":[220.5,367.5],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[718,301.8125],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X)","pos":[448,300.8125],"zindex":-10000}}],"sizeGrid":147,"title":"1"}]},"version":12}

Report/graphs/D5.json

@@ -1 +1 @@
-{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"isPullshout":false,"label":"(\\inj_1 \\circ \\dash)","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":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},{"from":0,"id":8,"label":{"isPullshout":false,"label":"\\{\\varphi_1 ; \\varphi_2\\} \\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":2,"id":9,"label":{"isPullshout":false,"label":"(R_0^{i-1} \\inj_1^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"twoheads","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":10,"label":{"isPullshout":false,"label":"(R_0^i \\{\\varphi_1;\\varphi_2\\})_\\UU","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":11,"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":12,"label":{"isPullshout":false,"label":"R_{i-1}^i \\varphi_1 \\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":2,"id":13,"label":{"isPullshout":false,"label":"(R_0^i \\varphi_1)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X \\oplus L_0^{i-1} Y)","pos":[225,75],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X)","pos":[525,75],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[681,241.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i Z)","pos":[225,375],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\oplus L_0^{i-1} Y))_\\UU","pos":[825,75],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[825,375],"zindex":0}}],"sizeGrid":150,"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":6,"label":{"kind":"normal","label":"(\\inj_1 \\circ \\dash)","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"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":2},{"from":0,"id":8,"label":{"kind":"normal","label":"\\{\\varphi_1 ; \\varphi_2\\} \\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":2,"id":9,"label":{"kind":"normal","label":"(R_0^{i-1} \\inj_1^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"twoheads","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":10,"label":{"kind":"normal","label":"(R_0^i \\{\\varphi_1;\\varphi_2\\})_\\UU","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":11,"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":12,"label":{"kind":"normal","label":"R_{i-1}^i \\varphi_1 \\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":2,"id":13,"label":{"kind":"normal","label":"(R_0^i \\varphi_1)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X \\oplus L_0^{i-1} Y)","pos":[225,75],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X)","pos":[525,75],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[681,241.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i Z)","pos":[225,375],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\oplus L_0^{i-1} Y))_\\UU","pos":[825,75],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[825,375],"zindex":0}}],"sizeGrid":150,"title":"1"}]},"version":12}

Report/graphs/D9.json

@@ -1 +1 @@
-{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":1,"id":6,"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":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":3},{"from":1,"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":4},{"from":4,"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":3},{"from":0,"id":10,"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":11,"label":{"isPullshout":false,"label":"\\dash \\circ g","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":12,"label":{"isPullshout":false,"label":"(\\left\\{g;\\eta_0^i \\circ L_0^{i-1} \\square \\right\\} \\circ \\inj_2)_\\El","style":{"alignment":"left","bend":-0.30000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":13,"label":{"isPullshout":false,"label":"h","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":0,"id":14,"label":{"isPullshout":false,"label":"\\phi_{XYZ}(\\phi^{-1}_{XYZ}(g,h))_2","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.7,"tail":"none"},"zindex":0},"to":1},{"from":8,"id":15,"label":{"isPullshout":true,"label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"double":false,"head":"","position":0,"tail":""},"zindex":0},"to":6}],"nodes":[{"id":0,"label":{"isMath":true,"label":"Y","pos":[300,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"E(Z)","pos":[500,300],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[700,300],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[700,500],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i Z)","pos":[500,500],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X)","pos":[300,300],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":11}
+{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":1,"id":6,"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":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":3},{"from":1,"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":4},{"from":4,"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":3},{"from":0,"id":10,"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":11,"label":{"kind":"normal","label":"\\dash \\circ g","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":12,"label":{"kind":"normal","label":"(\\left\\{g;\\eta_0^i \\circ L_0^{i-1} \\square \\right\\} \\circ \\inj_2)_\\El","style":{"alignment":"left","bend":-0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":13,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":0,"id":14,"label":{"kind":"normal","label":"\\phi_{XYZ}(\\phi^{-1}_{XYZ}(g,h))_2","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.7,"tail":"none"},"zindex":0},"to":1},{"from":8,"id":15,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":6}],"nodes":[{"id":0,"label":{"isMath":true,"label":"Y","pos":[300,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"E(Z)","pos":[500,300],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[700,300],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[700,500],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i Z)","pos":[500,500],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X)","pos":[300,300],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}

Report/graphs/G0.json

@@ -1 +1 @@
-{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":1,"id":2,"label":{"isPullshout":false,"label":"p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":0}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\UU","pos":[100,300],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\El","pos":[100,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":2,"label":{"kind":"normal","label":"p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\UU","pos":[100,178],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\El","pos":[100,100],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}

Report/graphs/G1-0.json

@@ -1 +1 @@
-{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":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}
+{"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":[486,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\BB_0","pos":[300,174],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}

Report/header.tex

@@ -1,4 +1,10 @@
 % Loading packages
+\usepackage[utf8]{inputenc}
+\usepackage{ae}
+\usepackage[T1]{fontenc}
+\usepackage{fontspec}
+\usepackage{alphabeta}
+\usepackage{polyglossia}
 \usepackage{hyperref}
 \usepackage{bookmark}
 \hypersetup{
@@ -11,7 +17,6 @@
 \usepackage{amssymb}
 \usepackage{bbm}
 \usepackage{stmaryrd}
-\usepackage[main=english]{babel}
 \usepackage{csquotes}
 \usepackage{listings}
 \usepackage{lstautogobble}
@@ -38,6 +43,7 @@
 \usepackage{pdfpages}
 \usepackage{lipsum}
 \usepackage{newunicodechar}
+\usepackage{txfonts}
 \usepackage{yade}
 
 \usepackage[textheight=0.75\paperheight]{geometry}
@@ -98,8 +104,9 @@
 
 
 % Macros caractères spécifiques au document
-\newunicodechar{λ}{{\lambda}}
+\newfontface\russian{Liberation Serif}
 \newcommand\BB{{\ensuremath{\mathcal{B}}}}
+\newcommand\en{{\text{\russian н}}}
 \newcommand\TT{{\ensuremath{\mathcal{T}}}}
 \newcommand\UU{{\ensuremath{\mathcal{U}}}}
 \newcommand\CC{{\ensuremath{\mathcal{C}}}}