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

Ajout d'une conclusion

Browse Source
This commit is contained in:
Samy Avrillon 2024-08-18 13:26:17 +02:00
parent d9c4e0e8b2
commit 0cdf37e75a
Signed by: Mysaa
GPG Key ID: 0220AC4A3D6A328B
1 changed files with 46 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

88
Report/M2Report.tex
View File

@ -1057,50 +1057,13 @@
\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)
\]
A morphism from $(X,\Cstr)$ to $(X', \Cstr')$ is a morphism from $X$ to $X'$ in $\TSet$ (i.e. a natural transformation $X \implies X'$) which makes the following diagram commute, for all $a$ in $S_{i-1}$.
\begin{center}
% YADE DIAGRAM BiMorphismDiagram.json
% GENERATED LATEX
\input{graphs/BiMorphismDiagram.tex}
% END OF GENERATED LATEX
\end{center}
Identities and compositions are that of the base category $\TSet$, and categorical equalities are trivially derived from the diagram above.
The diagram expresses as
\[
\forall \gamma \in \Hom_{G_{a-1}\Gamma_a,X}, \quad \Cstr'_a(f \circ \gamma) = f_\UU(\Cstr_a \gamma)
\]
\todo{Define properly the use of \this}
\subsection{$G$ and $F$ infinite constructions}
\[
G_i(Y) = \left(\sum_{a\in S_i}H_{Y(a)}\left(\lim_{(a/S_i)*}\overline{Y_a}\right), \lambda a.\lambda \eta.(a,u (\inj_2 \star))\right)
\]
where $u : \left(Y(a) \oplus 1, \inj_1\right) \to (\lim_{(a/S_i)*} \overline{Y_a})$
so that $\varphi_{b,f} u (\star) = \eta_\El^b(f)$
\[
F_i(X,\Cstr)(a) = X(p)^{-1}\left(\Cstr_a\left(\Hom_{\BB_{a-1}}(G_{a-1}\Gamma_a,X)\right)\right)
\]
\[
F_i(X,\Cstr)(f : a \to b)(X(p)(x); x \in \Cstr_a(\eta)) = \eta_\El^b(f)
\]
\todo{Show that those are the same functors as those defined recursively. Prove the adjunction/reflection infinitely ?}
\section{Summary}
\lipsum[1-3]
The initial goal of this internship was to study the transformation of GATs to GATs with only two sorts. We have only studied the transformation of sort specifications. We managed to give a formal construction of the semantics of any sort specification and of its transformation.
We have described a relation between both categories, which is an coreflection, i.e. an adjunction where the left adjoint is full and faithful. This adjunction allows us to build the initial model of the initial GAT from the initial model of the transformed GAT, so one can study properties of GATs with only two sorts and transpose them to any GATs.
There is still work to do in order to make the contents of this document apply to any GAT instead of only sort specifications. There is also ways of generalizing our formal construction to descriptions more general than GATs.
@ -1319,5 +1282,46 @@
% END OF GENERATED LATEX
\end{center}
\section{Misc}
\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)
\]
A morphism from $(X,\Cstr)$ to $(X', \Cstr')$ is a morphism from $X$ to $X'$ in $\TSet$ (i.e. a natural transformation $X \implies X'$) which makes the following diagram commute, for all $a$ in $S_{i-1}$.
\begin{center}
% YADE DIAGRAM BiMorphismDiagram.json
% GENERATED LATEX
\input{graphs/BiMorphismDiagram.tex}
% END OF GENERATED LATEX
\end{center}
Identities and compositions are that of the base category $\TSet$, and categorical equalities are trivially derived from the diagram above.
The diagram expresses as
\[
\forall \gamma \in \Hom_{G_{a-1}\Gamma_a,X}, \quad \Cstr'_a(f \circ \gamma) = f_\UU(\Cstr_a \gamma)
\]
\todo{Define properly the use of \this}
\subsection{$G$ and $F$ infinite constructions}
\[
G_i(Y) = \left(\sum_{a\in S_i}H_{Y(a)}\left(\lim_{(a/S_i)*}\overline{Y_a}\right), \lambda a.\lambda \eta.(a,u (\inj_2 \star))\right)
\]
where $u : \left(Y(a) \oplus 1, \inj_1\right) \to (\lim_{(a/S_i)*} \overline{Y_a})$
so that $\varphi_{b,f} u (\star) = \eta_\El^b(f)$
\[
F_i(X,\Cstr)(a) = X(p)^{-1}\left(\Cstr_a\left(\Hom_{\BB_{a-1}}(G_{a-1}\Gamma_a,X)\right)\right)
\]
\[
F_i(X,\Cstr)(f : a \to b)(X(p)(x); x \in \Cstr_a(\eta)) = \eta_\El^b(f)
\]
\todo{Show that those are the same functors as those defined recursively. Prove the adjunction/reflection infinitely ?}
\end{document}