From 84b61cc1bc53d00327f1fbb6ca57be7ed593ca76 Mon Sep 17 00:00:00 2001 From: Samy Avrillon Date: Fri, 30 Aug 2024 01:38:44 +0200 Subject: [PATCH] =?UTF-8?q?D=C3=A9but=20du=20diapo=20de=20soutenance?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Report/M2Diapo.tex | 261 +++++++++++++++++++++++++++++++++++++++++ Report/M2Report.tex | 4 + Report/header.tex | 8 +- Report/headerDiapo.tex | 186 +++++++++++++++++++++++++++++ 4 files changed, 453 insertions(+), 6 deletions(-) create mode 100644 Report/M2Diapo.tex create mode 100644 Report/headerDiapo.tex diff --git a/Report/M2Diapo.tex b/Report/M2Diapo.tex new file mode 100644 index 0000000..e3d6a63 --- /dev/null +++ b/Report/M2Diapo.tex @@ -0,0 +1,261 @@ +% !TeX spellcheck = en_US +\documentclass[12pt,xcolor={dvipsnames},aspectratio=169]{beamer} + +\input{./headerDiapo.tex} + +\title[Semantics of 2-sortification]{Categorical semantics of the reduction of GATs to two-sorted GATs. + \\[1ex] \large Notes on my 4.5-month internship at the LIX} +\hypersetup{pdftitle={Categorical semantics of the reduction of GATs to two-sorted GATs}} +\author[Samy Avrillon]{Samy Avrillon, supervised by + \\[1ex] Ambroise Lafont (LIX, Palaiseau, France)} +\date{} + +\begin{document} + + \begin{frame}[plain] + \maketitle + \end{frame} + + \section*{Table of contents} + \begin{frame}{Plan of the presentation} + \tableofcontents[hidesubsections] + \end{frame} + + \section{Introduction} + \subsection{What is a GAT ?} + \begin{frame}{What is a GAT ?} + \begin{itemize} + \item A syntactic object + \item Defines a set of models + \item 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} + \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}{2-sortification} + \renewcommand\arraystretch{1.5} + \begin{center} + \renewcommand\arraystretch{1.5} + \begin{tabular}{|c|c|} + \hline + $\mathcal{O} : \Set$ & + $\El : \mathcal{O} \to \Set$ \\\hline + \end{tabular} + \end{center} + + \todo{Cette partie} + \end{frame} + \begin{frame}{Category of Models \& Generalization} + \begin{tabular}{lcp{0.5\textwidth}} + $\boxed{\bullet}$ & $\CC_0 :=$ & + $\one$ \\ + $\boxed{\Con : \Set}$ & $\CC_1 := $& + \only<1>{$\left[X_\Con\right]$} + \only<2>{$\left[X_\Con : \Set\right]$} + \only<3>{$(\bullet : \CC_0) \times \left(\Set\right)$} + \only<4>{$\left(X : \CC_0\right) \times \Set^{H_1(X)}$} \\ + $\boxed{\Ty : (\Gamma : \Con) \to \Set}$ & $\CC_2 := $& + \only<1>{$\left[X_\Con, \left(X_\Ty(\Gamma)\right)_{\Gamma \in X_\Con}\right]$} + \only<2>{$\left[X_\Con : \Set, X_\Ty : \Set^{X_\Con}\right]$} + \only<3>{$\left(X_\Con : \CC_1\right) \times \left(\Set^{X_\Con}\right)$} + \only<4>{$\left(X : \CC_1\right) \times \Set^{H_2(X)}$} \\ + $\boxed{\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set}$ & $\CC_3 :=$& + \only<1>{$\left[X_\Con, \left(X_\Ty(\Gamma)\right)_{\Gamma \in X_\Con},\right.$} + \only<2>{$\left[X_\Con : \Set, X_\Ty : \Set^{X_\Con},\right.$} + \only<3>{$\left((X_\Con,X_\Ty) : \CC_2\right) \times$} + \only<4>{$\left(X : \CC_2\right) \times \Set^{H_3(X)}$} \\ && + \only<1>{$\left.\left(\left(X_\Tm(\Delta,A)\right)_{A \in \Ty(\Delta)}\right)_{\Delta \in X_\Con} \right]$} + \only<2>{\quad$\left.X_\Tm : \Set^{\prod_{\Delta:X_\Con}X_\Ty(\Delta)}\right]$} + \only<3>{\quad$\left(\Set^{\prod_{\Delta:X_\Con}X_\Ty(\Delta)}\right)$} + \end{tabular} + + \pause[3] + \[\begin{array}{rcl} + H_1(\bullet) &=& 1_\Set \\ + H_2(X_\Con) &=& X_\Con \\ + H_3(X_\Con,X_\Ty) &=& \displaystyle\prod_{\Delta:X_\Con}X_\Ty(\Delta) + \end{array}\] + \end{frame} + + \begin{frame}{Category of Models of transformed GAT} + \[ + \begin{array}{|c|} + \hline + \mathcal{O} : \Set \\ + \El : \mathcal{O} \to \Set \\ + \hline + \end{array} + \] + + \[ + \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} + \] + \pause + \begin{center} + \begin{tabular}{ll} + $X_\UU$:& Sortes \\ + $X_\El$:& Objets\\ + $X_p(x)$:& Sorte de l'objet \\ + \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 \\ + \end{tabular} + \end{center} + \begin{center} + \begin{tabular}{lrp{0.4\textwidth}} + $\boxed{\mathcal{O} : \Set\quad\El : \mathcal{O} \to \Set}$ & $\BB_0 =$ & + $X : \TSet$ \\ + $\boxed{\Con : \mathcal{O}}$ & $\Cstr_\Con :$ & + \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<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<2>{$H_3F_2(X,\Cstr_\Con,\Cstr_\Ty) \to X_\UU$} + \end{tabular} + \end{center} + \end{frame} + + \begin{frame}{Constructing the functors} + \[ + \begin{array}{l|l} + Y : \mathbf{\CC_3} & X : \mathbf{\BB_3} \\\hline + & X : \TSet\\ + 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 \\ + \left(\left(Y_\Tm(\Delta,A)\right)_{A \in Y_\Ty(\Delta)}\right)_{\Delta \in Y_\Con} & + \Cstr_\Tm : H_3 F_{2} (X,\Cstr_\Con,\Cstr_\Ty) \to X_\UU \\ + \end{array} + \] + + \begin{center} + \begin{tabular}{ll} + $X_\UU$:& Sortes \\ + $X_\El$:& Objets\\ + $X_p(x)$:& Sorte de l'objet \\ + \end{tabular} + \end{center} + \end{frame} + + \begin{frame}{Constructing $G_3$} + + \only<1>{ + \[\begin{array}{ccl} + X_\El & = & \text{«objets»}\\ + \labeledupdownarrow{p}&& \labeledupdownarrow{\text{«sorte de l'objet»}}\\ + X_\UU & = & \text{«sortes»} + \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) + \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) + \end{array}\] + \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 &\\ + \Cstr_\Con : X_\UU & Y_\Con = + \uncover<2->{\ensuremath{X_p^{-1}(\left\{\Cstr^X_\Con\right\}) \subseteq X_\El}}\\ + \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)\})}}\\ + \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))}} \\ + \end{array} + \] + \end{frame} + + +\end{document} + + + + + + + + + + diff --git a/Report/M2Report.tex b/Report/M2Report.tex index 28f83e7..092db5a 100644 --- a/Report/M2Report.tex +++ b/Report/M2Report.tex @@ -1,8 +1,12 @@ % !TeX spellcheck = en_US \documentclass[11pt,a4paper]{article} +\usepackage[textheight=0.75\paperheight,a4paper,margin=2cm]{geometry} + \input{./header.tex} +\usepackage{titling} + % po4a: environment remark % po4a: environment tikzpicture % po4a: environment property diff --git a/Report/header.tex b/Report/header.tex index 452152e..ee88d64 100644 --- a/Report/header.tex +++ b/Report/header.tex @@ -46,8 +46,6 @@ \usepackage[backend=biber,style=numeric]{biblatex} \usepackage{hyperref} -\usepackage[textheight=0.75\paperheight,a4paper,margin=2cm]{geometry} - \usepackage[lighttt]{lmodern} \usetikzlibrary{shapes.geometric,positioning,backgrounds} @@ -69,8 +67,6 @@ % Création des environnement globaux -\newtheorem{theorem}{Theorem} -\newtheorem{definition}{Definition} \newtheorem{property}{Property} \newtheorem{remark}{Remark} @@ -157,6 +153,8 @@ \newcommand\todo[1]{\begin{tcolorbox}[colback=red!20!white,colframe=red!85!black,boxrule=4pt] #1 \end{tcolorbox}} \newcommand\inlinetodo[1]{\colorbox{orange}{#1}} + + % Création des environnements spécifiques au document @@ -191,6 +189,4 @@ \fancyfoot[R]{\textbf{\thepage / \pageref{LastReportPage}}} \pagestyle{fancy} -\usepackage{titling} - \addbibresource{Bilibibio.bib} \ No newline at end of file diff --git a/Report/headerDiapo.tex b/Report/headerDiapo.tex new file mode 100644 index 0000000..6b33e18 --- /dev/null +++ b/Report/headerDiapo.tex @@ -0,0 +1,186 @@ +% Loading packages +\usepackage{fontspec} +\usepackage[utf8]{inputenc} +\usepackage{amsmath} +\usepackage{amssymb} +\usepackage{bbm} +\usepackage{stmaryrd} +\usepackage[english]{babel} +\usepackage{csquotes} +\usepackage{listings} +\usepackage{lstautogobble} +\usepackage{svg} +\usepackage{tikz} +\usepackage{multirow} +\usepackage{multicol} +\usepackage{tcolorbox} +\usepackage{mdframed} +\usepackage{proof} +\usepackage{xparse} +\usepackage{cprotect} +\usepackage{xpatch} +\usepackage{enumitem} +\usepackage{amsmath} +\usepackage{amsfonts} +\usepackage{mathtools} +\usepackage{txfonts} +\usepackage{yade} +\usepackage{environ} +\usepackage[backend=biber,style=numeric]{biblatex} +\usepackage{hyperref} +\usepackage{array} + +\usepackage[lighttt]{lmodern} +\usetikzlibrary{shapes.geometric,positioning,backgrounds} + +% Macros caractères globales +\newcommand{\pgrph}{\P} +\newcommand{\hsep}{\vspace{.2cm}\centerline{\rule{0.8\linewidth}{.05pt}}\vspace{.4cm}} +\renewcommand{\P}{\mathbb{P}} +\newcommand{\E}{\mathbb{E}} +\newcommand{\1}{\scalebox{1.2}{$\mathbbm{1}$}} +\newcommand{\floor}[1]{\left\lfloor#1\right\rfloor} +\newcommand{\littleO}{o} +\newcommand{\bigO}{\mathcal{O}} +\newcommand{\longdash}{\:\textrm{---}\:} +\newcommand\hole{\left[\raisebox{-0.25ex}{\scalebox{1.2}{$\cdot$}}\right]} +\newcommand\bracket[1]{\!\left[#1\right]} +\newcommand\spacebar{\;|\;} +\def\nDownarrow{\not\mspace{1mu}\Downarrow} +\let\pprec\preccurlyeq + +% Création des environnement globaux +\newtheorem{property}{Property} +\newtheorem{remark}{Remark} + +\newcounter{rule} + +% Commandes logiques globales +\newcommand{\ifnullthenelse}[3]{ + \ifnum\value{#1}=0 + #2 + \else + #3 + \fi +} + +%%% Commande \newtag permettant de changer le label d'une equation +\makeatletter +\newcommand\newtag[2]{#1\def\@currentlabel{#1}\label{#2}} +\makeatother + + +% Macros caractères spécifiques au document +\newfontface\russian{Liberation Serif} +\newcommand\BB{{\ensuremath{\mathcal{B}}}} +\newcommand\en{{\text{\russian н}}} +\newcommand\TT{{\ensuremath{\mathcal{T}}}} +\newcommand\UU{{\ensuremath{\mathcal{U}}}} +\newcommand\CC{{\ensuremath{\mathcal{C}}}} +\newcommand\El{{\ensuremath{\operatorname{\mathcal{E}l}}}} +\newcommand\ii{{\ensuremath{\mathbf{i}}}} +\newcommand\Con{{\ensuremath{\operatorname{Con}}}} +\newcommand\Ty{{\ensuremath{\operatorname{Ty}}}} +\newcommand\Tm{{\ensuremath{\operatorname{Tm}}}} +\newcommand\Cstr{{\ensuremath{\operatorname{\mathcal{C}str}}}} +\newcommand\Rtsc{{\ensuremath{\operatorname{\mathcal{R}tsc}}}} +\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\Hom{{\ensuremath{\operatorname{\mathcal{H}om}}}} +\newcommand\this{{\ensuremath{\operatorname{\texttt{this}}}}} +\newcommand\one{{\ensuremath{\mathbf{1}}}} +\newcommand\dash{{\;\textrm{---}\;}} +\renewcommand\enquote[1]{``#1''} +\newcommand\tl{{\triangleleft}} + +\DeclareMathOperator{\inj}{inj} +\DeclareMathOperator{\id}{id} +\DeclareMathOperator{\Id}{\mathcal{I}d} + +\newcommand\TSet{{\ensuremath{\left[\TT,\Set\right]}}} +\newcommand\TSetObject[3]{{\ensuremath{ + \left[ + \begin{tikzpicture}[baseline=(base)] + \node (U) at (0,0) {\UU}; + \node (El) at (0,1) {\El}; + \draw[->] (El) -- node[anchor=east] {\ensuremath{\scriptstyle p}} (U); + + \node (XU) at (1.5,0) {\ensuremath{#3}}; + \node (XEl) at (1.5,1) {\ensuremath{#1}}; + \draw[->] (XEl) -- node[anchor=west] {\ensuremath{\scriptstyle #2}} (XU); + + \draw[|->] (.3,0) -- (1,0); + \draw[|->] (.3,0.5) -- (1,0.5); + \draw[|->] (.3,1) -- (1,1); + + \coordinate (base) at (.5,.4); + \end{tikzpicture} + \right] +}}} + +\newcommand\simpleArrow[3]{ + \begin{tikzpicture} + \node (0) at (0,0) {$#1$}; + \node (1) at (6,0) {$#3$}; + \path[->] (0) edge["${\scriptstyle #2}$", pos=0.5, fore, black,=>, ] (1); + \end{tikzpicture} +} +\newcommand\simpleUpDownArrow[3]{ + \begin{tikzpicture} + \node (0) at (0,1) {$#1$}; + \node (1) at (0,0) {$#3$}; + \path[->] (0) edge["${\scriptstyle #2}$", pos=0.5, fore, black,=>, ] (1); + \end{tikzpicture} +} +\newcommand\labeledupdownarrow[1]{ + \begin{tikzpicture} + \path[->] (0,1) edge["${\scriptstyle #1}$", pos=0.5, fore, black,=>, ] (0,0); + \end{tikzpicture} +} + +\newcommand\diagram[1]{\begin{tcolorbox}\begin{center}\vspace{1.5cm}\Huge \texttt{\textbf{#1}}\vspace{1.5cm}\end{center}\end{tcolorbox}} + +\newcommand\todo[1]{\begin{tcolorbox}[colback=red!20!white,colframe=red!85!black,boxrule=4pt] #1 \end{tcolorbox}} +\newcommand\inlinetodo[1]{\colorbox{orange}{#1}} + +\newcommand{\backupbegin}{ + \newcounter{finalframe} + \setcounter{finalframe}{\value{framenumber}} +} +\newcommand{\backupend}{ + \setcounter{framenumber}{\value{finalframe}} +} + +\addbibresource{Bilibibio.bib} + +\usetheme{Madrid} + +\makeatletter +\setbeamertemplate{frametitle}{% + \nointerlineskip + \begin{beamercolorbox}[sep=1.6ex,wd=\paperwidth,leftskip=.5cm,rightskip=0cm]{frametitle}% + \usebeamerfont{frametitle}\usebeamercolor[fg]{frametitle}\beamer@frametitle\\ + \usebeamerfont{framesubtitle}\usebeamercolor[fg]{framesubtitle}\insertframesubtitle + \end{beamercolorbox}% +} +\makeatother + +\hypersetup{pdfpagemode=FullScreen} +% Transition en fade-in par défaut +\addtobeamertemplate{background canvas}{\transfade[duration=0.4]}{} + +\addtobeamertemplate{frametitle}{ + \let\insertframetitle\insertsubsectionhead}{} +\makeatletter +\CheckCommand*\beamer@checkframetitle{\@ifnextchar\bgroup\beamer@inlineframetitle{}} +\renewcommand*\beamer@checkframetitle{\global\let\beamer@frametitle\relax\@ifnextchar\bgroup\beamer@inlineframetitle{}} +\makeatother + +\setbeamertemplate{itemizeitem}{\scriptsize$\diamond$} +\newcommand\sectocframe[1][]{ + \begin{frame} + \pdfpcnote{#1} + \tableofcontents[currentsection,hideothersubsections,sections=\value{section}] + \end{frame} +} \ No newline at end of file