465 lines
14 KiB
TeX
465 lines
14 KiB
TeX
% !TeX spellcheck = en_US
|
|
\DocumentMetadata{}
|
|
\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{GATs and 2-sortification}
|
|
\begin{frame}{What is a GAT ?}
|
|
\begin{itemize}
|
|
\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 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$
|
|
\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$ \\
|
|
$\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{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$ \\
|
|
$\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{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}
|
|
\begin{frame}{2-sortification}
|
|
\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}{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}
|
|
\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
|
|
|
|
\vspace{1ex}
|
|
{\large How to state this fact}
|
|
|
|
\ding{229} Semantical proof
|
|
|
|
\begin{center}
|
|
\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
|
|
|
|
\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{()}$ & $\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[4]
|
|
\[\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)
|
|
\]
|
|
\pause
|
|
\begin{center}
|
|
\begin{tabular}{ll}
|
|
$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$:& Sorts \\
|
|
$X_\El(o)$:& Objects of sort $o$\\
|
|
\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_\UU,X_\El)$ \\
|
|
$\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(\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>{\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}
|
|
\end{frame}
|
|
|
|
\begin{frame}{Constructing the functors}
|
|
\[
|
|
\begin{array}{l|l}
|
|
Y : \mathbf{\CC_3} & X : \mathbf{\BB_3} \\\hline
|
|
& 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 \\
|
|
\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$:& Sorts \\
|
|
$X_\El(o)$:& Objects of sort $o$\\
|
|
\end{tabular}
|
|
\end{center}
|
|
\end{frame}
|
|
|
|
\begin{frame}{Constructing $G_3$}
|
|
|
|
\only<1>{
|
|
\[\begin{array}{ccl}
|
|
X_\UU & = & \text{«sorts»}\\
|
|
X_\El(o) & = & \text{«objects of sort $o$»}
|
|
\end{array}\]
|
|
}
|
|
\pause
|
|
\[\begin{array}{ccccccc}
|
|
X_\UU & = &
|
|
1 & \oplus &
|
|
Y_\Con & \oplus&
|
|
\displaystyle\coprod_{\Delta \in Y_\Con}Y_\Ty(\Delta) \\
|
|
X_\El(\inj_1(\star)) & = &
|
|
Y_\Con &&&&\\
|
|
X_\El(\inj_2(\Gamma)) & = &
|
|
&&Y_\Ty(\Gamma) &&\\
|
|
X_\El(\inj_3(\Delta,A)) & = &
|
|
&&&& Y_\Tm(\Delta,A)\\
|
|
|
|
\end{array}\]
|
|
\pause
|
|
\[\begin{array}{lcl}
|
|
\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$}
|
|
|
|
\renewcommand\arraystretch{1.8}
|
|
\[
|
|
\begin{array}{l|l}
|
|
X : \mathbf{\BB_3} & Y = F_3(X): \mathbf{\CC_3}\\\hline
|
|
X_\UU : \Set\quad X_\El : \Set^{X_\UU} &\\
|
|
\Cstr_\Con : X_\UU & Y_\Con =
|
|
\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_\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_\El(\Cstr^X_\Tm(\Delta,A))}} \\
|
|
\end{array}
|
|
\]
|
|
\pause[5]
|
|
\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$
|
|
|
|
\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}
|
|
\end{frame}
|
|
|
|
\section{The complete proof \& Discoveries}
|
|
|
|
\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}
|
|
|
|
\begin{frame}{Fibration of $\CC_i$}
|
|
|
|
\end{frame}
|
|
|
|
\begin{frame}{$S_i$ from syntax}
|
|
|
|
\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}
|
|
|
|
\begin{frame}
|
|
\begin{center}
|
|
\Large Thank you for your attention
|
|
\end{center}
|
|
\end{frame}
|
|
|
|
\end{document}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|