From c36520f1a3cb8f7306173147b80a555016139242 Mon Sep 17 00:00:00 2001 From: Samy Avrillon Date: Tue, 3 Sep 2024 08:47:52 +0200 Subject: [PATCH] Correction d'erreurs --- Report/M2Diapo.tex | 166 ++++++++++++++++++++++++++++++++--------- Report/headerDiapo.tex | 1 + 2 files changed, 132 insertions(+), 35 deletions(-) diff --git a/Report/M2Diapo.tex b/Report/M2Diapo.tex index eb0b3fa..176384e 100644 --- a/Report/M2Diapo.tex +++ b/Report/M2Diapo.tex @@ -37,21 +37,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 +92,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 +117,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 +144,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 +175,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 +184,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 +271,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 +291,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 +302,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 +346,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 +380,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 +396,28 @@ \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} - \begin{frame}{Structure of the proof} + \begin{frame}{Structure of the global proof} \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$ + \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 $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 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} @@ -353,6 +443,12 @@ \end{itemize} \end{frame} + \begin{frame} + \begin{center} + \Large Thank you for your attention + \end{center} + \end{frame} + \end{document} diff --git a/Report/headerDiapo.tex b/Report/headerDiapo.tex index 02cf5f2..263a04c 100644 --- a/Report/headerDiapo.tex +++ b/Report/headerDiapo.tex @@ -27,6 +27,7 @@ \usepackage{environ} \usepackage{pifont} \usepackage{transparent} +\usepackage{ulem} \usepackage[backend=biber,style=numeric]{biblatex} \usepackage{hyperref} \usepackage{array}