diff --git a/Report/M2Report.tex b/Report/M2Report.tex index f92994c..65efac2 100644 --- a/Report/M2Report.tex +++ b/Report/M2Report.tex @@ -152,13 +152,10 @@ We will construct both categories $\CC$ and $\BB$ recursively, adding new sorts one by one. 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}. - The overall construction of the categories and of the adjunctions $F_i \vdash G_i$ is given below. + 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$. @@ -167,11 +164,14 @@ We construct the category $\CC_i$ as the following pair: \[ - \CC_i = (X : \CC_{i-1}) \times \Set^{\Hom(O_i,X)} \qquad\text{(this is a dependent coproduct)} + \CC_i = (X : \CC_{i-1}) \times \left(\Set\middle/\Hom(O_i,X)\right) \] - 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. + 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)}$} - For example, for our type theory example, we first have + 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 \[ O_1 = \star \in \operatorname{Obj}(\CC_0) = \operatorname{Obj}(1) \] @@ -291,13 +291,15 @@ 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(X,Y)$ is a functor $(X:C) \times (\Set/A(X)) \to \TSet$ with - \[\begin{array}{c} - \Hbar_A(X,Y)_\UU = A(X)\\ - \Hbar_A(X,Y)_\El = Y - \end{array}\] + 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. - \todo{Réference de comment on crée le foncteur, pourquoi c'en est un, si c'est utile ...} + \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} \[ @@ -753,3 +755,7 @@ + + + + diff --git a/Report/graphs/G1.json b/Report/graphs/G1.json index 9784b62..f1b3fbd 100644 --- a/Report/graphs/G1.json +++ b/Report/graphs/G1.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":13,"label":{"isPullshout":false,"label":"F_i","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":14,"label":{"isPullshout":false,"label":"G_i","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":0,"id":15,"label":{"isPullshout":false,"label":"R_{i-1}^i","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":16,"label":{"isPullshout":false,"label":"L_{i-1}^i","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":1,"id":17,"label":{"isPullshout":false,"label":"\\dash \\circ I_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":2,"id":18,"label":{"isPullshout":false,"label":"F_{i-1}","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":19,"label":{"isPullshout":false,"label":"G_{i-1}","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":20,"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":2,"id":21,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":22,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":5,"id":23,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":24,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":4,"id":25,"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":7},{"from":6,"id":26,"label":{"isPullshout":false,"label":"L_0^i","style":{"alignment":"right","bend":-0.6,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":0,"id":27,"label":{"isPullshout":false,"label":"R_0^i","style":{"alignment":"right","bend":0.9999999999999999,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":28,"label":{"isPullshout":false,"label":"\\lambda.\\star","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":29,"label":{"isPullshout":false,"label":"\\lambda.1","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":6}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\BB_i","pos":[195,61],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\left[S_i,\\Set\\right]","pos":[474,61],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\BB_{i-1}","pos":[195,225],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\left[S_{i-1},\\Set\\right]","pos":[474,225],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\vdots","pos":[474,328],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"\\vdots","pos":[195,328],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\BB_0 = \\TSet","pos":[195,431],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"\\left[\\emptyset,\\Set\\right] = 1","pos":[474,431],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"\\vdash","pos":[33,245.8125],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"\\vdash","pos":[195,160.8125],"zindex":0}},{"id":10,"label":{"isMath":true,"label":"\\bot","pos":[323,60.8125],"zindex":0}},{"id":11,"label":{"isMath":true,"label":"\\bot","pos":[327,223.8125],"zindex":0}},{"id":12,"label":{"isMath":true,"label":"\\bot","pos":[336,430.8125],"zindex":0}}],"sizeGrid":130,"title":"1"}]},"version":11} \ 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\\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":"F_i","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":8,"label":{"kind":"normal","label":"G_i","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":0,"id":9,"label":{"kind":"normal","label":"R_{i-1}^i","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":10,"label":{"kind":"normal","label":"L_{i-1}^i","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":2,"id":11,"label":{"kind":"normal","label":"F_{i-1}","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":12,"label":{"kind":"normal","label":"G_{i-1}","style":{"alignment":"right","bend":0.2,"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":"","style":{"alignment":"left","bend":0.2,"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":"","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":15,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0.2,"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":"","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":5,"id":17,"label":{"kind":"normal","label":"L_0^i","style":{"alignment":"right","bend":-0.5,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":0,"id":18,"label":{"kind":"normal","label":"R_0^i","style":{"alignment":"right","bend":0.7,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":19,"label":{"kind":"normal","label":"\\lambda.\\star","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":20,"label":{"kind":"normal","label":"\\lambda.1","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":18,"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":17},{"from":9,"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":10},{"from":7,"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":8},{"from":11,"id":24,"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":19,"id":25,"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":20},{"from":13,"id":26,"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":14},{"from":15,"id":27,"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":16}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\BB_i","pos":[195,61],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\CC_i","pos":[474,61],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\BB_{i-1}","pos":[195,225],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\CC_{i-1}","pos":[474,225],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\vdots","pos":[195,328],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"\\BB_0 = \\TSet","pos":[195,431],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\CC_0 = 1","pos":[474,431],"zindex":0}}],"sizeGrid":130,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/header.tex b/Report/header.tex index c0c8835..eb324ae 100644 --- a/Report/header.tex +++ b/Report/header.tex @@ -109,6 +109,7 @@ \newcommand\Ty{{\ensuremath{\operatorname{Ty}}}} \newcommand\Tm{{\ensuremath{\operatorname{Tm}}}} \newcommand\Cstr{{\ensuremath{\operatorname{\mathcal{C}str}}}} +\newcommand\Cat{{\ensuremath{\operatorname{\mathcal{C}at}}}} \newcommand\Set{{\ensuremath{\operatorname{\mathcal{S}et}}}} \newcommand\FamSet{{\ensuremath{\operatorname{\mathcal{F}am\mathcal{S}et}}}} \newcommand\Hom{{\ensuremath{\operatorname{\mathcal{H}om}}}}