% !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{GATs and 2-sortification}
	\begin{frame}{What is a GAT ?}
		\begin{itemize}
			\item A \textbf{list} of declarations
			\item[\ding{220}] Enables to declare sorts, objects of those sorts and 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}{ll}
				$A : \Set$&\multirow{2}{*}{$\left.\begin{array}{c}\\\\\end{array}\right\}\text{sorts}$}\\
				$B : \Set$&\\\hdashline
				$\operatorname{exec} : A \to B$&$\}\text{constructors}$
			\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}{.7\textwidth}
					\renewcommand\arraystretch{1.5}
					\begin{tabular}{ll}
						$A : \Set$ & \multirow{2}{*}{$\left.\begin{array}{c}\\\\\end{array}\right\}\text{sorts}$}\\
						$B : \Set$ &\\\hdashline
						$\operatorname{exec} : A \to B$ &\multirow{2}{*}{$\left.\begin{array}{c}\\\\\end{array}\right\}\text{constructors}$}\\
						$\operatorname{invexec} : B \to A$&\\\hdashline
						$\operatorname{isol} : (x : A) \to \operatorname{invexec}(\operatorname{exec}\;x) = x$&
						\multirow{2}{*}{$\left.\begin{array}{c}\\\\\end{array}\right\}\text{equalities}$}\\
						$\operatorname{isor} : (y : B) \to \operatorname{exec}(\operatorname{invexec}\;y) = y$&\\
					\end{tabular}
				\end{column}
				\begin{column}{.3\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$ \\\hdashline
				$\id : (A : \Obj) \to \Hom\;A\;A$ \\
				$\circ : (A\;B\;C:\Obj) \to \Hom\;B\;C \to\Hom\;A\;B \to \Hom\;A\;C$ \\\hdashline
				$\operatorname{idl}: (A B : \Obj) \to (\sigma : \Hom\;A\;B) \to \circ\;(\id\;B)\;\sigma = \sigma$\\
				$\operatorname{idr}: (A B : \Obj) \to (\sigma : \Hom\;A\;B) \to \circ\;\sigma\;(\id\;A) = \sigma$\\
				$\operatorname{\circ-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$ \\\hdashline
				$\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}{Subject of my internship}{2-sortification of GATs}
		\begin{center}
			{\large Transform a GAT into a GAT with only two sorts}
		\end{center}
		\vspace{3ex}
		
		\ding{229} Process observed since at least 2021
		
		\ding{229} Never formally studied
		
		\ding{229} Studying all GATs by only studying GATs with two sorts ?
	\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 : 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}{Categories of models}
		\begin{center}
			\renewcommand{\ULthickness}{2.4pt}
			\only<1>{GAT = sorts + constructors + equalities}
			\only<2>{GAT = \textbf{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 \\\hdashline
		\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}{Categories of Models}{of the original GAT}
		\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 the 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}{Category of Models}{of the transformed GAT}
		
		\begin{center}
			\color{blue}{
			\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}}$ & $\XCon_X :$ &
			\only<1>{$X_\UU$}
			\only<2>{$H_1F_0(X) \to X_\UU$} \\
			$\boxed{\Ty : (\Gamma : \underline{\Con}) \to \mathcal{O}}$ & $\XTy_X :$&
			\only<1>{$\left(\Gamma \in X_\El(\XCon_X)\right) \to X_\UU $}
			\only<2>{$H_2F_1(X,\XCon_X) \to X_\UU$} \\
			$\boxed{\Tm : (\Delta : \underline{\Con}) \to (A : \underline{\Ty\;\Delta}) \to \mathcal{O}}$ &
			$\XTm_X : $ &
			\only<1>{\rule[6ex]{0pt}{0pt}\renewcommand\arraystretch{0.9}$\begin{array}{c}\left(\Delta \in X_\El(\XCon_X)\right) \to\\ \left(A \in X_\El(\XTy_X(\Delta))\right) \to\\ X_\UU\end{array}$}
			\only<2>{$H_3F_2(X,\XCon_X,\XTy_X) \to X_\UU$}
		\end{tabular}
		\end{center}
		\pause
		\begin{center}
			\includesvg[scale=.4]{graphs/diagrammeFGmini.svg}
		\end{center}
	\end{frame}
	
	\begin{frame}{Constructing $F$ and $G$}
		
		\begin{center}
			\includesvg[scale=.4]{graphs/diagrammeFGmini.svg}
		\end{center}
		\[
		\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 & \XCon_X : X_\UU \\
			\left(Y_\Ty(\Gamma)\right)_{\Gamma \in Y_\Con} &
			\XTy_X : H_2 F_{1} (X,\XCon_X) \to X_\UU \\
			\left(\left(Y_\Tm(\Delta,A)\right)_{A \in Y_\Ty(\Delta)}\right)_{\Delta \in Y_\Con} &
			\XTm_X : H_3 F_{2} (X,\XCon_X,\XTy_X) \to X_\UU \\
		\end{array}
		\]
	\end{frame}
	
	\begin{frame}{Constructing $G_3$}
		\vspace{-2ex}
		\begin{columns}
			\begin{column}{.5\textwidth}
		\begin{center}
			\includesvg[scale=.4]{graphs/diagrammeGmini.svg}
		\end{center}
	\end{column}
	\begin{column}{.5\textwidth}
		\[
			Y = \left(Y_\Con,Y_\Ty,Y_\Tm\right)
		\]
	\end{column}
\end{columns}
		\vspace{.5ex}
		\only<1>{
		\[\begin{array}{ccl}
			X_\UU & = & \text{«sorts»}\\
			X_\El(o) & = & \text{«objects of sort $o$»}
		\end{array}\]
		}
		\pause
		\renewcommand{\arraystretch}{0.5}
		\[\begin{array}{ccccccccc}
			X_\UU & = &
			\{\star\} & \uplus &
			Y_\Con & \uplus&
			\displaystyle\coprod_{\Delta \in Y_\Con}Y_\Ty(\Delta) &
			\xrightarrow{X_\El}&\Set\\
			\pause
			&& \tikzmark{1}{\star} &&&&&&\tikzmark{2}{Y_\Con}\\
			X_\El & &
			&&\tikzmark{3}{\Gamma}&&&&\tikzmark{4}{Y_\Ty(\Gamma)}\\
			&&&&&& \tikzmark{5}{(\Delta,A)}&& \tikzmark{6}{Y_\Tm(\Delta,A)}\\
			
		\end{array}\]
		\begin{tikzpicture}[overlay,remember picture]
			\draw[|->] (1) to (2);
			\draw[|->] (3) to (4);
			\draw[|->] (5) to (6);
		\end{tikzpicture}
		\pause
		\begin{columns}
		\begin{column}{.5\textwidth}
		\[\begin{array}{lcl}
			\XCon_X &=& \star \in \{\star\}\\
			\XTy_X(\Gamma) &=& \Gamma \in Y_\Con \\
			\XTm_X(\Delta,A) &=& (\Delta,A) \in \displaystyle\coprod_{\Delta \in Y_\Con}Y_\Ty(\Delta)
		\end{array}\]
		\end{column}
		\pause
		\begin{column}{.5\textwidth}
		\begin{tcolorbox}
			All sorts of $X_\UU$ are in the image of some constructor $(\XCon_X,\XTy_X,\XTm_X)$
		\end{tcolorbox}
		\end{column}
		\end{columns}
	\end{frame}
	
	\begin{frame}{Constructing $F_3$}
		\begin{center}
			\includesvg[scale=.4]{graphs/diagrammeFmini.svg}
		\end{center}
		\vspace{-1ex}
		\renewcommand\arraystretch{1.5}
		\[
		\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} &\\
			\XCon_X : X_\UU & Y_\Con =
			\uncover<2->{\ensuremath{X_\El(\XCon_X)}}\\
			\XTy_X : H_2 F_{1} (X,\XCon_X) \to X_\UU &
			Y_\Ty(\Gamma) = 
			\uncover<3->{\ensuremath{X_\El(\XTy_X(\Gamma))}}\\
			\XTm_X : H_3 F_{2} (X,\XCon_X,\XTy_X) \to X_\UU &
			Y_\Tm(\Delta,A) =
			\uncover<4->{\ensuremath{X_\El(\XTm_X(\Delta,A))}} \\
		\end{array}
		\]
		\pause[5]
		\vspace{-.5ex}
		\begin{tcolorbox}
			The preimage by $X_\El$ of each object of $Y$ is a sort of $X_\UU$ constructed by some constructor
		\end{tcolorbox}
		
	\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}
			Morphisms of $\BB_3$ and $\CC_3$ both respect constructors
			\pause
			
			All sorts of $G_3Y_\UU$ are in the image of some constructor $(\XCon_{G_3Y},\XTy_{G_3Y},\XTm_{G_3Y})$
			
			\ding{220}$\Hom_{\BB_3}\left(G_3Y,X\right)$ morphisms are only defined on constructors
			
			\pause
			
			The preimage by $X_\El$ of each object of $F_3X$ is a sort of $X_\UU$ constructed by some constructor
			
			\ding{220}$\Hom_{\CC_3}\left(Y,F_3X\right)$ morphisms only send to constructible terms
		\end{remark}
	\end{frame}
	
	\section{Conclusion}
	
	\begin{frame}{Conclusion}
		\begin{center}
			\hspace{9.2ex}$\CC$ \hspace{3.7cm} $\BB$
			\vspace{.5cm}
			
			\includesvg[scale=.4]{graphs/diagrammeFG.svg}
		\end{center}
	\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}
	
	\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}
	
	\begin{frame}{Fibration of $\CC_i$}
		
	\end{frame}
	
	\begin{frame}{$S_i$ from syntax}
		
	\end{frame}
	
\end{document}