From 5363b3d76e0cfc88af8d7a2210b0a285df214fae Mon Sep 17 00:00:00 2001 From: Samy Avrillon Date: Mon, 19 Aug 2024 15:21:21 +0200 Subject: [PATCH] Modifications d'Ambroise --- Report/M2Report.tex | 188 +++++++++++++++++---------------- Report/graphs/TlUniversal.json | 2 +- Report/header.tex | 2 + 3 files changed, 101 insertions(+), 91 deletions(-) diff --git a/Report/M2Report.tex b/Report/M2Report.tex index dfff323..f830996 100644 --- a/Report/M2Report.tex +++ b/Report/M2Report.tex @@ -21,29 +21,30 @@ \begin{document} \doparttoc + \setlength\droptitle{-1.5cm} \maketitle - + \vspace{-1cm} \hsep \subsection*{General Context} Generalized Algebraic Theories a.k.a. GATs are syntactic objects introduced in 1986 by Cartmell \cite{CartmellGATs}. They enable us to describe algebraic structures that we can see as a generalization of Type Theory's inductive types. For example, we can describe the models of some type theory using a GAT. - A GAT is made of a list of \enquote{sorts} that describes sets, usually followed by a list of \enquote{constructors}. + A GAT is made of a list of \enquote{sorts} called a \enquote{sort specification} that describes sets, usually followed by a list of \enquote{constructors}. \subsection*{Problem Studied} - There is a process that transforms any GAT into another GAT with only two sorts. This transformation has been used by Filippo Sestini in their PhD, in order to make simpler proofs the scope of their study. However it has not been proven that using this transformation does not reduce the generality of their thesis. + There is a process that transforms any GAT into another GAT with only two sorts. This transformation has been used by Filippo Sestini in their PhD, in order to restrict their study to GATs with only two sorts. However, this systematic transformation has not yet been formally justified. \subsection*{Proposed Contribution} - During this internship, my goal was to semantically formalize this transformation. I looked directly at the categories of models without looking at the syntactic aspects of GATs. I only looked at \enquote{sort specification}, i.e. GATs that are juste a list of sort declarations with no constructors. I started with applying the transformation on simple examples in order to identify properties that would prove the transformation to be correct. I did that in a categorical framework. Then, i formally stated those properties and proved them as generically as possible. + During this internship, my goal was to semantically formalize this transformation. I focused directly on the categories of models without looking at the syntactic aspects of GATs. I only focused on \enquote{sort specification}, i.e. GATs that are just a list of sort declarations with no constructors. I started with applying the transformation on simple examples in order to identify properties that would prove the transformation to be correct, working in a categorical framework. Then, I formally stated those properties and proved them as generically as possible. \subsection*{Arguments Supporting Their Validity} The overall proof was made semantically and at each step, we tried to generalize objects as much as possible. The ways of constructing the objects is based on published papers \cite{Altenkirch2018} \cite{Fiore2008}. - My contribution also proves the conjecture stated in Sestini's PhD. + My contribution is also a first step towards solving the conjecture stated in Sestini's PhD. \subsection*{Summary and Future Work} @@ -52,9 +53,11 @@ A next step could be to add term constructors to our formalization. We could describe their transformation and adapt the properties we stated for sort specification to them. - We could also try to further generalize GATs using this transformation. We could for example try to describe sorts that are mutually included one into the other. There is work in studying them, and looking at how the transformation affects them in order to discover new properties. + We could also try to further generalize GATs using this transformation. We could for example try to describe sorts that are mutually included one into the other. More work needs to be done studying them and looking at how the transformation affects them in order to discover new properties. - \hsep + We could also aim to encode this transformation and the associated proofs in a proof assistant like Agda or Coq. + + \newpage \setcounter{tocdepth}{2} \tableofcontents @@ -135,7 +138,7 @@ \paragraph{Goal} - The goal of my internship was to study and understand the relationship between the categories of models of an original GAT and the category of models of the transformed \enquote{two-sortified} GAT, in order to legitimate this transformation. In this document, we will only study sort specifications (i.e. lists of sort declaration, with no constructors). + The goal of my internship was to study and understand the relationship between the categories of models of an original GAT and the category of models of the transformed \enquote{two-sortified} GAT, in order to legitimate this transformation. In this document, we will only study sort specifications (i.e. lists of sort declarations, with no constructors). We constructed a coreflection between those two categories, whose formal definition is given in \autoref{sec:proofSection}. It consists 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. This coreflection justifies the transformation as the initial object of $\CC$ can be computed as the image by $F$ of the initial object of $\BB$. @@ -178,7 +181,7 @@ \paragraph{Category of models of the empty sort specification} - The category of models of the empty sort specification will simply be $\one$, the category with only one object $\star$ and one trivial morphism (i.e. the terminal category of $\Cat$). This is because the empty sort specification only has one model. We will denote this category as $\CC_0$. + The category of models of the empty sort specification will simply be $\one$, the category with only one object $\star$ and one trivial (identity) morphism (i.e. the terminal category of $\Cat$). This is because the empty sort specification has only one model. We will denote this category as $\CC_0$. \paragraph{Category of models of the transformed GAT} @@ -204,6 +207,8 @@ % END OF GENERATED LATEX \end{center} + So an object of $\TSet$ is composed of two sets $X_\UU$ and $X_\El$ and an arrow $X_p : X_\El \to X_\UU$. Morphisms are natural transformations $f : X \to X'$ i.e. two functions $f_\UU : X_\UU \to X'_\UU$ and $f_\El : X_\El \to X'_\El$ that commutes with $X_p$ and $X'_p$. + This category is equivalent to the category $\FamSet$ with an equivalence we will see later (\autoref{SetXSetXEquivalence}) With this formalisation, a model of this sort specification is a functor $X : \TT \to \Set$, such that @@ -231,7 +236,7 @@ We can check that those two functors create an adjunction, as \[ - \Hom(G_0 \star,X) = \Hom(0_\TSet,X) \cong \one \cong \Hom(\star,F_0 X) + \Hom(G_0 \star,X) = \Hom(0_\TSet,X) \cong 1_\Set \cong \Hom(\star,F_0 X) \] We also have that they create a coreflection, as $F_0G_0$ goes from $\one$ to $\one$, and so $F_0G_0 = \Id_\one$ as $\one$ is terminal in $\Cat$. So $F_0G_0$ is an isofunctor. @@ -284,7 +289,7 @@ H_\Con(\star) = 1 \in \Set \] - This functor means that $\Con$ takes no parameter i.e. there is only \emph{one} way of constructing a $\Con$. + This functor means that $\Con$ takes no parameter (or one parameter of type \texttt{unit}) i.e. there is only \emph{one} way of constructing a $\Con$. We build $\CC_1$ to be a pair of \begin{itemize} @@ -370,9 +375,9 @@ Now the constructor we are adding takes one parameter. It means that for every element of $\El$ associated with $\Con$, there is an object in $\mathcal{O}$. - This constructor translates into an object + This constructor means that a model $X$ comes with a function as follows: \[ - \Cstr^X_\Ty : X_p^{-1}(\Cstr^X_\Con) \to X_\UU + \Cstr^X_\Ty : X_p^{-1}\left(\{\Cstr^X_\Con\}\right) \to X_\UU \] The codomain of this constructor means \enquote{Every object of $X_\El$ that are associated to the $\Con$ object of $X_\UU$ i.e. the object $\Cstr^X_\Con$} @@ -431,7 +436,7 @@ \item $X_p$ sends an object of a sort to the sort it corresponds to \end{itemize} - Therefore, we will construct $X_\UU$ to be the disjoint union of all the indices of the sets inside $Y$, $X_\El$ will be the disjoint union of all the sets inside $Y$, and $X_p$ will keep track of what is the index of a set. + Therefore, we will construct $X_\UU$ to be the disjoint union (denoted $\oplus$) of all the indices of the sets inside $Y$, $X_\El$ will be the disjoint union of all the sets inside $Y$, and $X_p$ will keep track of what is the index of a set. \[\begin{array}{ccccccc} @@ -455,7 +460,7 @@ \Cstr^X_\Tm(\Delta,A) &=& \inj_3(\Delta,A) \end{array}\] - where $\inj_i$ is the $i$-th injector of the direct sum $\oplus$. + where $\inj_i$ is the $i$-th injector of the disjoint union $\oplus$. \begin{remark} With this functor, every element of $X_\UU$ is reached by some constructor. And therefore, every object of $X_\El$ points to a sort that is reached by some constructor. @@ -488,12 +493,12 @@ \begin{remark} We can see that the $F_3$ functor does not take into account elements of $X_\UU$ that are not \enquote{created} by one of the constructors, nor does it take into account the elements of $X_\El$ that are associated with those elements of $X_\UU$. - This will later justify that when one adds elements to the base object $X$ of a model of $\BB_i$, then the image model by $F_i$ is unchanged, i.e. $F_i \inj_\tl^i$ is an isomorphism. + This will later justify that when one adds elements to the base object $X$ of a model of $\BB_i$, then the image model by $F_i$ is unchanged, which we will later express by \enquote{$F_i \inj_\tl^i$ is an isomorphism} in \hyperref[sec:proofSection]{the global proof}. \end{remark} \paragraph{An adjunction} - I will not do the proof that $F_3 \vdash G_3$, but i will give moral reasons of why the adjunction holds. + I will not do the proof that $F_3 \vdash G_3$ in this specific case, as it will be proven in the general case in the global proof, but i will give intuitions of why the adjunction holds. An adjunction would be described by the following isomorphism: \[ @@ -545,7 +550,7 @@ \[ R_0^i := R^1_0 \circ \dots \circ R_{i-1}^i \] - \item An operator $\tl^i : \BB_i \times \BB_0 \to \BB_i$ along with two morphism $\inj_1^i : X \to X \tl^i Y$ and $\inj_2^i : Y \to R_0^i(X \tl^i Y)$ for every $X,Y$ in $\BB_i \times \BB_0$, such that the canonical morphism $\en_{i-1}^i : (R_{i-1}^i X) \tl^{i-1} Y \to R_{i-1}^i (X \tl^i Y)$ is an isomorphism. This operation follows a specific universal property: For every morphisms $g : X \to Z$ and $h : Y \to R_0^iZ$, there is an unique morphism $\{g;h\}$ such that the following diagrams commute: + \item An operator $\tl^i : \BB_i \times \BB_0 \to \BB_i$ along with two morphism $\inj_1^i : X \to X \tl^i Y$ and $\inj_2^i : Y \to R_0^i(X \tl^i Y)$ for every $X,Y$ in $\BB_i \times \BB_0$. This operation follows a specific universal property: For every morphisms $g : X \to Z$ and $h : Y \to R_0^iZ$, there is an unique morphism $\{g;h\}$ such that the following two diagrams of $\BB_i$ and of $\BB_0$ commute: \label{sec:tlUniversalProperty} \begin{center} @@ -555,16 +560,17 @@ % END OF GENERATED LATEX \end{center} - We will also denote a composition morphism as such: - \[\en_0^i := R_0^{i-1} \en_{i-1}^i \circ \dots \circ R_0^1\en_1^2 \circ \en_0^1 : (R_0^i X) \oplus Y = (R_0^i X) \tl^0 Y \to R_0^i (X \tl^i Y)\] - - The operator is also defined on morphisms, such that for any morphism $g : X \to X'$ in $\BB_i$ and $h : Y \to Y'$ in $\BB_0$, there is a morphism $g \tl^i h : X \tl^i Y \to X' \tl^i Y'$ in $\BB_i$. + The operator can be extended to act on morphisms by exploiting the universal property, so that for any morphism $g : X \to X'$ in $\BB_i$ and $h : Y \to Y'$ in $\BB_0$, there is a morphism $g \tl^i h : X \tl^i Y \to X' \tl^i Y'$ in $\BB_i$. \item A functor $F_i : \BB_i \to \CC_i$ \item A functor $G_i : \CC_i \to \BB_i$ \item An adjunction between them $F_i \vdash G_i$ \item A proof that $F_iG_i \cong \Id_{\CC_i}$ (i.e. $F_i \vdash G_i$ make up a coreflection) \item A proof that $F_i\inj_1^i$ is an isomorphism. The inverse isomorphism will be denoted as $(F_i\inj_1^i)^{-1}$ + \item A proof that the canonical morphism $\en_{i-1}^i : (R_{i-1}^i X) \tl^{i-1} Y \to R_{i-1}^i (X \tl^i Y)$ is an isomorphism. + + We will denote the composition of those $\en$ morphism as such: + \[\en_0^i := R_0^{i-1} \en_{i-1}^i \circ \dots \circ R_0^1\en_1^2 \circ \en_0^1 : (R_0^i X) \tl^0 Y \to R_0^i (X \tl^i Y)\] \end{itemize} Here is a figure that describes the recursive construction of some of the above objects @@ -605,7 +611,7 @@ \label{SetXSetXEquivalence} When the category $\mathcal{C}$ is $\Set$, we have the equivalence - \[\Set/X \cong \Set^X\] + \[\Set/X \simeq \Set^X\] This equivalence is described by the following correspondence of objects. An object $(Y,f)$ of $\Set/X$ is transformed into the family of sets $A : X \to \Set$ defined by @@ -766,12 +772,12 @@ % END OF GENERATED LATEX \end{center} - The action on a morphism $(g,h)$ from $(X,Y)$ to $(X',Y')$ is the following: + The action on a morphism $(g,h)$ from $(X,Y)$ to $(X',Y')$ is defined such as: \[ - W(g,h) := \left(g \tl^{i-1} K_{H_iF_{i-1}}(g,h)\right) + R_{i-1}^i W(g,h) := \left(g \tl^{i-1} K_{H_iF_{i-1}}(g,h)\right) \] - We verify that it is indeed a morphism of $\BB_{i}$ in appendix \ref{apx:wdefsound} + We verify in appendix \ref{apx:wdefsound} that this morphism verifies the property of morphisms of $\BB_i$, so that it is indeed a morphism of $\BB_{i}$. \subsubsection{E definition} @@ -846,9 +852,9 @@ % END OF GENERATED LATEX \end{center} - The first injector $\inj_1^i : X \to X \tl^i Y$ is defined as follows: + The first injector $\inj_1^i : X \to X \tl^i Y$ is defined such that: \[ - \inj_1^i := \inj_1^{i-1} : R_{i-1}^i X \to R_{i-1}^i (X \tl^i Y) = R_{i-1}^i X \tl^{i-1} Y + R_{i-1}^i \inj_1^i := \inj_1^{i-1} : R_{i-1}^i X \to R_{i-1}^i (X \tl^i Y) = R_{i-1}^i X \tl^{i-1} Y \] We check that $\inj_1^i$ is a morphism of $\BB_i$ in appendix \ref{apx:inj1morphism}. @@ -860,7 +866,7 @@ \paragraph{Universal Property} We will now show that that the universal property stated in \autoref{sec:tlUniversalProperty} holds. - To that end, we take two objects $X$ and $Z$ in $\BB_i$, $Y$ in $\BB_0$, a morphism $g : X \to Z$ in $\BB_i$ and a morphism $h : Y \to R_0^iZ$ in $\BB_0$. We want to build a morphism $\{g,h\}$ of $\BB_i$ such that the following diagram commute. + To that end, we take two objects $X$ and $Z$ in $\BB_i$, $Y$ in $\BB_0$, a morphism $g : X \to Z$ in $\BB_i$ and a morphism $h : Y \to R_0^iZ$ in $\BB_0$. We want to build a morphism $\{g,h\}$ of $\BB_i$ such that the following diagrams of $\BB_i$ and $\BB_0$ commute. \begin{center} % YADE DIAGRAM TlUniversal.json @@ -869,9 +875,9 @@ % END OF GENERATED LATEX \end{center} - We define $\{g ; h\}_i = \{R_{i-1}^i g ; h\}_{i-1}$. We check that this is a morphism of $\BB_i$ in appendix \ref{apx:universalpropertymorphismIsMorphism}. + We check that $\{R_{i-1}^i g ; h\}_{i-1}$ verifies the property of morphisms of $\BB_i$ in appendix \ref{apx:universalpropertymorphismIsMorphism}. Therefore, we can define $\{g ; h\}_i$ such that $R_{i-1}^i\{g ; h\}_i = \{R_{i-1}^i g ; h\}_{i-1}$. - And this morphism $\{g;h\}_i$ is such that the universal property for it is exactly the same as the one of $\{R_{i-1}^i g, h\}$. + This morphism $\{g;h\}_i$ is such that the universal property for it is exactly the same as the one of $\{R_{i-1}^i g, h\}$. With this definition, the isomorphism $\en_{i-1}^i : (R_{i-1}^i X) \tl^{i-1} Y \to R_{i-1}^i(X \tl^i Y)$ is simply the identity morphism. @@ -909,13 +915,13 @@ \section{Other Properties} - \subsection{Fibration of the category $\CC_i$} + \subsection{Sort specifications as simple direct categories} In the formal proof, we defined $\CC_i$ as an inductive Grothendieck construction as in Altenkirch and al. papers \cite{Altenkirch2018}. But there is an other way \cite{Fiore2008} of building the category $\CC_i$ which is equivalent to the one presented above. - With this other method, a sort specification is described by a countable simple direct category $S$ (i.e. a countable category where all the arrows follow an unique direction, and $\Hom$-sets are finite). The models of the sort specification are therefore the presheaves over the category $S$ called $\left[S,\Set\right]$. + With this other method, a sort specification is described by a finite simple direct category $S$ (i.e. a finite category where all the arrows follow an unique direction, and $\Hom$-sets are finite). The models of the sort specification are therefore the presheaves over the category $S$ called $\left[S,\Set\right]$. \paragraph{Constructing $S$ as a sequence} In order to fall back on the definition we gave in the formal proof, we will build the final countable simple direct category $S$ as a sequence $\emptyset = S_0,S_1,\dots,S_i$ where $S_i$ is the category describing the sort specification limited to the $i$ first sort declarations. @@ -943,12 +949,12 @@ \end{center} \begin{remark} - This definition is reversable (up to the order of the sorts), and therefore, one can define a sequence of $\Gamma_i$ functors from any countable simple direct category. + This definition is reversible (up to the order of the sorts), and therefore, one can define a sequence of $\Gamma_i$ functors from any countable simple direct category. \end{remark} - \paragraph{Falling back on the formal proof} + \paragraph{Link with the formal proof} - In the formal proof, we used categories $\CC_i$ and functors $H_i : \CC_i \to \Set$. We now undertand that the categories $\CC_i$ are defined on top of the categories $S_i$ with $\CC_i := \left[S_i,\Set\right]$. + In the formal proof, we used categories $\CC_i$ and functors $H_i : \CC_i \to \Set$. We now understand that the categories $\CC_i$ are defined on top of the categories $S_i$ with $\CC_i := \left[S_i,\Set\right]$. In the same way, the functors $H_i : \CC_{i-1} \to \Set$ are defined on top of the functors $\Gamma_i$ with the following relation: \[ @@ -1072,7 +1078,7 @@ We have described a relation between both categories, which is an coreflection, i.e. an adjunction where the left adjoint is full and faithful. This adjunction allows us to build the initial model of the initial GAT from the initial model of the transformed GAT, so one can study properties of GATs with only two sorts and transpose them to any GATs. - There is still work to do in order to make the contents of this document apply to any GAT instead of only sort specifications. There is also ways of generalizing our formal construction to descriptions more general than GATs. + There is still work to be done in order to make the contents of this document apply to any GAT instead of only sort specifications. There are also ways of generalizing our formal construction to description more general than GATs, like GATs with sorts mutually included one into the other. @@ -1156,25 +1162,16 @@ Now, we take $(g,h)$ a morphism from $(X,Y)$ to $E(Z)$. - The morphism $\phi^{-1}_{XYZ}(g,h)$ of $\BB_i$ from $W(X,Y)$ to $Z$ is a morphism of $\BB_{i-1}$ from $X \tl^{i-1} K_{H_iF_{i-1}} (X,Y)$ to $R_{i-1}^i(Z)$ that make a specific diagram commute. We build this morphism using the universal property of $\tl^{i-1}$, stated in the introduction of this section. - - \[ - \phi^{-1}_{XYZ}(g,h) := \left\{g ; \square \right\} - \] - - \todo{Est-ce qu'il faut que j'écrive $R_{i-1}^i\phi^{-1}_{XYZ}(g,h) := ...$ pour être plus «homogène» ?} - - Where $\square$ is a morphism $K_{H_iF_{i-1}} (X,Y) \to R_0^i Z$ in $\TSet$ defined by the following diagram: + The morphism $\phi^{-1}_{XYZ}(g,h)$ of $\BB_i$ from $W(X,Y)$ to $Z$ is a morphism of $\BB_{i-1}$ from $X \tl^{i-1} K_{H_iF_{i-1}} (X,Y)$ to $R_{i-1}^i(Z)$ that make a specific diagram commute. We build this morphism using the universal property of $\tl^{i-1}$ stated in the introduction of this section on the morphisms $g$ and $\square$, where $\square$ is a morphism $K_{H_iF_{i-1}} (X,Y) \to R_0^i Z$ in $\TSet$ defined by the following diagram: \begin{center} % YADE DIAGRAM PhiXYZ-1Square.json % GENERATED LATEX \input{graphs/PhiXYZ-1Square.tex} % END OF GENERATED LATEX - \end{center} - Finally, we check that $\phi^{-1}_{XYZ}(g,h)$ is a morphism of $\BB_i$ from $W(X,Y)$ to $Z$, i.e. that it makes the following diagram commute: + We check that the morphism $\{g;\square\}$ verifies the property of morphisms of $\BB_i$ i.e. it makes the following diagram commute: \begin{center} % YADE DIAGRAM PhiXYZ-1MorphismOfBi.json @@ -1183,6 +1180,12 @@ % END OF GENERATED LATEX \end{center} + Therefore, we can define $\phi^{-1}_{XYZ}(g,h)$ such that + \[ + R_{i-1}^i\phi^{-1}_{XYZ}(g,h) := \left\{g ; \square \right\}_{i-1} + \] + + \subsection{Composition $\phi_{XYZ} \circ \phi_{XYZ}^{-1}$} The first component of $\phi_{XYZ} (\phi_{XYZ}^{-1}(g,h))$ is @@ -1205,7 +1208,7 @@ (R_0^{i-1}\{g,\square\})_\El \circ (\inj^{i-1}_2)_\El = \square_\El \]} - The diagram commutes, and so we can deduce that the second component of $\phi_{XYZ}(f)$ is $h$, by proprty of the pullback $E(Z)$ + The diagram commutes, and so we can deduce that the second component of $\phi_{XYZ}(f)$ is $h$, by property of the pullback $E(Z)$ \subsection{Composition $\phi_{XYZ}^{-1} \circ \phi_{XYZ}$} @@ -1329,47 +1332,52 @@ % END OF GENERATED LATEX \end{center} - \section{Misc} - \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) - \] - A morphism from $(X,\Cstr)$ to $(X', \Cstr')$ is a morphism from $X$ to $X'$ in $\TSet$ (i.e. a natural transformation $X \implies X'$) which makes the following diagram commute, for all $a$ in $S_{i-1}$. - - \begin{center} - % YADE DIAGRAM BiMorphismDiagram.json - % GENERATED LATEX - \input{graphs/BiMorphismDiagram.tex} - % END OF GENERATED LATEX - \end{center} - - Identities and compositions are that of the base category $\TSet$, and categorical equalities are trivially derived from the diagram above. - - The diagram expresses as - \[ - \forall \gamma \in \Hom_{G_{a-1}\Gamma_a,X}, \quad \Cstr'_a(f \circ \gamma) = f_\UU(\Cstr_a \gamma) - \] - - \todo{Define properly the use of \this} - - \subsection{$G$ and $F$ infinite constructions} - - \[ - G_i(Y) = \left(\sum_{a\in S_i}H_{Y(a)}\left(\lim_{(a/S_i)*}\overline{Y_a}\right), \lambda a.\lambda \eta.(a,u (\inj_2 \star))\right) - \] - - where $u : \left(Y(a) \oplus 1, \inj_1\right) \to (\lim_{(a/S_i)*} \overline{Y_a})$ - - so that $\varphi_{b,f} u (\star) = \eta_\El^b(f)$ - - \[ - F_i(X,\Cstr)(a) = X(p)^{-1}\left(\Cstr_a\left(\Hom_{\BB_{a-1}}(G_{a-1}\Gamma_a,X)\right)\right) - \] - \[ - F_i(X,\Cstr)(f : a \to b)(X(p)(x); x \in \Cstr_a(\eta)) = \eta_\El^b(f) - \] - - \todo{Show that those are the same functors as those defined recursively. Prove the adjunction/reflection infinitely ?} +% \section{Misc} +% \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) +% \] +% A morphism from $(X,\Cstr)$ to $(X', \Cstr')$ is a morphism from $X$ to $X'$ in $\TSet$ (i.e. a natural transformation $X \implies X'$) which makes the following diagram commute, for all $a$ in $S_{i-1}$. +% +% \begin{center} +% % YADE DIAGRAM BiMorphismDiagram.json +% GENERATED LATEX +\input{graphs/BiMorphismDiagram.tex} +% END OF GENERATED LATEX +% % GENERATED LATEX +% \input{graphs/BiMorphismDiagram.tex} +% % END OF GENERATED LATEX +% \end{center} +% +% Identities and compositions are that of the base category $\TSet$, and categorical equalities are trivially derived from the diagram above. +% +% The diagram expresses as +% \[ +% \forall \gamma \in \Hom_{G_{a-1}\Gamma_a,X}, \quad \Cstr'_a(f \circ \gamma) = f_\UU(\Cstr_a \gamma) +% \] +% +% \todo{Define properly the use of \this} +% +% \subsection{$G$ and $F$ infinite constructions} +% +% \[ +% G_i(Y) = \left(\sum_{a\in S_i}H_{Y(a)}\left(\lim_{(a/S_i)*}\overline{Y_a}\right), \lambda a.\lambda \eta.(a,u (\inj_2 \star))\right) +% \] +% +% where $u : \left(Y(a) \oplus 1, \inj_1\right) \to (\lim_{(a/S_i)*} \overline{Y_a})$ +% +% so that $\varphi_{b,f} u (\star) = \eta_\El^b(f)$ +% +% \[ +% F_i(X,\Cstr)(a) = X(p)^{-1}\left(\Cstr_a\left(\Hom_{\BB_{a-1}}(G_{a-1}\Gamma_a,X)\right)\right) +% \] +% \[ +% F_i(X,\Cstr)(f : a \to b)(X(p)(x); x \in \Cstr_a(\eta)) = \eta_\El^b(f) +% \] +% +% \todo{Show that those are the same functors as those defined recursively. Prove the adjunction/reflection infinitely ?} \end{document} + + diff --git a/Report/graphs/TlUniversal.json b/Report/graphs/TlUniversal.json index 8afd40f..26c2182 100644 --- a/Report/graphs/TlUniversal.json +++ b/Report/graphs/TlUniversal.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\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"R_0^i\\inj_1^i","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\\{g,h\\}","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"kind":"normal","label":"R_0^ig","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":7,"label":{"kind":"normal","label":"g","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":8,"label":{"kind":"normal","label":"\\inj_2^i","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1}],"nodes":[{"id":0,"label":{"isMath":true,"label":"R_0^iX","pos":[100,94],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"R_0^i(X \\tl^i Y)","pos":[300,94],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^iZ","pos":[300,176],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"Y","pos":[500,94],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file +{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":7,"label":{"kind":"normal","label":"R_0^i\\inj_1^i","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":8,"label":{"kind":"normal","label":"R_0^i\\{g,h\\}","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":9,"label":{"kind":"normal","label":"R_0^ig","style":{"alignment":"right","bend":0.10000000000000003,"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":"g","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":11,"label":{"kind":"normal","label":"\\inj_2^i","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":4,"id":12,"label":{"kind":"normal","label":"\\inj_1^i","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":"\\{g,h\\}","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":4,"id":14,"label":{"kind":"normal","label":"g","style":{"alignment":"right","bend":0.10000000000000003,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6}],"nodes":[{"id":0,"label":{"isMath":true,"label":"R_0^iX","pos":[370,84],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"R_0^i(X \\tl^i Y)","pos":[551,84],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^iZ","pos":[551,167],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"Y","pos":[727,84],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"X","pos":[100,84],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"X \\tl^i Y","pos":[249,84],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"Z","pos":[249,167],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/header.tex b/Report/header.tex index 311394f..452152e 100644 --- a/Report/header.tex +++ b/Report/header.tex @@ -191,4 +191,6 @@ \fancyfoot[R]{\textbf{\thepage / \pageref{LastReportPage}}} \pagestyle{fancy} +\usepackage{titling} + \addbibresource{Bilibibio.bib} \ No newline at end of file