Mysaa/M2Internship
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

More paragraphs

Browse Source
This commit is contained in:
Samy Avrillon 2024-07-18 15:35:28 +02:00
parent e9da8a9107
commit a779d3ed7f
Signed by: Mysaa
GPG Key ID: 0220AC4A3D6A328B
3 changed files with 21 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
Report/M2Report.tex
View File

@ -152,13 +152,10 @@
We will construct both categories $\CC$ and $\BB$ recursively, adding new sorts one by one. 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 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} \begin{center}
% YADE DIAGRAM G1.json % YADE DIAGRAM G1.json
% GENERATED LATEX
\input{graphs/G1.tex}
% END OF GENERATED LATEX
\end{center} \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$. 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: 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) 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) 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 Where $\Hbar_A$ is a functor $(X:C) \times (\Set/A(X)) \to \TSet$ defined as
\[\begin{array}{c} \[
\Hbar_A(X,Y)_\UU = A(X)\\ \Hbar_X(X,(Y,f)) = \TSetObject{Y}{f}{A(X)}
\Hbar_A(X,Y)_\El = Y \]
\end{array}\] 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} With $\widetilde{\inj_2}$ being defined by \inlinetodo{Changer les noms des hypothèses H3' et H1r}
\[ \[
@ -753,3 +755,7 @@

2
Report/graphs/G1.json
View File

File diff suppressed because one or more lines are too long

1
Report/header.tex
View File

@ -109,6 +109,7 @@
\newcommand\Ty{{\ensuremath{\operatorname{Ty}}}} \newcommand\Ty{{\ensuremath{\operatorname{Ty}}}}
\newcommand\Tm{{\ensuremath{\operatorname{Tm}}}} \newcommand\Tm{{\ensuremath{\operatorname{Tm}}}}
\newcommand\Cstr{{\ensuremath{\operatorname{\mathcal{C}str}}}} \newcommand\Cstr{{\ensuremath{\operatorname{\mathcal{C}str}}}}
\newcommand\Cat{{\ensuremath{\operatorname{\mathcal{C}at}}}}
\newcommand\Set{{\ensuremath{\operatorname{\mathcal{S}et}}}} \newcommand\Set{{\ensuremath{\operatorname{\mathcal{S}et}}}}
\newcommand\FamSet{{\ensuremath{\operatorname{\mathcal{F}am\mathcal{S}et}}}} \newcommand\FamSet{{\ensuremath{\operatorname{\mathcal{F}am\mathcal{S}et}}}}
\newcommand\Hom{{\ensuremath{\operatorname{\mathcal{H}om}}}} \newcommand\Hom{{\ensuremath{\operatorname{\mathcal{H}om}}}}