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

Potypos

Browse Source
This commit is contained in:
Samy Avrillon 2024-08-18 19:52:55 +02:00
parent 1d0860712e
commit 1019ac6702
Signed by: Mysaa
GPG Key ID: 0220AC4A3D6A328B
1 changed files with 8 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
Report/M2Report.tex
View File

@ -27,7 +27,7 @@
\subsection*{General Context} \subsection*{General Context}
Generalized Algebraic Theories a.k.a. GATs are synctaxic objects introduced in 1986 by Cartmell \cite{CartmellGATs}. They enable us to describe algebraic structures that we can see as a generalization of Type Theory's inductive types. For example, we can describe the models of some type theory using a GAT. Generalized Algebraic Theories a.k.a. GATs are syntactic objects introduced in 1986 by Cartmell \cite{CartmellGATs}. They enable us to describe algebraic structures that we can see as a generalization of Type Theory's inductive types. For example, we can describe the models of some type theory using a GAT.
A GAT is made of a list of \enquote{sorts} that describes sets, usually followed by a list of \enquote{constructors}. A GAT is made of a list of \enquote{sorts} that describes sets, usually followed by a list of \enquote{constructors}.
@ -47,7 +47,7 @@
\subsection*{Summary and Future Work} \subsection*{Summary and Future Work}
We formalised semantically this transformation, enabling us to be more general and to avoid the syntactical aspects of GATs. We formalized semantically this transformation, enabling us to be more general and to avoid the syntactical aspects of GATs.
This transformation has been proven, so that studying only GATs with two sorts can be done without loosing generality. This transformation has been proven, so that studying only GATs with two sorts can be done without loosing generality.
A next step could be to add term constructors to our formalization. We could describe their transformation and adapt the properties we stated for sort specification to them. A next step could be to add term constructors to our formalization. We could describe their transformation and adapt the properties we stated for sort specification to them.
@ -82,7 +82,7 @@
\end{tabular} \end{tabular}
\vspace{1em} \vspace{1em}
A sort specification therefore specifies the differents families of sets contained in a model, and how they relate to each other in terms of indexing. A sort specification therefore specifies the different families of sets contained in a model, and how they relate to each other in terms of indexing.
\paragraph{Term specification} \paragraph{Term specification}
Once we have a sort specification, we can add constructors to it in order to make a complete GAT. Constructors are composed of parameters (the same kind as for sort declarations) and of a codomain which is a sort defined by a previous sort declaration. Those constructors specify elements of the sets contained in the model. Once we have a sort specification, we can add constructors to it in order to make a complete GAT. Constructors are composed of parameters (the same kind as for sort declarations) and of a codomain which is a sort defined by a previous sort declaration. Those constructors specify elements of the sets contained in the model.
@ -204,7 +204,7 @@
% END OF GENERATED LATEX % END OF GENERATED LATEX
\end{center} \end{center}
This category is equivalent to the catgegory $\FamSet$ with an equivalence we will see later (\autoref{SetXSetXEquivalence}) This category is equivalent to the category $\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 With this formalisation, a model of this sort specification is a functor $X : \TT \to \Set$, such that
\begin{itemize} \begin{itemize}
@ -613,7 +613,7 @@
A(x) := f^{-1}(\{x\}) = \text{the preimage by f of the singleton $\{x\}$} A(x) := f^{-1}(\{x\}) = \text{the preimage by f of the singleton $\{x\}$}
\] \]
Conversly, a familiy of sets $A : X \to \Set$ is transformed into the following object of $\Set/X$ Conversely, a family of sets $A : X \to \Set$ is transformed into the following object of $\Set/X$
\begin{center} \begin{center}
% YADE DIAGRAM EquivSetXSetX.json % YADE DIAGRAM EquivSetXSetX.json
% GENERATED LATEX % GENERATED LATEX
@ -675,7 +675,7 @@
\label{sec:constructingCategory} \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 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 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}. 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 Altenkirch 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. We suppose that those $H_i$ functors are given.
\subsubsection{Constructing $\CC_i$} \subsubsection{Constructing $\CC_i$}
@ -686,7 +686,7 @@
\] \]
and where $H_i$ is the specific functor described above. 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)}$. This way of constructing the category has formerly been described by Altenkirch and al. \cite{Altenkirch2018}, with the only difference of the equivalence $\Set/H_i(X) \simeq \Set^{H_i(X)}$.
\subsubsection{Constructing $\BB_i$} \subsubsection{Constructing $\BB_i$}
@ -911,7 +911,7 @@
\subsection{Fibration of the category $\CC_i$} \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}. In the formal proof, we defined $\CC_i$ as an inductive Grothendieck construction as in Altenkirch and al. papers \cite{Altenkirch2018}.
But there is an other way \cite{Fiore2008} of building the category $\CC_i$ which is equivalent to the one presented above. But there is an other way \cite{Fiore2008} of building the category $\CC_i$ which is equivalent to the one presented above.
@ -924,11 +924,6 @@
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$. 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$.
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
\]
The final category is simply $S = \bigcup S_i$. The final category is simply $S = \bigcup S_i$.
In our type theory example, the category $S$ is constructed as follows: In our type theory example, the category $S$ is constructed as follows: