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

Compare commits

base: Mysaa:4c7b5b604e3e76d4a0dc62bfa70493da0ec9bbeb
Branches Tags
Mysaa:master
..
compare: Mysaa:a7df1d8369103a006346ad66b416b573fd23cda6
Branches Tags
Mysaa:master

2 Commits
4c7b5b604e ... a7df1d8369

Author SHA1 Message Date
Samy Avrillon
a7df1d8369
Suppression des slides superfules 2024-09-03 11:35:58 +02:00
Samy Avrillon
c36520f1a3
Correction d'erreurs 2024-09-03 08:47:52 +02:00
2 changed files with 174 additions and 57 deletions
Show Stats Expand all files Collapse all files

228
Report/M2Diapo.tex
View File

@ -17,11 +17,6 @@
\maketitle
\end{frame}
\section*{Table of contents}
\begin{frame}{Plan of the presentation}
\tableofcontents[hidesubsections]
\end{frame}
\section{GATs and 2-sortification}
\begin{frame}{What is a GAT ?}
\begin{itemize}
@ -37,21 +32,51 @@
\begin{frame}{A GAT for a function in Set}
\begin{tcolorbox}
\begin{columns}
\begin{column}{.6\textwidth}
\renewcommand\arraystretch{1.5}
\begin{tabular}{l}
$A : \Set$ \\
$B : \Set$ \\\hline
$\operatorname{exec} : A \to B$ \\
\pause
$\operatorname{invexec} : B \to A$\\\hline
$\operatorname{isol} : (x : A) \to \operatorname{invexec}(\operatorname{exec}\;x) = x$\\
$\operatorname{isor} : (y : B) \to \operatorname{exec}(\operatorname{invexec}\;y) = y$\\
$\operatorname{exec} : A \to B$
\end{tabular}
\end{column}
\begin{column}{.4\textwidth}
Models:
triples (A,B,f)
\end{column}
\end{columns}
\end{tcolorbox}
\end{frame}
\begin{frame}{A GAT for an bijective function in Set}
\begin{tcolorbox}
\begin{columns}
\begin{column}{.6\textwidth}
\renewcommand\arraystretch{1.5}
\begin{tabular}{l}
$A : \Set$ \\
$B : \Set$ \\\hline
$\operatorname{exec} : A \to B$ \\
$\operatorname{invexec} : B \to A$\\\hline
$\operatorname{isol} : (x : A) \to \operatorname{invexec}(\operatorname{exec}\;x) = x$\\
$\operatorname{isor} : (y : B) \to \operatorname{exec}(\operatorname{invexec}\;y) = y$\\
\end{tabular}
\end{column}
\begin{column}{.4\textwidth}
Models:
triples (A,B,f)
s.t. f is bijective
\end{column}
\end{columns}
\end{tcolorbox}
\end{frame}
\begin{frame}{A GAT for a small category}
\begin{tcolorbox}
\begin{columns}
\begin{column}{0.8\textwidth}
\renewcommand\arraystretch{1.5}
\begin{tabular}{l}
$\Obj : \Set$ \\
@ -62,11 +87,20 @@
$\operatorname{idr}: (A B : \Obj) \to (\sigma : \Hom\;A\;B) \to \operatorname{comp} \sigma (\id\;A) = \sigma$\\
$\operatorname{comp-trans}: \dots$\\
\end{tabular}
\end{column}
\begin{column}{0.2\textwidth}
Models:
small categories
\end{column}
\end{columns}
\end{tcolorbox}
\end{frame}
\begin{frame}{A GAT for Type Theory}
\begin{tcolorbox}
\begin{columns}
\begin{column}{0.7\textwidth}
\renewcommand\arraystretch{1.5}
\begin{tabular}{l}
$\Con : \Set$ \\
@ -78,6 +112,20 @@
$\operatorname{app} : (\Gamma : \Con) \to (A\;B :\Ty\;\Gamma) \to$\\
\qquad$\Tm\;\Gamma\;(\operatorname{implies}\;A\;B)\to\Tm\;\Gamma\; A \to \Tm\;\Gamma\; B$
\end{tabular}
\end{column}
\begin{column}{0.3\textwidth}
Models : Triples
$(X_\Con,X_\Ty,X_\Tm)$
with constructors
$\operatorname{empty} \in X_\Con$
\qquad\vdots
\end{column}
\end{columns}
\end{tcolorbox}
\end{frame}
@ -91,12 +139,13 @@
\begin{frame}{2-sortification of the Set Function GAT}
\begin{tcolorbox}
\renewcommand\arraystretch{1.5}
\begin{tabular}{ll}
$\mathcal{O} : \Set$ & \color{RoyalBlue} \text{sorts} \\
$\El : \mathcal{O} \to \Set$ & \color{RoyalBlue}\text{objects of that sort} \pause\\\hline
$A : \mathcal{O}$ &\\
$B : \mathcal{O}$ &\\
$\operatorname{exec} : \El\;A \to \El\;B$ &
\begin{tabular}{llrcl}
\pause
$\mathcal{O} : \Set$ & \color{RoyalBlue} \text{sorts} & $o:\mathcal{O}$ &$\leftrightarrow$&$o$ is a sort \\
$\El : \mathcal{O} \to \Set$ & \color{RoyalBlue}\text{objects of that sort} & \qquad $x : \El\;o$ & $\leftrightarrow$ & $x : \mathcal{O}$ \pause\\\hline
$A : \mathcal{O}$ &&\multicolumn{1}{l}{\color{teal}$A : \Set$}&&\\
$B : \mathcal{O}$ &&\multicolumn{1}{l}{\color{teal}$B : \Set$}&&\\
$\operatorname{exec} : \El\;A \to \El\;B$&&\color{teal}$\operatorname{exec} : A \to B$&&
\end{tabular}
\end{tcolorbox}
\end{frame}
@ -121,6 +170,7 @@
\ding{229} Can one study all GATs by studying only GATs with two sorts
\vspace{1ex}
{\large How to state this fact}
\ding{229} Semantical proof
@ -129,15 +179,52 @@
\includesvg[scale=.4]{graphs/diagrammeFG.svg}
\end{center}
\ding{229} This adjunction proves that one can make the initial model of any GAT from the initial model of the transformed GAT\inlinetodo{Ptet trop pointu}
\ding{229} This adjunction proves that one can make the initial model of any GAT from the initial model of the transformed GAT
\end{frame}
\section{One Example}
\begin{frame}{Constructing the categories}
\begin{center}
\only<1>{GAT = sorts + constructors + equalities}
\only<2>{GAT = sorts + \sout{constructors} + \sout{equalities}}
\end{center}
\pause[2]
\begin{center}
\begin{tabular}{|l|l|}
\hline
$\begin{array}{l}
\Con : \Set \\
\Ty : \Con \to \Set \\
\Tm : (\Gamma : \Con) \to \Ty\;\Gamma \to \Set
\end{array}$
&
$\begin{array}{l}
\mathcal{O} : \Set\\
\El : \mathcal{O} \to \Set \\\hline
\underline{\Con} : \mathcal{O} \\
\underline{\Ty} : \El\;\underline{\Con} \to \mathcal{O} \\
\underline{\Tm} : (\Gamma : \El\;\underline{\Con}) \to \El(\underline{\Ty}\;\Gamma) \to \mathcal{O}
\end{array}$\\\hline\rule{0pt}{1.0\normalbaselineskip}
\only<2>{$\CC \hookrightarrow (\Con,\Ty,\Tm)$}
\only<3->{$\CC_0 \hookrightarrow ()$}
&
\only<2>{$\BB \hookrightarrow (\mathcal{O},\El,\underline{\Con},\underline{\Ty},\underline{\Tm})$}
\only<3->{$\BB_0 \hookrightarrow (\mathcal{O},\El)$}\\
\uncover<3->{$\CC_1 \hookrightarrow (\Con)$} &
\uncover<3->{$\BB_1 \hookrightarrow (\mathcal{O},\El,\underline{\Con})$}\\
\uncover<3->{$\CC_2 \hookrightarrow (\Con,\Ty)$} &
\uncover<3->{$\BB_2 \hookrightarrow (\mathcal{O},\El,\underline{\Con},\underline{\Ty})$}\\
\uncover<3->{$\CC_3 \hookrightarrow (\Con,\Ty,\Tm)$} &
\uncover<3->{$\BB_3 \hookrightarrow (\mathcal{O},\El,\underline{\Con},\underline{\Ty},\underline{\Tm})$}\\\hline
\end{tabular}
\end{center}
\end{frame}
\begin{frame}{Category of Models \& Generalization}
\begin{tabular}{lcp{0.5\textwidth}}
$\boxed{\bullet}$ & $\CC_0 :=$ &
$\boxed{()}$ & $\CC_0 :=$ &
$\one$ \\
$\boxed{\Con : \Set}$ & $\CC_1 := $&
\only<1>{$\left[X_\Con\right]$}
@ -179,7 +266,6 @@
\[
\BB_0 := \left(X_\UU : \Set, X_\El : \Set^{X_\UU}\right)
{\color{PineGreen}\ensuremath{\simeq \left(X_\UU : \Set, X_\El : \Set/X_\UU\right)}}
\]
\pause
\begin{center}
@ -200,9 +286,10 @@
\end{tabular}
\end{center}
\begin{center}
\renewcommand\arraystretch{1.4}
\begin{tabular}{lrp{0.4\textwidth}}
$\boxed{\mathcal{O} : \Set\quad\El : \mathcal{O} \to \Set}$ & $\BB_0 =$ &
$X : \TSet$ \\
$(X_\UU,X_\El)$ \\
$\boxed{\Con : \mathcal{O}}$ & $\Cstr_\Con :$ &
\only<1>{$X_\UU$}
\only<2>{$H_1F_0(X) \to X_\UU$} \\
@ -210,7 +297,7 @@
\only<1>{$\left(\Gamma \in X_\El(\Cstr_\Con)\right) \to X_\UU $}
\only<2>{$H_2F_1(X,\Cstr_\Con) \to X_\UU$} \\
$\boxed{\Tm : (\Delta : \underline{\Con}) \to (A : \underline{\Ty\;\Delta}) \to \mathcal{O}}$ & $\Cstr_\Tm : $ &
\only<1>{$\begin{array}{c}\left(\Delta \in X_\El(\Cstr_\Con)\right) \to\\ \left(A \in X_\El(\Cstr_\Ty(\Delta))\right) \to\\ X_\UU\end{array}$}
\only<1>{\rule[6ex]{0pt}{0pt}\renewcommand\arraystretch{0.9}$\begin{array}{c}\left(\Delta \in X_\El(\Cstr_\Con)\right) \to\\ \left(A \in X_\El(\Cstr_\Ty(\Delta))\right) \to\\ X_\UU\end{array}$}
\only<2>{$H_3F_2(X,\Cstr_\Con,\Cstr_\Ty) \to X_\UU$}
\end{tabular}
\end{center}
@ -254,9 +341,9 @@
X_\El(\inj_1(\star)) & = &
Y_\Con &&&&\\
X_\El(\inj_2(\Gamma)) & = &
&&\displaystyle\coprod_{\Gamma \in Y_\Con}Y_\Ty(\Gamma) &&\\
&&Y_\Ty(\Gamma) &&\\
X_\El(\inj_3(\Delta,A)) & = &
&&&& \displaystyle\coprod_{\Delta \in Y_\Con}\coprod_{A \in Y_\Ty(\Delta)}Y_\Ty(\Delta,A)\\
&&&& Y_\Tm(\Delta,A)\\
\end{array}\]
\pause
@ -288,7 +375,7 @@
\uncover<4->{\ensuremath{X_\El(\Cstr^X_\Tm(\Delta,A))}} \\
\end{array}
\]
\pause[4]
\pause[5]
\begin{remark}
Each object of $Y$ are associated by $X_\El$ to some $\Cstr$
\end{remark}
@ -304,30 +391,73 @@
\begin{remark}
All sorts of $G_3Y$ are reached by some $\Cstr$ of $G_3Y$
\uncover<3>{\ding{220}$\Hom_{\BB_3}\left(G_3Y,X\right)$ transforms constructible into constructible}
Each object of $F_3X$ are associated by $X_\El$ to some $\Cstr$ of $X$
\uncover<3>{\ding{220}$\Hom_{\CC_3}\left(Y,F_3X\right)$ transforms constructible into constructible}
\end{remark}
\pause
\begin{property}
$FG \cong \Id$
\end{property}
\end{frame}
\section{The complete proof \& Discoveries}
\section{Conclusion}
\begin{frame}{Structure of the proof}
\begin{frame}{Conclusion}
\begin{center}
\hspace{2ex}$\CC$ \hspace{3.5cm} $\BB$
\vspace{.5cm}
\includesvg[scale=.4]{graphs/diagrammeFG.svg}
\end{center}
\end{frame}
\begin{frame}{Future work}
\begin{itemize}
\item $\CC_i$
\item $\BB_i$
\item $R_{i-1}^i : \BB_i \to \BB_{i-1}$
$R_0^i : \BB_i \to \BB_0$
\item $\tl^i : \BB_i \times \BB_0 \to \BB_i$
$\inj_1^i : X \to X \tl^i Y$
$\inj_2^i : Y \to R_0^i(X \tl^i Y)$
\item $F_i : \BB_i \to \CC_i : G_i$
\item $F_i \vdash G_i$
\item $F_iG_i \cong \Id_{\CC_i}$
$F_i\inj_1^i$
\item $(R_{i-1}^i X) \tl^{i-1} Y \to R_{i-1}^i (X \tl^i Y)$
\item Complete GAT (term constructors + equalities)
\item Proof Assistant Formalization
\item $S_i$ non-direct
\end{itemize}
\end{frame}
\begin{frame}
\begin{center}
\Large Thank you for your attention
\end{center}
\end{frame}
\appendix
\begin{frame}
\[\begin{array}{lcl}
F_3G_3(Y)_\Con &=& G_3(Y)_p^{-1}(\{\Cstr^{G_3(Y)}_\Con\})\\
&=& G_3(Y)_p^{-1}(\{\inj_1 \star\}) \\
&=& Y_\Con
\end{array}\]
and
\[\begin{array}{lcl}
F_3G_3(Y)_\Ty(\Gamma) &=& G_3(Y)_p^{-1}(\{\Cstr^{G_3(Y)}_\Ty(\Gamma)\})\\
&=& G_3(Y)_p^{-1}(\{\inj_2 \Gamma\}) \\
&=& \operatorname{proj}_1^{-1}(\Gamma) \\
&=& \left\{(\Gamma',A) \in \coprod_{\Gamma' \in Y_\Con}Y_\Ty(\Gamma') \middle| \Gamma' = \Gamma\right\}\\
&\simeq& Y_\Ty(\Gamma)
\end{array}\]
and finally, with the same method, we get that
\[
F_3G_3(Y)_\Tm(\Delta,A) \simeq Y_\Tm(\Delta,A)
\]
\end{frame}
\begin{frame}{Structure of the global proof}
\begin{itemize}
\item Categories $\CC_i$ \quad $\BB_i$
\item Functors $F_i : \BB_i \to \CC_i : G_i$
\item Adjunction $F_i \vdash G_i$
\item Forgetful functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$
\item Operator $\tl^i : \BB_i \times \BB_0 \to \BB_i$ \quad
$\inj_1^i : X \to X \tl^i Y$ \quad
$\inj_2^i : Y \to R_0^i(X \tl^i Y)$
\item Coreflection $F_iG_i \cong \Id_{\CC_i}$
\item Isomorphism $F_i\inj_1^i$
\item Isomorphism $(R_{i-1}^i X) \tl^{i-1} Y \to R_{i-1}^i (X \tl^i Y)$
\end{itemize}
\end{frame}
@ -339,20 +469,6 @@
\end{frame}
\section{Conclusion}
\begin{frame}{Conclusion}
\end{frame}
\begin{frame}{Future work}
\begin{itemize}
\item Complete GAT (term constructors + equalities)
\item Proof Assistant Formalization
\item $S_i$ non-direct
\end{itemize}
\end{frame}
\end{document}

3
Report/headerDiapo.tex
View File

@ -27,6 +27,7 @@
\usepackage{environ}
\usepackage{pifont}
\usepackage{transparent}
\usepackage{ulem}
\usepackage[backend=biber,style=numeric]{biblatex}
\usepackage{hyperref}
\usepackage{array}
@ -170,7 +171,7 @@
\hypersetup{pdfpagemode=FullScreen}
% Transition en fade-in par défaut
\addtobeamertemplate{background canvas}{\transfade[duration=0.4]}{}
%\addtobeamertemplate{background canvas}{\transfade[duration=0.4]}{}
\addtobeamertemplate{frametitle}{
\let\insertframetitle\insertsubsectionhead}{}