From 19f72c6f51ef98a9acf4f10e68bdef17ecb608b2 Mon Sep 17 00:00:00 2001 From: Samy Avrillon Date: Fri, 16 Aug 2024 19:53:39 +0200 Subject: [PATCH] Ajout d'une partie exemples --- Report/M2Report.tex | 425 ++++++++++++++++++++-- Report/graphs/AdjunctionLevel0.json | 1 + Report/graphs/TypeTheoryConstruction.json | 1 + Report/header.tex | 9 + 4 files changed, 405 insertions(+), 31 deletions(-) create mode 100644 Report/graphs/AdjunctionLevel0.json create mode 100644 Report/graphs/TypeTheoryConstruction.json diff --git a/Report/M2Report.tex b/Report/M2Report.tex index 66581ce..1794a5a 100644 --- a/Report/M2Report.tex +++ b/Report/M2Report.tex @@ -110,50 +110,408 @@ % END OF GENERATED LATEX \end{center} - \section{Constructing the coreflection} + \section{Example} - \paragraph{Structure of the proof} + Before making the formal proof, we will construct and explain the objects on two examples. + \subsection{Structure of the proof} + + We will formalize the transformation for \emph{sort specifications} (i.e. lists of sort declarations). + + This proof will be an induction on the number of sorts taken into account. At each step, we will add a new sort declaration, represented by a functor $H_i$ described later (\autoref{sec:constructingCategory}). + + At the $i$-th recursion step, we will build the following objects : + \begin{itemize} + \setlength\itemsep{-1ex} + \item The category of models of the GAT $\CC_i$ + \item The category of models of the transformed GAT $\BB_i$ + \item A forgetful functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$. - We will formalize the transformation for \emph{sort specifications} (i.e. lists of sort declarations). + Those functors compose themselves into a functor $R_0^i : \BB_i \to \BB_0$: + \[ + 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 a morphism $\inj_\tl^i : X \to 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 two following diagrams commute: + \label{sec:tlUniversalProperty} - This proof is an induction on the number of sorts taken into account. At each step, we will add a new sort declaration, represented by a functor $H_i$ described later (\autoref{sec:constructingCategory}). + \begin{center} + % YADE DIAGRAM TlUniversal.json + % GENERATED LATEX + \input{graphs/TlUniversal.tex} + % END OF GENERATED LATEX + \end{center} - At the $i$-th recursion step, we will build the following objects : - \begin{itemize} - \setlength\itemsep{-1ex} - \item The category of models of the GAT $\CC_i$ - \item The category of models of the transformed GAT $\BB_i$ - \item A forgetful functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$ that creates limits. In our type theory example, $R_1^2$ is a functor from the category of models of $(\mathcal{O},\El,\Con,\Ty,\Tm)$ to the category of models of $(\mathcal{O},\El,\Con,\Ty)$. + where $\en_0^i$ is the following composition: + + \[\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)\] + + And where $\inj_2$ is the second injector of $\oplus$, the coproduct of the category $\BB_0 = \TSet$. We will define $\tl^0$ to be $\oplus$, so the equality above holds. + + 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$. + + \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_\tl^i$ is an isomorphism. The inverse isomorphism will be denoted as $(F_i\inj_\tl^i)^{-1}$ + \end{itemize} + + \subsection{The empty sort specification} + + Our proof will we an induction on the number of sorts, and so the first step will be creating the objects for the empty sort specification. + + Therefore we will build the following objects + + \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$. - Those functors compose themselves into a functor $R_0^i : \BB_i \to \BB_0$, that also creates limits: - \[ - 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 a morphism $\inj_\tl^i : X \to 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 two following diagrams commute: - \label{sec:tlUniversalProperty} + \paragraph{Category of models of the transformed GAT} + + The transformed GAT for the empty sort specification is the sort specification $(\mathcal{O},\El)$ (no constructors as there are no sort in the initial sort specification): + \vspace{.5ex} + \begin{center} + \renewcommand\arraystretch{1} + \begin{tabular}{|l|} + \hline + $\UU : \Set$ \\ + $\El : \mathcal{O} \to \Set$ \\ + \hline + \end{tabular} + \end{center} + \vspace{.5ex} + + The usual way of defining the category of models of this sort specification is by taking the category of families of sets $\FamSet$, whose objects are pairs of a set $X$ and a family of sets indexed by $X$ : $(Y_x)_{x\in X}$. However, we will rather use another category : $\TSet$, the category of presheaves over the category $\TT$, the category with two object and one non-trivial arrow between them. The objects and morphism of $\TT$ are described below: \begin{center} - % YADE DIAGRAM TlUniversal.json + % YADE DIAGRAM CategoryTT.json % GENERATED LATEX - \input{graphs/TlUniversal.tex} + \input{graphs/CategoryTT.tex} % END OF GENERATED LATEX \end{center} - - where $\en_0^i$ is the following composition: - \[\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)\] + This category is equivalent to the catgegory $\FamSet$ with an equivalence we will see later\inlinetodo{Insérer la référence} - And where $\inj_2$ is the second injector of $\oplus$, the coproduct of the category $\BB_0 = \TSet$. We will define $\tl^0$ to be $\oplus$, so the equality above holds. + With this formalisation, a model of this sort specification is a functor $X : \TT \to \Set$, 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} - 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$. - - \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_\tl^i$ is an isomorphism. The inverse isomorphism will be denoted as $(F_i\inj_\tl^i)^{-1}$ - \end{itemize} + We will denote this category of models of the empty sort specification as $\BB_0$. + + We notice that the category $\BB_0$ has a coproduct that we will denote as $\tl^0$. The two injectors of this coproduct will be denoted as $\inj_1^0$ and $\inj_2^0$. + + \paragraph{Functors} + + We want to show that there is a reflection between those two categories $\BB_0$ and $\CC_0$ as follows: + + \begin{center} + % YADE DIAGRAM AdjunctionLevel0.json + % GENERATED LATEX + \input{graphs/AdjunctionLevel0.tex} + % END OF GENERATED LATEX + \end{center} + + $F_0 : \TSet \to \one$ is simply the terminal functor of $\Cat$, i.e. the functor sending all objects to $\star$, the only object of $\one$, and all morphisms to $\id_\star$. + + $G_0 : \one \to \TSet$ is the functor that sends the only object of $\one$ to the initial object of $\TSet$: $0_\TSet$ (such that $G_0$ preserves colimits) + + 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) + \] + + 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. + + \subsection{Type theory example} + We will take as a first example the sort specification of type theory presented in the introduction. The sort specification and its transformation are as follows: + + \vspace{1ex} + \begin{center} + \renewcommand\arraystretch{1} + \begin{tabular}{|l|l|} + \hline + & $\UU : \Set$ \\ + & $\El : \mathcal{O} \to \Set$ \\ + $\Con : \Set$ & $\Con : \mathcal{O}$\\ + $\Ty : (\Gamma : \Con) \to \Set$ & $\Ty : (\Gamma : \underline{\Con}) \to \mathcal{O}$\\ + $\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set$ & $\Tm : (\Delta : \underline{\Con}) \to (A : \underline{\Ty\;\Delta}) \to \mathcal{O}$ \\ + \hline + \end{tabular} + \end{center} + \vspace{1ex} + + We will build the following objects, step by step, adding one sort at a time: + + \begin{center} + % YADE DIAGRAM TypeTheoryConstruction.json + % GENERATED LATEX + \input{graphs/TypeTheoryConstruction.tex} + % END OF GENERATED LATEX + \end{center} + + Where the categories $\CC_i$ are the categories of models of the sort specification limited to the $i$ first sort declarations, and $\BB_i$ are the categories of models of the transformed GAT limited to the $i$ first sort declarations. For example, $\CC_2$ is the category of models of the two first sorts of the sort specification ($\Con$,$\Ty$). $\BB_0$,$\CC_0$,$F_0$, and $G_0$ have been defined in the last subsection. + + The $R^i_{i-1}$ functors between the categories are forgetful functors that forgets about the added sorts. + + I will only give here the explanation of functors $F_3$ and $G_3$, omitting the intermediate functors $F_1$,$G_1$,$F_2$,$G_2$. Their construction is given in the complete proof. + + \paragraph{Category of models} + + We have seen in the introduction how was a model of the type theory sort specification. We will rebuild that inductively, adding one sort at a time. + + In order to construct those categories in a generic way, we will define functors $H_X : \CC_{X-1} \to \Set$ that will describe the \enquote{parameters} of the sort declaration. + + \[ + \boxed{\Con : \Set} + \] + We begin with the following functor, corresponding to the sort declaration above + \[ + 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$. + + We build $\CC_1$ to be a pair of + \begin{itemize} + \item An object $X_0$ of $\CC_0$ + \item A family of sets $X_\Con$ indexed by $H_\Con(x) = 1$ + \end{itemize} + + As there is only one object in $\CC_0$ and that a family of sets indexed by $1$ is simply a set, we have that this category $\CC_1$ is isomorphic to $\Set$ (i.e. the category of sets). + This is as expected: a model $X$ consists of a set $X_\Con$. + + \[ + \boxed{\Ty : (\Gamma : \Con) \to \Set} + \] + + Then, we take the functor $H_2(X) = X_\Con$, corresponding to the sort declaration above. This functor means that $\Ty$ takes one parameter of type $\Con$ i.e. There is exactly one $\Ty$ sort for every $\Con$ there is in the model. + + Again, we build $\CC_\Ty$ to be a pair of + \begin{itemize} + \item A model $X_\Con$ from $\CC_1$ + \item A family of sets $X_\Ty$ indexed by $H_\Ty(X_\Con) = X_\Con$ + \end{itemize} + + This category is, as expected, the category $\FamSet$ of families of sets i.e. objects are pairs of a set $X_\Con$ and of a family indexed by $X_\Con$: $(X_\Ty(\Gamma))_{\Gamma\in X_\Con}$. + + \[ + \boxed{\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set} + \] + + The functor $\CC_2 \to \Set$ we will use here is defined as follows: + \[ + H_\Tm(X_\Con,X_\Ty) = \coprod_{\Delta \in \Con}X_\Ty(\Delta) \in \Set + \] + + $\coprod$ denotes the coproduct or disjoint union in $\Set$. This functor means that $\Tm$ takes one parameter $\Delta$ of sort $\Con$ and one parameter of sort $\Ty\;\Delta$, i.e. there is exactly one $\Tm$ for every pair of a $\Con$ called $\Delta$ in the model, and of a $\Ty$ associated to $\Delta$ in the model. + + We build $\CC_3$ to be a pair of + \begin{itemize} + \item A model $(X_\Con,X_\Ty)$ from $\CC_2$ + \item A family of sets $X_\Tm$ indexed by $H_\Tm(\Con)$ + \end{itemize} + + This category is isomorphic to the category composed of triples of + \begin{itemize} + \item A set $X_\Con$ + \item A family of sets indexed by $X_\Con$ : $\left(X_\Ty(\Gamma)\right)_{\Gamma \in X_\Con}$ + \item A family of sets indexed by $(\Delta : X_\Con)$ and $X_\Ty(\Delta)$ : + $\left(\left(X_\Tm(\Delta,A)\right)_{A \in X_\Ty(\Delta)}\right)_{\Delta \in X_\Con}$ + \end{itemize} + + \paragraph{Category of models of the transformed GAT} + + We have also seen in the introduction how was constructed the category of models of the transformed GAT. We will reconstruct it sort by sort. + + \[ + \boxed{\begin{array}{c} + \mathcal{O} : \Set \\ + \El : \mathcal{O} \to \Set + \end{array}} + \] + + We have seen in previous subsection that the category of models of this GAT is $\BB_0 = \TSet$. We will only add new \emph{constructors} to these models, and no new sorts. + + \[ + \boxed{\Con : \mathcal{O}} + \] + + We are adding a constructor to the model. This constructor takes no parameters, which means we want to select one sort out of our model to be the $\Con$ sort. And we recall that the sorts of a model $X : \TSet$ are the elements of $X_\UU$. + + Therefore a model of the above GAT with only one constructor is a model $X : \TSet$ along with an object $\Cstr^X_\Con \in X_\UU$. An object of $\BB_1$ is a pair of + \begin{itemize} + \item A functor $X : \TT \to \Set$ + \item An element $\Cstr^X_\Con \in X_\UU$ + \end{itemize} + + A morphism $f$ from $(X,\Cstr^X_\Con)$ to $(X',\Cstr^{X'}_\Con)$ is simply a morphism of $\TSet$ from $X$ to $X'$ that respects the constructor, i.e. that is such that + \[ + f_\UU(\Cstr^X_\Con) = \Cstr^{X'}_\Con + \] + + \[ + \boxed{\Ty : \underline{\Con} \to \mathcal{O}} + \] + + 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 + \[ + \Cstr^X_\Ty : X_p^{-1}(\Cstr^X_\Con) \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$} + This codomain is quite verbose, but we have another way of expressing it. In the final proof, we will have already constructed the functor $F_1 : \BB_1 \to \CC_1$, and we had a functor $H_\Ty : \CC_1 \to \Set$ that described the parameters of the sort declaration of $\Ty$ for the category $\CC_1$. Well, it turns out that $H_\Ty \circ F_1 : \BB_1 \to \Set$ describes exactly the codomain expressed above. + + Therefore, the category $\BB_2$ consists of a pair of + \begin{itemize} + \item A model $(X,\Cstr^X_\Con)$ from $\BB_1$ + \item A constructor $\Cstr^X_\Ty : H_iF_{i-1}(X,\Cstr^X_\Con) \to X_\UU$ + \end{itemize} + + One again, morphism $f$ from $(X,\Cstr^X_\Con,\Cstr^X_\Ty)$ to $(X',\Cstr^{X'}_\Con,\Cstr^{X'}_\Ty)$ are simply morphisms of $\BB_1$ from $(X,\Cstr^X_\Con)$ to $(X',\Cstr^{X'}_\Con)$ that respect the $\Cstr_\Ty$ constructor, i.e. that verifies, for every $\Gamma$ in $H_iF_{i-1}(X,\Cstr^X_\Con)$ that + \[ + f_\UU(\Cstr^X_\Ty(\Gamma)) = \Cstr^{X'}_\Ty(f_\El(\Gamma)) + \] + + \[ + \boxed{\Tm : (\Delta : \underline{\Con}) \to (A : \underline{\Ty\;\Delta}) \to \mathcal{O}} + \] + + This one is made like the others, a model of $\BB_3$ is a pair of + \begin{itemize} + \item A model $(X,\Cstr^X_\Con,\Cstr^X_\Ty)$ of $\BB_2$ + \item A constructor $\Cstr^X_\Tm$ that goes from $H_\Tm F_2 X$ to $X_\UU$ + \end{itemize} + + And morphism are restricted with the $\Tm$ constructor rule that states that for every $(\Delta,A)$ in $H_iF_{i-1}(X,\Cstr^X_\Con,\Cstr^X_\Ty)$ + \[ + f_\UU(\Cstr^X_\Tm(\Delta,A)) = \Cstr^{X'}_\Tm(f_\El(\Delta),f_\El(A)) + \] + + \paragraph{Constructing $G_3$} + + We want to make functors connecting those two categories + \[ + \begin{array}{l|l} + Y : \mathbf{\CC_3} & X : \mathbf{\BB_3} \\ + & X : \TSet\\ + Y_\Con : \Set & \Cstr^X_\Con : X_\UU \\ + \left(Y_\Ty(\Gamma)\right)_{\Gamma \in Y_\Con} & + \Cstr^X_\Ty : H_\Ty F_{1} (X,\Cstr^X_\Con) \to X_\UU \\ + \left(\left(Y_\Tm(\Delta,A)\right)_{A \in Y_\Ty(\Delta)}\right)_{\Delta \in Y_\Con} & + \Cstr^X_\Tm : H_\Tm F_{2} (X,\Cstr^X_\Con,\Cstr^X_\Ty) \to X_\UU \\ + \end{array} + \] + + Let's first look at the first component of the «result» $X = G_3(Y)$. It will be a functor of $\TSet$. We recall how $\TSet$ corresponds to the sort specification $(\mathcal{O},\El)$: + \begin{itemize} + \item $X_\UU$ is the set of all sorts + \item $X_\El$ is the set of all «objects» of those sorts + \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 indice of a set. + + \[\begin{array}{ccccccc} + + X_\El & = & + Y_\Con & \oplus & + \displaystyle\coprod_{\Gamma \in Y_\Con}Y_\Ty(\Gamma) & \oplus & + \displaystyle\coprod_{\Delta \in Y_\Con}\coprod_{A \in Y_\Ty(\Delta)}Y_\Ty(\Delta,A) \\ + \labeledupdownarrow{p}&&\labeledupdownarrow{}&&\labeledupdownarrow{\operatorname{proj}_1}&&\labeledupdownarrow{\operatorname{proj}_{2,1}}\\ + X_\UU & = & + 1 & \oplus & + Y_\Con & \oplus& + \displaystyle\coprod_{\Gamma \in Y_\Con}Y_\Ty(\Gamma) + \end{array}\] + where $\operatorname{proj}_1 : \coprod_{a\in A}B(a) \to A$ is the first projector of the coproduct, and $\operatorname{proj}_{2,1}$ get the index $ \coprod_{a \in A}B(a)$ of a double coproduct $\coprod_{a \in A}\coprod_{b\in B(a)} C(a,b)$ + \vspace{.2ex} + + Now, the constructors only have to give the right sort according to their arguments. So + \[\begin{array}{lcl} + \Cstr^X_\Con &=& \inj_1(\star)\\ + \Cstr^X_\Ty(\Gamma) &=& \inj_2(\Gamma) \\ + \Cstr^X_\Tm(\Delta,A) &=& \inj_3(\Delta,A) + \end{array}\] + + where $\inj_i$ is the $i$-th injector of the direct sum $\oplus$. + + \todo{Parler des morphismes ? Est-ce nécessaire ?} + + \paragraph{Constructing $F_i$} + + Now we will try to create an object $Y = F_i X$ of $\CC_3$ from an object $X$ of $\BB_3$. + + \begin{itemize} + \item $Y_\Con$ should be the set of all objects of sort $\Con$. In the transformed GAT, it means all objects of $\El$ which have been created with the sort $\Cstr^X_\Con$. Therefore we have + \[ + Y_\Con = X_p^{-1}(\left\{\Cstr^X_\Con\right\}) \subseteq X_\El + \] + \item $Y_\Ty(\Gamma)$ should be the set of all objects of sort $\Ty\;\Gamma$, which means all objects of $\El$ which have been created with the sort $\Cstr^X_\Ty(\Gamma)$. Therefore we have, for every $\Gamma$ in $Y_\Con$ + \[ + Y_\Ty(\Gamma) = X_p^{-1}(\{\Cstr^X_\Ty(\Gamma)\}) + \] + This is well-defined, as + \[ + \Gamma : Y_\Con = X(p)^{-1}(\{\Cstr^X_\Con\}) = H_\Ty(X(p)^{-1}(\{\Cstr^X_\Con\})) = H_\Ty F_1(X,\Cstr^X_\Con) + \] + \item In the same way, we define + \[ + Y_\Tm(\Delta,A) = X_p^{-1}(\Cstr^X_\Tm(\Delta,A)) + \] + which is also well-defined + \end{itemize} + + \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. + \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. + + An adjunction would be described by the following isomorphism: + \[ + \Hom_{\BB_3}\left(G_3Y,X\right) \simeq \Hom_{\CC_3}\left(Y,F_3X\right) + \] + + Recall that sorts of $G_3Y$ are all in the domain of some constructor, so therefore, a morphism of $\Hom_{\BB_3}(G_3Y,X)$ only acts on constructible sorts. + Also, the only sorts that remain in $F_3X$ are the one that were reached by some constructor of $X$, therefore a morphism of $\Hom_{\CC_3}(Y,F_3X)$ only acts on constructible sorts. + + Therefore, both morphism are only descriptions of actions on constructible sorts into constructible sorts. That's how we create the isomorphism. + + Morphisms of $\BB_3$ from $G_3Y$ to $X$ are morphisms of $\TSet$ that respect constructors. It means that + + \paragraph{A coreflection} + + If we look at $F_3G_3 Y$ for a model $Y$ of $\CC_3$, we remark that + \[\begin{array}{lcl} + F_3G_3(Y)_\Con &=& G(Y)_p^{-1}(\{\Cstr^{G(Y)}_\Con\})\\ + &=& G(Y)_p^{-1}(\{\inj_1 \star\}) \\ + &=& Y_\Con + \end{array}\] + and + \[\begin{array}{lcl} + F_3G_3(Y)_\Ty(\Gamma) &=& G(Y)_p^{-1}(\{\Cstr^{G(Y)}_\Ty(\Gamma)\})\\ + &=& G(Y)_p^{-1}(\{\inj_2 \Gamma\}) \\ + &=& proj_1^{-1}(\Gamma) \\ + &=& \left\{(\Gamma',A) \in \coprod_{\Gamma' \in Y_\Con}Y_\Ty(\Gamma') \middle| \Gamma' = \Gamma\right\}\\ + &\simeq& Y_\Ty(\Gamma) + \end{array}\] + and finally, with the same method, we get that + \[ + F_3G_3(Y)_\Tm(\Delta,A) \simeq Y_\Tm(\Delta,A) + \] + + And therefore $F_3G_3 \equiv \Id_{\CC_3}$. + + \section{Constructing the coreflection} + Here is a figure that describes the recursive construction of some of the above objects \begin{center} % YADE DIAGRAM GlobalRecursiveConstruction.json @@ -189,6 +547,7 @@ 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{Slice category over a set} + \label{SetXSetXEquivalence} When the category $\mathcal{C}$ is $\Set$, we have the equivalence \[\Set/X \simeq \Set^X\] @@ -545,7 +904,6 @@ \] It is a morphism of $\BB_i$ as it makes the following diagram commute: - \begin{center} % YADE DIAGRAM TlInj1MorphismOfBi.json % GENERATED LATEX @@ -1111,6 +1469,11 @@ + + + + + diff --git a/Report/graphs/AdjunctionLevel0.json b/Report/graphs/AdjunctionLevel0.json new file mode 100644 index 0000000..81e7be9 --- /dev/null +++ b/Report/graphs/AdjunctionLevel0.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\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":2,"label":{"kind":"normal","label":"F_0","style":{"alignment":"right","bend":0.10000000000000003,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":3,"label":{"kind":"normal","label":"G_0","style":{"alignment":"right","bend":0.10000000000000003,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":2,"id":4,"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":3}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\TSet = \\BB_0","pos":[300,97],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\CC_0 = \\one","pos":[572,97],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/TypeTheoryConstruction.json b/Report/graphs/TypeTheoryConstruction.json new file mode 100644 index 0000000..63bf10d --- /dev/null +++ b/Report/graphs/TypeTheoryConstruction.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\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":8,"label":{"kind":"normal","label":"F_3","style":{"alignment":"right","bend":0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":9,"label":{"kind":"normal","label":"G_3","style":{"alignment":"right","bend":0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":1,"id":10,"label":{"kind":"normal","label":"F_2","style":{"alignment":"right","bend":0.10000000000000003,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":11,"label":{"kind":"normal","label":"G_2","style":{"alignment":"right","bend":0.10000000000000003,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":5,"id":12,"label":{"kind":"normal","label":"G_1","style":{"alignment":"right","bend":0.10000000000000003,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":13,"label":{"kind":"normal","label":"F_1","style":{"alignment":"right","bend":0.10000000000000003,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":6,"id":14,"label":{"kind":"normal","label":"F_0","style":{"alignment":"right","bend":0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":15,"label":{"kind":"normal","label":"G_0","style":{"alignment":"right","bend":0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":0,"id":16,"label":{"kind":"normal","label":"R^3_2","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":17,"label":{"kind":"normal","label":"R^2_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":18,"label":{"kind":"normal","label":"R^1_0","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":0,"id":19,"label":{"kind":"normal","label":"R^3_0","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":13,"id":20,"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":12},{"from":10,"id":21,"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":11},{"from":8,"id":22,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":14,"id":23,"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":15}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\BB_3","pos":[225,45],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\BB_2","pos":[225,135],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\BB_1","pos":[225,225],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\CC_3","pos":[405,45],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\CC_2","pos":[405,135],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"\\CC_1","pos":[405,225],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\BB_0","pos":[225,315],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"\\CC_0","pos":[405,315],"zindex":0}}],"sizeGrid":90,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/header.tex b/Report/header.tex index f6811b1..19e4b47 100644 --- a/Report/header.tex +++ b/Report/header.tex @@ -146,6 +146,11 @@ \path[->] (0) edge["${\scriptstyle #2}$", pos=0.5, fore, black,=>, ] (1); \end{tikzpicture} } +\newcommand\labeledupdownarrow[1]{ +\begin{tikzpicture} + \path[->] (0,1) edge["${\scriptstyle #1}$", pos=0.5, fore, black,=>, ] (0,0); +\end{tikzpicture} +} \newcommand\diagram[1]{\begin{tcolorbox}\begin{center}\vspace{1.5cm}\Huge \texttt{\textbf{#1}}\vspace{1.5cm}\end{center}\end{tcolorbox}} @@ -161,4 +166,8 @@ \titleformat{\subparagraph}[runin]{\normalfont\normalsize\bfseries}{}{0em}{\subparaghaphboxedcontent} \titlespacing*{\subparagraph}{0pt}{3.25ex plus 1ex minus .2ex}{0.5em} +% Fixing Yade green +\definecolor{green}{RGB}{11,102,35} + + \addbibresource{Bilibibio.bib} \ No newline at end of file