% !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}