From 4effe18e0f64fbddd182ecf00348b533df723060 Mon Sep 17 00:00:00 2001 From: Samy Avrillon Date: Fri, 16 Aug 2024 20:40:28 +0200 Subject: [PATCH] Removing examples from the proof --- Report/M2Report.tex | 74 +++++++++++---------------------------------- 1 file changed, 17 insertions(+), 57 deletions(-) diff --git a/Report/M2Report.tex b/Report/M2Report.tex index 9a2cb5c..fb89c5b 100644 --- a/Report/M2Report.tex +++ b/Report/M2Report.tex @@ -110,7 +110,8 @@ % END OF GENERATED LATEX \end{center} - \section{Example} + \section{Examples} + \label{sec:Examples} Before making the formal proof, we will study our construction on three examples. @@ -132,6 +133,8 @@ \subsection{The empty sort specification} + \label{sec:EmptySortSpec} + Our first example is the empty sort specification. As our proof will we an induction on the number of sorts, its first step will always be creating the objects for this empty sort specification. \paragraph{Category of models of the empty sort specification} @@ -162,7 +165,7 @@ % END OF GENERATED LATEX \end{center} - This category is equivalent to the catgegory $\FamSet$ with an equivalence we will see later\inlinetodo{Insérer la référence} + This category is equivalent to the catgegory $\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 \begin{itemize} @@ -486,7 +489,7 @@ F_3G_3(Y)_\Tm(\Delta,A) \simeq Y_\Tm(\Delta,A) \] - And therefore $F_3G_3 \equiv \Id_{\CC_3}$. + And therefore $F_3G_3 \cong \Id_{\CC_3}$. \subsection{Another sort specification} \todo{L'exemple, ou sinon remplacer toutes les occurences de «trois» par «deux»} @@ -568,7 +571,7 @@ \label{SetXSetXEquivalence} When the category $\mathcal{C}$ is $\Set$, we have the equivalence - \[\Set/X \simeq \Set^X\] + \[\Set/X \cong \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 @@ -588,10 +591,9 @@ Morphisms are translated using the same logic. - \paragraph{Category of models of the two-sort sort specification} - \label{sec:categoryOfModelsOfTwoSorts} - 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 $\FamSet$, defined as $(X:\Set) \times \Set^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: - + This equivalence justifies that we used $\TSet$, the category of presheaves over $\TT$ instead of $\FamSet$ to describe the category of models of the sort specification $(\mathcal{O},\El)$ in \autoref{sec:EmptySortSpec}. + + We recall that the category $\TT$ is as follows \begin{center} % YADE DIAGRAM CategoryTT.json % GENERATED LATEX @@ -601,13 +603,7 @@ This category is equivalent to the catgegory $\FamSet$, as $(X : \Set) \times \Set^X$ is equivalent to $(X : \Set) \times (\Set/X)$ (as seen above), which is isomorphic to $\TSet$ (both categories consists of two sets and one arrow between them). - 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$. + The categories of models of the transformed GATs will be built atop of this category $\BB_0 = \TSet$. \paragraph{$K$ functor} @@ -618,16 +614,16 @@ The morphisms are translated as-is. \begin{remark} - This functor can be constructed using the formal construction of the Grothendieck construction of $\TSet \cong (X: \Set) \times (\Set/X)$ as a pullback in the category of categories $\Cat$ + This functor can be constructed using the formal construction of the Grothendieck construction of $\TSet \simeq (X: \Set) \times (\Set/X)$ as a pullback in the category of categories $\Cat$ \end{remark} \subsection{Initialization} - In this subsection, we will build the objects of the first step of our induction. This will correspond to the empty sort specification, i.e. the induction step $i = 0$. + In this subsection, we will recall objects built in \autoref{sec:EmptySortSpec}, and build some other objects corresponding to the empty sort specification i.e. the first step of our induction. \begin{itemize} \setlength\itemsep{-1ex} - \item $\CC_0$ is $\one$, the category with only one object $\star$ and one trivial morphism (i.e. the terminal category of $\Cat$), because the empty sort specification only has one model. - \item $\BB_0$ is $\TSet$, the category of models of the $(\mathcal{O},\El)$ sort specification (see dedicated paragraph in last subsection for a description). + \item $\CC_0$ is $\one$, the category with only one object $\star$ and one trivial morphism (i.e. the terminal category of $\Cat$) + \item $\BB_0$ is $\TSet$, the category of models of the $(\mathcal{O},\El)$ sort specification. \item The universal property of $\tl^0$ is that of the coproduct. Therefore, we will define $\tl^0 : \BB_0 \times \BB_0 \to \BB_0$ to be the coproduct $\oplus$ of $\TSet$, with $\inj_\tl^0 : X \to X \oplus Y$ being the first injector of the coproduct. The second injector of the coproduct $\oplus$ will be refered as $\inj_2$. \item $F_0 : \TSet \to \one$ is the terminal functor of $\Cat$ \item $G_0 : \one \to \TSet$ is the functor that sends the only object of $\one$ to the initial object of $\TSet$: $0_\TSet$ @@ -645,13 +641,9 @@ \label{sec:constructingCategory} In this part, i will show how we construct recursively both categories $\CC_i$ and $\BB_i$, along with the functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$. We will use the loop invariants that we expressed in the introduction of this section. - In order to construct the categories, we need some object describing the specific sort we are adding to the categories. This object is a specific functor $H_i : \CC_{i-1} \to \Set$. Those functors are the same that Altenkirsh and al. \cite{Altenkirch2018} used in their paper to describe a specification of sorts. + In order to construct the categories, we need some object describing the sorts we are adding to the categories. This object is a given functor $H_i : \CC_{i-1} \to \Set$. Those functors are the same that Altenkirsh and al. \cite{Altenkirch2018} used in their paper to describe a specification of sorts. They are such that, for $X : \CC_{i-1}$ a model, they describe the set $H_iX$ of parameter range for the added sort. We gave an example of those functors in section \nameref{sec:Examples} if you want to understand how they work. There is also a way of obtaining them directly from the syntax, described in section \nameref{sec:HiFromSyntax}. We suppose that those $H_i$ functors are given. - \begin{remark} - There is a way of getting the functor $H_i$ from the syntax, which is described in \autoref{sec:HiFromSyntax}. - \end{remark} - \subsubsection{Constructing $\CC_i$} We construct the category $\CC_i$ as the following Grothendieck pair: @@ -662,38 +654,6 @@ This way of constructing the category has formerly been described by Altenkirsch and al. \cite{Altenkirch2018}, with the only difference of the equivalence $\Set/H_i(X) \simeq \Set^{H_i(X)}$. - \paragraph{An example of $H_i$ functors} - Let us now give an example of those $H_i$ objects for our type theory example. - - \[ - \boxed{\Con : \Set} - \] - We begin with the following functor, corresponding to the sort declaration above - \[ - H_1(\star) = 1 \in \Set - \] - - This corresponds to the fact that $\Con$ takes no parameter. - - Therefore $\CC_1 = 1 \times \Set^1 \simeq \Set$, which 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 types need \emph{one} context to be built. - - Therefore $\CC_2 = (X:\Set) \times (\Set/X) \simeq (X:\Set) \times (\Set^X) = \FamSet$, a model $X$ is a family of sets $\left(X_\Ty(\Gamma)\right)_{\Gamma \in X_\Con}$, as expected. - \[ - \boxed{\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set} - \] - - Finally, we take the functor $H_3(X) = \sum_{\Gamma : X_\Con}X_\Ty(\Gamma)$. It means that terms need \emph{one} context, and \emph{one} type of that context. - - An object of that final category $\CC_3$ is a triple - \[ - (X_\Con: \Set, X_\Ty : X_\Con \to \Set, X_\Tm : (\Delta: X_\Con) \to X_\Ty(\Delta) \to \Set) - \] \subsubsection{Constructing $\BB_i$} We construct the category $\BB_i$ as follows. @@ -852,7 +812,7 @@ 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 \autoref{sec:tlUniversalProperty} + 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\}