From 1b087759bb07f13b6263adb0745dbc9ba128e91c Mon Sep 17 00:00:00 2001 From: Samy Avrillon Date: Thu, 15 Aug 2024 23:32:42 +0200 Subject: [PATCH] Filled part 3 (2/3) --- Report/M2Report.tex | 242 +++++++++++++++++++---------- Report/graphs/TyThExampleSCat.json | 1 + 2 files changed, 159 insertions(+), 84 deletions(-) create mode 100644 Report/graphs/TyThExampleSCat.json diff --git a/Report/M2Report.tex b/Report/M2Report.tex index 76addb1..c61bc41 100644 --- a/Report/M2Report.tex +++ b/Report/M2Report.tex @@ -89,7 +89,7 @@ $\dots$ \end{tabular} - This process is useful when studying GATs, as it allows to restrict a study to GATs with only two sorts without loss of generality. Filippo Sestini noticed that in his thesis \cite{SestiniPhD}, although they didn't prove it. + This process is useful when studying GATs, as it allows to restrict a study to GATs with only two sorts without loss of generality. Filippo Sestini noticed that in his thesis \cite{SestiniPhD}: \begin{quote} Many instances of multi-sorted IITs [IITs are a variant 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. @@ -234,14 +234,14 @@ \paragraph{$K$ functor} - We define a helper functor $K : (X:C) \times (\Set/A(X)) \to \TSet$ defined as follows + We define a helper functor $K_A : (X:C) \times (\Set/A(X)) \to \TSet$ defined as follows \[ - K_X(X,(Y,f)) = \TSetObject{Y}{f}{A(X)} + K_A(X,(Y,f)) = \TSetObject{Y}{f}{A(X)} \] The morphisms are translated as-is. \begin{remark} - This functor can be constructed using the formal construction of the Grothendieck construction as a pullback in the category of categories $\Cat$ + 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$ \end{remark} \subsection{Initialization} @@ -283,6 +283,8 @@ \] and where $H_i$ is the specific functor described above. + 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. @@ -305,7 +307,6 @@ 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} \] @@ -516,7 +517,7 @@ The proof is that statement is given in \autoref{apx:FG-refl}. - \subsection{Inductive step: $\tl^i$} + \subsection{Inductive step: Constructing $\tl^i$} \label{sec:coproductConstr} @@ -602,58 +603,170 @@ And we know from the previous induction step that $F_{i-1}\inj_\tl^{i-1}$ is an isomorphism. Therefore, $F_i\inj_\tl^i$ is an isomorphism. - \section{Misc} + \section{Other Properties} + \subsection{Fibration of the category $\CC_i$} + In the formal proof, we defined $\CC_i$ as an inductive Grothendieck construction as in Altenkirsch and al. papers \cite{Altenkirch2018}. - \subsection{Fiore's Category - Fibration of the category of sorts} + But there is an other way \cite{Fiore2008} of building the category $\CC_i$ which is equivalent to the one presented above. - Fiore \cite{Fiore2008} describes \emph{sort specifications} as countable simple direct categories (i.e. countable categories where all the arrows follow an unique direction and hom-sets are finite). The models of a GAT then are the presheaves over that category $S$: $\left[S,\Set\right]$. + 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]$. - One can understand the correspondance between those categories and sort specifications as follows: - \begin{itemize} - \item An object of the category is a sort of the specification. - \item An arrow $x$ from an object $s$ to an object $s'$ is a parameter of the sort declaration of $s$ of the for $(x : s' \dots)$. - \item The parameter $y$ of a parameter $x$ of a sort specification (i.e. the sort declaration parameter has the form $(x: s' \dots \left[y=z\right] \dots)$) is given by $z = x \circ y$. - \end{itemize} + \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. - \begin{remark} - We ignore in this definition identity arrows, and we will do so in the rest of this document. Identities are the only arrows that are not «directed» in the direct category. - - Interpreting the identity arrow would mean having a parameter of type $s$ to construct the sort $s$. which loops in a self-dependency. - - You can assume in the rest of the document that the formalizations \enquote{all arrows} or \enquote{the arrows} pointing to/from exclude identity arrows. - \end{remark} + The input data describing the GAT will be a sequence of finite functors $\Gamma_i : S_{i-1} \to \Set$. - \todo{Éventuellement changer tous les paramètres par la forme complète, exemple - \[ - \operatorname{eq}: (\Gamma : \Con) \to (A : \Ty \left[\Gamma=\Gamma\right]) \to \Tm \left[\Gamma=\Gamma\right] \left[A=A\right] \to \Tm \left[\Gamma=\Gamma\right] \left[A=A\right] \to \Ty \left[\Gamma=\Gamma\right] - \] - C'est bien plus verbeux et en pratique pas utilisé, mais permet de mieux voir la «composition» dans la catégorie de Fiore.} - \todo{Est-ce qu'on fait une notation \enquote{arrow*} pour dire «flèche qui n'est pas l'identité» pour plus de rigueur ?} + We will then construct the category $S_i$ by adding a single object $\alpha_i$ to the category $S_{i-1}$, along with morphisms $f : \alpha_j \to \alpha_{i+1}$ for $f \in \Gamma_{i+1}(\alpha_j)$ and $j \leq i$. The morphisms follow the composition condition, describing that every pair of morphisms $f : \alpha_j \to \alpha_{i+1}$ and $g : \alpha_k \to \alpha_{i+1}$ (i.e. $f\in\Gamma_{i+1}(\alpha_k)$ and $g\in\Gamma_{i+1}(\alpha_j)$) and for every morphism of $S_{i}$ $h : \alpha_j \to \alpha_k$, we have $\Gamma_{i+1}(h)(f) \circ f = g$. - For example the category version of the specification of sorts of Type Theory given above is defined as: + Avec le formalisme de la construction de Grothendieck, on peut formaliser la construction de la nouvelle catégorie comme cela: + \[ + S_i = S_{i-1} \times + \] - \begin{itemize} - \item There is three objects called $\Con$,$\Ty$, and $\Tm$. - \item The arrows are defined as - \begin{itemize} - \item There is no arrow going out of $\Con$ - \item There is one arrow going out of $\Ty$: $\Gamma$ pointing to $\Con$. - \item There is two arrows going out of $\Tm$: $\Delta$ pointing to $\Con$ and $\Gamma$ pointing to $\Ty$. - \end{itemize} - \item The $\Gamma$ parameter of $\Ty$ in the parameter $A$ of $\Tm$ is $\Delta$. Therefore, we have $\Delta = A \circ \Gamma$. - \end{itemize} + The final category is simply $S = \bigcup S_i$. - The category is pictured below: + In our type theory example, the category $S$ is constructed as follows: \begin{center} - % YADE DIAGRAM B1.json - % GENERATED LATEX - \input{graphs/B1.tex} - % END OF GENERATED LATEX + \begin{tabular}{c|c|c} + $\boxed{\Con : \Set}$ & + $\boxed{\Ty : (\Gamma : \Con) \to \Set}$ & + $\boxed{\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set}$ \\ + $S_1 = \qquad \Con$ & + $S_2 = \qquad \Con \leftarrow \Ty$ & + $S_3 = \qquad \Con \leftarrow \Ty \leftarrow \Tm$ \\ + $\left[S_1,\Set\right] \simeq \CC_1$ & + $\left[S_2,\Set\right] \simeq \CC_2$ & + $\left[S_3,\Set\right] \simeq \CC_3$ + \end{tabular} \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. + \end{remark} + + \paragraph{Falling back on 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 same way, the functors $H_i : \CC_{i-1} \to \Set$ are defined on top of the functors $\Gamma_i$ with the following relation: + \[ + H_i(X) := \Hom_{\left[S_{i-1},\Set\right]}\left(\Gamma_i,X\right) + \] + + \subsection{Creating semantics object from the syntax} + \label{sec:HiFromSyntax} + + In this part, we will see how the functors $\Gamma_i$ given above can be constructed from the syntax of a sort specification. The previous subsection gives us a way of constructing the $H_i$ functors from the $\Gamma_i$ functors, and thus one can make the complete proof with the definition below. + + \paragraph{Verbose sort specification} + We will take a verbose version of a sort specification, where when \enquote{implementing} a sort, we gave the name of the parameter and the name of the term. For example, our type theory example becomes the following verbose version: + + \begin{center} + \renewcommand\arraystretch{1.5} + \begin{tabular}{l} + $\Con : \Set$\\ + $\Ty : (\Gamma : \Con) \to \Set$ \\ + $\Tm : (\Delta : \Con) \to (A : \Ty \left[\Gamma \mapsto \Delta\right]) \to \Set$ + \end{tabular} + \end{center} + \vspace{1em} + The only sort declaration that changes is that of $\Tm$ as it is the only one for which one of its parameter is a sort with parameters. + + With that verbose definition, a generic sort specification is a list of sort declarations indexed by $\mathbb{T}$, the fully ordered set of all sorts. The sort declarations are as follow, for a sort $T \in \mathbb{T}$ + + \[ + T : \left[x_a^T : U_T(a) \left[x^{U_T(a)}_{b} \mapsto x^T_{v_T(a,b)}\right]_{b\leq I_{U_T(a)}}\right]_{a \leq I_T} \to \Set + \] + + Where + \begin{itemize} + \setlength\itemsep{-.2em} + \item $I_T$ is the number of parameters of the sort $T$ + \item $x^T_a$ is the $a$-th parameter of the sort $T$ + \item $U_T(a)$ is the sort of the $a$-th parameter of the sort $T$ (we have $U_T(a) < T$) + \item $I_{U_T(a)}$ is the number of parameters of the sort $U_T(a)$ i.e. the number of arguments we have to give to make an object of sort $U_T(a)$ + \item $x^{U_T(a)}_b$ is the $b$-th parameter of the sort $U_T(a)$ + \item $v_T(a,b)$ is the index of the parameter of the sort $T$ given as the $b$-th parameter of the $a$-th parameter of the sort $T$ (we have $v_T(a,b) < a$) + \item The types of parameters have to be respected, therefore we must have the equality + \[ + U_T(v_T(a,b)) = U_{U_T(a)}(b) + \] + \end{itemize} + + For example, for the above sort declaration, we would have + \begin{itemize} + \setlength\itemsep{-.2em} + \item $\mathbb{T} = \left\{\Con < \Ty < \Tm\right\}$ + \item $I_\Con = 0$, $I_\Ty = 1$, $I_\Tm = 2$ + \item $x^\Ty_1 = "\Gamma"$, $x^\Tm_1 = "\Delta"$, $x^\Tm_2 = "A"$ + \item $U_\Ty(1) = \Con$, $U_\Tm(1) = \Con$, $U_\Tm(2) = \Ty$ + \item $v_\Tm(2,1) = 1$ such that $x^\Tm_{v_\Tm(2,1)} = "\Delta"$ (associated to $x^\Ty_{b=1} = "\Gamma"$) + \end{itemize} + + \paragraph{Describing the category $S$} + + We will then describe what is the category $S$ corresponding to a given sort specification $(\mathbb{T},I,U,v)$ + + Its objects are simply the sorts, i.e. the elements of $\mathbb{T}$. + + Morphisms from a sort $T_x$ to a different sort $T_y$ are described by $U$ and correspond to the parameters of the sort $T_x$ that are of sort $T_y$. In other words: + + \[ + \Hom_{S}(T_x,T_y) = \left\{x^{T_x}_a\middle| a \leq I_{T_x} \text{ and } U_{T_x}(a) = T_y\right\} + \] + + We can see that the category is direct, because of the rule $U_T(a) < T$ i.e. if $T_x < T_y$ then $\Hom_S(T_x,T_y) = \emptyset$. + For every sort $T$, we define $\Hom_S(T,T)$ to contain only the identity morphism $\id_T$, for which composition rules are already defined. + + Composition is described by $v$, corresponding to\enquote{parameters of parameters}. + Let's take two morphisms $x^{T_x}_b : T_x \to T_y$ and $x^{T_y}_a : T_y \to T_z$. Their composition is defined by + \[ + x^{T_y}_a \circ x^{T_x}_b = x^{T_x}_{v_{T_x}(a,b)} + \] + + This composition is well-defined as + \[ + U_{T_x}(v_{T_x}(a,b)) = U_{U_{T_x}(a)}(b) = U_{T_y}(b) = T_z + \] + + For our type theory example, the category $S$ is as follows + + \begin{center} + % YADE DIAGRAM TyThExampleSCat.json + % GENERATED LATEX + \input{graphs/TyThExampleSCat.tex} + % END OF GENERATED LATEX + \end{center} + + \paragraph{Creating the functor $\Gamma_i$} + + We know we can create the functors $\Gamma_i$ directly from a complete category $S$, but we will look more in detail what those functors mean related to the syntax. + + If we are given the category $S_{i-1}$ with objects corresponding to the $i-1$ sorts already defined. + + We want to build a finite functor $\Gamma_i : S_{i-1} \to \Set$ corresponding to the following sort declaration of a new sort $T_i$ + + We will build $\Gamma_i$ as follows: + + \[ + \Gamma_i(T_x) = \left\{x^{T_i}_a\middle| a \leq I_{T_i} \text{ and } U_{T_i}(a) = T_x\right\} + \] + + \[ + \Gamma_i(x_b^{T_x} : T_x \to T_y)(x^{T_i}_a \in \Gamma_i(T_x)) = x^{T_i}_{v_{T_i}(a,b)} + \] + + This definition is redundant with that of the last paragraph, but it has the advantage of directly creating the functor $\Gamma_i$ that are used to create the functors $H_i$ and all the rest of the proof. + + \subsection{Non-recursive definitions} + + \subsubsection{Redefinition of $\BB_i$} + \subsubsection{Redefinition of $G_i$ and $F_i$} + \subsubsection{Non-direct base category} + \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) @@ -695,46 +808,6 @@ \todo{Show that those are the same functors as those defined recursively. Prove the adjunction/reflection infinitely ?} - - \subsection{Adding 2-transformation of constructors} - \label{sec:constructors2trans} - \todo{Describe the process} - - \subsection{Overview} - - \subsubsection{$\CC$ as presheaf category} - \label{sec:CtoSSetFiore} - We use the specification of sorts definition of Fiore \cite{Fiore2008}. - - A specification of sorts is given by a sequence of functors $\Gamma_i : S_{i-1} \to \Set$. We construct the category $S_{i+1}$ by adding a single object $\alpha_{i+1}$ to the category $S_{i}$, along with morphisms $f : \alpha_j \to \alpha_{i+1}$ for $f \in \Gamma_{i+1}(\alpha_j)$ and $j \leq i$. The morphisms follow the composition condition, describing that every pair of morphisms $f : \alpha_j \to \alpha_{i+1}$ and $g : \alpha_k \to \alpha_{i+1}$ (i.e. $f\in\Gamma_{i+1}(\alpha_k)$ and $g\in\Gamma_{i+1}(\alpha_j)$) and for every morphism of $S_{i}$ $h : \alpha_j \to \alpha_k$, we have $\Gamma_{i+1}(h)(f) \circ f = g$. - - We have define a sequence of direct categories $\emptyset = S_0 \subset S_1 \subset S_2 \subset \dots$ (with inclusions functors $I_i : S_{i+1} \to S_i$). We define the \enquote{final} direct category as $S = \bigcup S_i$ - - This definition is an isomorphism, so we can define a GAT categorically as any locally finite direct category. - - Then the semantics of the GAT is described as the category of presheaves over $S$, written $[S, \Set]$. - - Altenkirsch has another way of constructing the semantics of a specification of sorts \cite{Altenkirch2018}, and he also describes a way to describe constructors. - - So we can construct the base category, which is that of families of sets. - - - In order to construct the $i$-th sort, we use a finite functor $\Gamma_i : S_{i-1} \to \Set$ describing entirely the sort declaration. - - This functor is to be understood as $\Gamma_i(a)$ is the set of parameters of type $a$ for our new sort. In the above example, we would have $\Gamma_\Ty(\Con) = \{"\Gamma"\} = 1$ and $\Gamma_\Tm(\Con) = \{\Delta\}$,$\Gamma_\Tm(\Ty) = \{"A"\}$,$\Gamma_\Tm(\Gamma) = \left["A" \mapsto "\Delta"\right]$. - - Then, to construct $S_i$, we add one object $i$ to $S_{i-1}$, along with morphisms $x : i \to a$ for every $x \in \Gamma_i(a)$ for every $a$ in $S_{i-1}$. We also add equalities - $s \circ x = x'$ for every $s : b \to a$ and $x \in \Gamma_i(a)$ and $x' \in \Gamma_i(b)$ where $\Gamma_i(s)(x') = x$. - - \begin{remark} - We have that $\Hom_{S_i}(a,b) = \Gamma_b(a)$ or $(a/S_i)* \equiv \Gamma_a$.\inlinetodo{C'est sûr la deuxième partie ?} - - This equality allows us to construct the $\Gamma_i$ functors from the final $S$ category. - \end{remark} - - \subsection{Consructing the $H_i$ functors from the syntax} - \label{sec:HiFromSyntax} - \section{Summary} \lipsum[2-3] @@ -1017,5 +1090,6 @@ + diff --git a/Report/graphs/TyThExampleSCat.json b/Report/graphs/TyThExampleSCat.json new file mode 100644 index 0000000..94335e2 --- /dev/null +++ b/Report/graphs/TyThExampleSCat.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":2,"id":3,"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":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":"\"\\Delta\" \\;=\\; \\Gamma \\circ A","style":{"alignment":"right","bend":0.10000000000000003,"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}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file