diff --git a/Report/.gitignore b/Report/.gitignore index 62c66b2..c32ddf4 100644 --- a/Report/.gitignore +++ b/Report/.gitignore @@ -1,2 +1,3 @@ .build/ graphs/*.tex +svg-inkscape diff --git a/Report/M2Diapo.tex b/Report/M2Diapo.tex index b5a747b..eb0b3fa 100644 --- a/Report/M2Diapo.tex +++ b/Report/M2Diapo.tex @@ -1,4 +1,5 @@ % !TeX spellcheck = en_US +\DocumentMetadata{} \documentclass[12pt,xcolor={dvipsnames},aspectratio=169]{beamer} \input{./headerDiapo.tex} @@ -21,67 +22,119 @@ \tableofcontents[hidesubsections] \end{frame} - \section{Introduction} - \subsection{What is a GAT ?} + \section{GATs and 2-sortification} \begin{frame}{What is a GAT ?} \begin{itemize} - \item A syntactic object - \item Defines a set of models - \item Defines a category of models + \item A dependent \textbf{type theory} + \item[\ding{220}] Enables to create sorts, object of those sorts, equalities between those objects + \item A \textbf{syntactic object} + \item[\ding{220}] Type judgements are defined with induction rules + \item Describes \textbf{models} + \item[\ding{220}] Defines a category of models \end{itemize} \end{frame} - \begin{frame}{A GAT for Type Theory} - \renewcommand\to{{\;\rightarrow\;}} - \begin{center} - \renewcommand\arraystretch{1.5} - \begin{tabular}{|c|c|c|} - \hline - $\Con : \Set$ & - $\Ty : (\Gamma : \Con) \to \Set$ & - $\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set$ \\\hline - \end{tabular} - \end{center} - \pause - \begin{columns} - \begin{column}{0.60\textwidth} - \begin{center} - \begin{tcolorbox}[boxsep=-5pt] - \renewcommand\arraystretch{1.25} - \begin{tabular}{l} - $\triangleright: (\Gamma:\Con)\to(A:\Ty\;\Gamma)\to\Con$ \\ - $\diamond: \Con$ \\ - $\operatorname{var} : (\Gamma:\Con) \to (A:\Ty\;\Gamma) \to \Tm\;(\Gamma\triangleright A)\;A$ \\ - $\implies : (\Gamma:\Con) \to \Ty\;\Gamma \to \Ty\;\Gamma \to \Ty\;\Gamma$ \\ - $\operatorname{app} : (\Gamma : \Con) \to (A\;B :\Ty\;\Gamma) \to$\\ - \qquad$\Tm\;\Gamma\;(A\implies B)\to\Tm\;\Gamma\; A \to \Tm\;\Gamma\; B$ - \end{tabular} + + + \begin{frame}{A GAT for a function in Set} + \begin{tcolorbox} + \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$\\ + \end{tabular} \end{tcolorbox} - \end{center} - \end{column} - \begin{column}{0.4\textwidth} - \[\begin{array}{c} - \Gamma : \Con\\ - A,B : \Ty\;\Gamma\\ - t : \Tm (\Gamma \triangleright (A \implies B)) A\\ - {\mathbf{\top}}\\ - \operatorname{app}\;\operatorname{var}\;t : \Tm\;(\Gamma\triangleright(A\implies B))\;A - \end{array}\] - \end{column} - \end{columns} + \end{frame} + + \begin{frame}{A GAT for a small category} + \begin{tcolorbox} + \renewcommand\arraystretch{1.5} + \begin{tabular}{l} + $\Obj : \Set$ \\ + $\Hom : \Obj \to \Obj \to \Set$ \\\hline + $\id : (A : \Obj) \to \Hom\;A\;A$ \\ + $\operatorname{comp} : (A\;B\;C:\Obj) \to \Hom\;B\;C \to\Hom\;A\;B \to \Hom\;A\;C$ \\\hline + $\operatorname{idl}: (A B : \Obj) \to (\sigma : \Hom\;A\;B) \to \operatorname{comp} (\id\;B) \sigma = \sigma$\\ + $\operatorname{idr}: (A B : \Obj) \to (\sigma : \Hom\;A\;B) \to \operatorname{comp} \sigma (\id\;A) = \sigma$\\ + $\operatorname{comp-trans}: \dots$\\ + \end{tabular} + \end{tcolorbox} + \end{frame} + + \begin{frame}{A GAT for Type Theory} + \begin{tcolorbox} + \renewcommand\arraystretch{1.5} + \begin{tabular}{l} + $\Con : \Set$ \\ + $\Ty : \Con \to \Set$ \\ + $\Tm : (\Gamma : \Con) \to \Ty\;\Gamma \to \Set$ \\\hline + $\operatorname{empty}: \Con$ \\ + $\operatorname{ext}: (\Gamma:\Con)\to(A:\Ty\;\Gamma)\to\Con$ \\ + $\operatorname{implies} : (\Gamma:\Con) \to \Ty\;\Gamma \to \Ty\;\Gamma \to \Ty\;\Gamma$ \\ + $\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{tcolorbox} + \end{frame} \begin{frame}{2-sortification} - \renewcommand\arraystretch{1.5} \begin{center} + {\large Transform a GAT into a GAT with only two sorts} + + \ding{229} Simplify a study of GATs + \end{center} + \end{frame} + \begin{frame}{2-sortification of the Set Function GAT} + \begin{tcolorbox} \renewcommand\arraystretch{1.5} - \begin{tabular}{|c|c|} - \hline - $\mathcal{O} : \Set$ & - $\El : \mathcal{O} \to \Set$ \\\hline + \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$ & \end{tabular} + \end{tcolorbox} + \end{frame} + \begin{frame}{2-sortification of Type Theory GAT} + \begin{tcolorbox} + \renewcommand\arraystretch{1.4} + \begin{tabular}{l} + $\mathcal{O} : \Set$ \\ + $\El : \mathcal{O} \to \Set$ \pause\\\hline + $\Con : \mathcal{O}$ \\ + $\Ty : \El\;\Con \to \mathcal{O}$ \\ + $\Tm : (\Gamma : \El\;\Con) \to \El\;(\Ty\;\Gamma) \to \mathcal{O}$ \\ + $\operatorname{empty}: \El\;\Con$ \\ + $\operatorname{ext}: (\Gamma:\El\;\Con)\to(A:\El\;(\Ty\;\Gamma))\to\El\;\Con$ \\ + $\operatorname{implies} : (\Gamma:\El\;\Con) \to \El\;(\Ty\;\Gamma) \to \El\;(\Ty\;\Gamma) \to \El\;(\Ty\;\Gamma)$ + \end{tabular} + \end{tcolorbox} + \end{frame} + \begin{frame}{Goal of the internship}{} + + {\large Is this transformation correct ?} + + \ding{229} Can one study all GATs by studying only GATs with two sorts + + {\large How to state this fact} + + \ding{229} Semantical proof + + \begin{center} + \includesvg[scale=.4]{graphs/diagrammeFG.svg} \end{center} - \todo{Cette partie} + \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} + \end{frame} + + \section{One Example} + \begin{frame}{Category of Models \& Generalization} \begin{tabular}{lcp{0.5\textwidth}} $\boxed{\bullet}$ & $\CC_0 :=$ & @@ -126,30 +179,24 @@ \[ \BB_0 := \left(X_\UU : \Set, X_\El : \Set^{X_\UU}\right) - \uncover<2->{\ensuremath{\simeq \left(X_\UU : \Set, X_\El : \Set/X_\UU\right)}} - \uncover<3->{\ensuremath{\equiv \TSet}} - \] - \pause - \[ - \TT := \simpleUpDownArrow{El}{p}{\UU} + {\color{PineGreen}\ensuremath{\simeq \left(X_\UU : \Set, X_\El : \Set/X_\UU\right)}} \] \pause \begin{center} \begin{tabular}{ll} - $X_\UU$:& Sortes \\ - $X_\El$:& Objets\\ - $X_p(x)$:& Sorte de l'objet \\ + $X_\UU$:& Sorts \\ + $X_\El(o)$:& Objects of sort $o$\\ \end{tabular} \end{center} \end{frame} \begin{frame}{Adding transformed sort declarations} + \begin{center} \begin{tabular}{ll} - $X_\UU$:& Sortes \\ - $X_\El$:& Objets\\ - $X_p(x)$:& Sorte de l'objet \\ + $X_\UU$:& Sorts \\ + $X_\El(o)$:& Objects of sort $o$\\ \end{tabular} \end{center} \begin{center} @@ -160,10 +207,10 @@ \only<1>{$X_\UU$} \only<2>{$H_1F_0(X) \to X_\UU$} \\ $\boxed{\Ty : (\Gamma : \underline{\Con}) \to \mathcal{O}}$ & $\Cstr_\Ty :$& - \only<1>{$\left(\Gamma \in X_\El\middle|X_p(\Gamma) = \Cstr_\Con\right) \to X_\UU $} + \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\middle|X_p(\Delta) = \Cstr_\Con\right) \to\\ \left(A \in X_\El\middle|X_p(A) = \Cstr_\Ty(\Delta)\right) \to\\ X_\UU\end{array}$} + \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<2>{$H_3F_2(X,\Cstr_\Con,\Cstr_\Ty) \to X_\UU$} \end{tabular} \end{center} @@ -173,7 +220,7 @@ \[ \begin{array}{l|l} Y : \mathbf{\CC_3} & X : \mathbf{\BB_3} \\\hline - & X : \TSet\\ + & X_\UU : \Set \quad X_\El : \Set^{X_\UU}\\ Y_\Con : \Set & \Cstr_\Con : X_\UU \\ \left(Y_\Ty(\Gamma)\right)_{\Gamma \in Y_\Con} & \Cstr_\Ty : H_2 F_{1} (X,\Cstr_\Con) \to X_\UU \\ @@ -184,9 +231,8 @@ \begin{center} \begin{tabular}{ll} - $X_\UU$:& Sortes \\ - $X_\El$:& Objets\\ - $X_p(x)$:& Sorte de l'objet \\ + $X_\UU$:& Sorts \\ + $X_\El(o)$:& Objects of sort $o$\\ \end{tabular} \end{center} \end{frame} @@ -195,65 +241,78 @@ \only<1>{ \[\begin{array}{ccl} - X_\El & = & \text{«objets»}\\ - \labeledupdownarrow{p}&& \labeledupdownarrow{\text{«sorte de l'objet»}}\\ - X_\UU & = & \text{«sortes»} + X_\UU & = & \text{«sorts»}\\ + X_\El(o) & = & \text{«objects of sort $o$»} \end{array}\] } \pause \[\begin{array}{ccccccc} - - X_\El & = & - Y_\Con & \oplus & - \displaystyle\coprod_{\Gamma \in Y_\Con}Y_\Ty(\Gamma) & \oplus & - \displaystyle\coprod_{\Delta \in Y_\Con}\coprod_{A \in Y_\Ty(\Delta)}Y_\Ty(\Delta,A)\\ - \labeledupdownarrow{p}&&\labeledupdownarrow{}&&\labeledupdownarrow{\operatorname{proj}_1}&&\labeledupdownarrow{\operatorname{proj}_{2,1}}\\ X_\UU & = & 1 & \oplus & Y_\Con & \oplus& - \displaystyle\coprod_{\Delta \in Y_\Con}Y_\Ty(\Delta) + \displaystyle\coprod_{\Delta \in Y_\Con}Y_\Ty(\Delta) \\ + X_\El(\inj_1(\star)) & = & + Y_\Con &&&&\\ + X_\El(\inj_2(\Gamma)) & = & + &&\displaystyle\coprod_{\Gamma \in Y_\Con}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)\\ + \end{array}\] \pause \[\begin{array}{lcl} - \Cstr^X_\Con &=& \inj_1(\star)\\ - \Cstr^X_\Ty(\Gamma) &=& \inj_2(\Gamma) \\ - \Cstr^X_\Tm(\Delta,A) &=& \inj_3(\Delta,A) + \Cstr_\Con &=& \inj_1(\star)\\ + \Cstr_\Ty(\Gamma) &=& \inj_2(\Gamma) \\ + \Cstr_\Tm(\Delta,A) &=& \inj_3(\Delta,A) \end{array}\] + \pause + \begin{remark} + All sorts of $X_\UU$ are reached by some $\Cstr$ + \end{remark} \end{frame} \begin{frame}{Constructing $F_3$} - \begin{center} - \begin{tabular}{ll} - $X_\UU$:& Sortes \\ - $X_\El$:& Objets\\ - $X_p(x)$:& Sorte de l'objet \\ - \end{tabular} - \end{center} \renewcommand\arraystretch{1.8} \[ \begin{array}{l|l} X : \mathbf{\BB_3} & Y = F_3(X): \mathbf{\CC_3}\\\hline - X : \TSet &\\ + X_\UU : \Set\quad X_\El : \Set^{X_\UU} &\\ \Cstr_\Con : X_\UU & Y_\Con = - \uncover<2->{\ensuremath{X_p^{-1}(\left\{\Cstr^X_\Con\right\}) \subseteq X_\El}}\\ + \uncover<2->{\ensuremath{X_\El(\Cstr^X_\Con)}}\\ \Cstr_\Ty : H_2 F_{1} (X,\Cstr_\Con) \to X_\UU & Y_\Ty(\Gamma) = - \uncover<3->{\ensuremath{X_p^{-1}(\{\Cstr^X_\Ty(\Gamma)\})}}\\ + \uncover<3->{\ensuremath{X_\El(\Cstr^X_\Ty(\Gamma))}}\\ \Cstr_\Tm : H_3 F_{2} (X,\Cstr_\Con,\Cstr_\Ty) \to X_\UU & Y_\Tm(\Delta,A) = - \uncover<4->{\ensuremath{X_p^{-1}(\Cstr^X_\Tm(\Delta,A))}} \\ + \uncover<4->{\ensuremath{X_\El(\Cstr^X_\Tm(\Delta,A))}} \\ \end{array} \] + \pause[4] + \begin{remark} + Each object of $Y$ are associated by $X_\El$ to some $\Cstr$ + \end{remark} + \end{frame} \begin{frame}{Adjunction $F \vdash G$} + \[ + \Hom_{\BB_3}\left(G_3Y,X\right) \simeq \Hom_{\CC_3}\left(Y,F_3X\right) + \] + \pause + \begin{remark} + All sorts of $G_3Y$ are reached by some $\Cstr$ of $G_3Y$ + + Each object of $F_3X$ are associated by $X_\El$ to some $\Cstr$ of $X$ + \end{remark} + \pause + \begin{property} + $FG \cong \Id$ + \end{property} \end{frame} - \begin{frame}{$FG \cong \Id$} - - \end{frame} + \section{The complete proof \& Discoveries} \begin{frame}{Structure of the proof} \begin{itemize} @@ -280,13 +339,15 @@ \end{frame} + \section{Conclusion} + \begin{frame}{Conclusion} \end{frame} \begin{frame}{Future work} \begin{itemize} - \item Complete GAT + \item Complete GAT (term constructors + equalities) \item Proof Assistant Formalization \item $S_i$ non-direct \end{itemize} @@ -303,3 +364,5 @@ + + diff --git a/Report/diapoNotes.md b/Report/diapoNotes.md new file mode 100644 index 0000000..a038074 --- /dev/null +++ b/Report/diapoNotes.md @@ -0,0 +1,71 @@ +# M2 Presentation + +### Introduction slide +Notes on my internship + +### Plan of the presentation +First present what is the subject of my study, and what i tried to achieve. + +The whole proof is too formal and complex: Informally prove one specific example. + +Then, i will present the «structure» of the global proof, and show some things discovered along the way + +## GAT and 2-sortification +### What is a GAT + +### A GAT for a function in set +A GAT can be composed of three kinds of lines: +- Sort declarations +- Objects costructors +A model is the data of a function from a set to another set i.e. a triple the data of two sets, and a «mapping» between them +We can spice up this GAT: Gat of isomorphic functions. +- Equalities + +### A GAT for a category +Another example of GATs: +A category is the data of ...... with ...... such that ...... + +### A GAT for Type Theory +Last example that of type theory +-> a lot to add, contructors, equalities ..., just for the example. + +### 2-sortification +Known process +Used by Sestini +Can simplify a study of GATs to only GATs of two sorts + +### 2-sortification of the Set function GAT +Sort specification is always the same. O will describe «sorts» and El will describe «objects of that sort» + +Then, we replace Set occuneces by O and we prefix everything else by El + +### 2-sortification of the Type Theoyr GAT + +### Goal of the internship + +## One Example +### Category of Models & Generalization + +### Category of models of the Transformed GAT + +### Adding transformed sort declarations + +### Constructing the functors + +### Contsructing G3 + +### Constructing F3 + +### Adjunction FG + +## The complete proof & Discoveries +### Structure of the proof + +### Fibration of C + +### S from syntax + +## Conclusion +### Conclusion + +### Future work diff --git a/Report/graphs/diagrammeFG.svg b/Report/graphs/diagrammeFG.svg new file mode 100644 index 0000000..d1af201 --- /dev/null +++ b/Report/graphs/diagrammeFG.svg @@ -0,0 +1,375 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Report/headerDiapo.tex b/Report/headerDiapo.tex index 6b33e18..02cf5f2 100644 --- a/Report/headerDiapo.tex +++ b/Report/headerDiapo.tex @@ -19,13 +19,14 @@ \usepackage{xparse} \usepackage{cprotect} \usepackage{xpatch} -\usepackage{enumitem} \usepackage{amsmath} \usepackage{amsfonts} \usepackage{mathtools} \usepackage{txfonts} \usepackage{yade} \usepackage{environ} +\usepackage{pifont} +\usepackage{transparent} \usepackage[backend=biber,style=numeric]{biblatex} \usepackage{hyperref} \usepackage{array} @@ -87,6 +88,7 @@ \newcommand\Cat{{\ensuremath{\operatorname{\mathcal{C}at}}}} \newcommand\Set{{\ensuremath{\operatorname{\mathcal{S}et}}}} \newcommand\FamSet{{\ensuremath{\operatorname{\mathcal{F}am\mathcal{S}et}}}} +\newcommand\Obj{{\ensuremath{\operatorname{\mathcal{O}bj}}}} \newcommand\Hom{{\ensuremath{\operatorname{\mathcal{H}om}}}} \newcommand\this{{\ensuremath{\operatorname{\texttt{this}}}}} \newcommand\one{{\ensuremath{\mathbf{1}}}} diff --git a/Report/yade-config.json b/Report/yade-config.json index 1d0252d..b177de1 100644 --- a/Report/yade-config.json +++ b/Report/yade-config.json @@ -1,5 +1,5 @@ { - "watchedFile": "M2Report.tex", + "watchedFile": "M2Diapo.tex", "baseDir": "graphs", "externalOutput": true, "preambleFile": "yade-preamble.tex"