% !TeX spellcheck = en_US
\documentclass[10pt,a4paper]{article}

\input{./header.tex}

\title{Categorical semantics of the reduction of GATs to two-sorted GATs.
	\\[1ex] \large Notes on my 4.5-month internship at the Laboratoire d'Informatique de l'École Polytechnique (Palaiseau, France)}
\hypersetup{pdftitle={Categorical semantics of the reduction of GATs to two-sorted GATs}}
\author{Samy Avrillon, supervised by
	\\[1ex] Ambroise Lafont (LIX, Palaiseau, France)}

\begin{document}
	\doparttoc
	\maketitle
	
	\hsep
	
	\tableofcontents
	
	\newpage
	
	\section{Introduction}
		
		\lipsum[7-9]
		
	\section{Content}
	
	
	\subsection{Infinite construction of $\BB_i$}
		\[
			\BB_i := \left(X : \TSet, \Cstr : (a : S_{i-1}) \to \Hom_{\BB_{a-1}}(G_{a-1}\Gamma_a,R_{a-1}^i(\this)) \to X(\UU)\right)
		\]
		A morphism from $(X,\Cstr)$ to $(X', \Cstr')$ is a morphism from $X$ to $X'$ in $\TSet$ (i.e. a natural transformation $X \implies X'$) which makes the following diagram commute, for all $a$ in $S_{i-1}$.
		
		\diagram{D1}
		
		Identities and compositions are that of the base category $\TSet$, and categorical equalities are trivially derived from the diagram above.
		
		The diagram expresses as
		\[
			\forall \gamma \in \Hom_{G_{a-1}\Gamma_a,X}, \quad \Cstr'_a(f \circ \gamma) = f_\UU(\Cstr_a \gamma)
		\]
		
		\todo{Define properly the use of \this}
		
	\subsection{$H$ functors}
	
		For every object $X$ of a locally small category $C$, we define the functor $H_X : (X/\Set) \to \TSet$
		\[
			H_X(Y,f) = \TSetObject{X}{f}{Y}
		\]
		
		Dually, we make another functor $\Hbar_X : (\Set/X) \to \TSet$
		\[
			\Hbar_X(Y,f) = \TSetObject{Y}{f}{X}
		\]
		
		The morphisms translate as-is, and composition and identity relies on that of $(X/\Set)$ or $(\Set/X)$.
		
		\todo{(small) Show that it is actually a functor (should be trivial), potentially add a diagram}
		
	\subsection{$G$ and $F$ infinite constructions}
	
		\[
			G_i(Y) = \left(\sum_{a\in S_i}H_{Y(a)}\left(\lim_{(a/S_i)*}\overline{Y_a}\right), λa.λ\eta.(a,u (\inj_2 \star))\right)
		\]
		
		where $u : \left(Y(a) \oplus 1, \inj_1\right) \to (\lim_{(a/S_i)*} \overline{Y_a})$
		
		so that $\varphi_{b,f} u (\star) = \eta_\El^b(f)$
		
		\[
			F_i(X,\Cstr)(a) = X(p)^{-1}\left(\Cstr_a\left(\Hom_{\BB_{a-1}}(G_{a-1}\Gamma_a,X)\right)\right)
		\]
		\[
			F_i(X,\Cstr)(f : a \to b)(X(p)(x); x \in \Cstr_a(\eta)) = \eta_\El^b(f)
		\]
		
	\subsection{Hypohesis}
		
		\begin{property}[H3]
			\[
				F_i(X \oplus L_0^i Y) \cong F_i X
			\]
		\end{property}
		
		\todo{Do we need to specify that the adjunction is (rtl) $F(inj_1^i)$ ? And prove it ?}
		
		\begin{property}[H3']
			\[
				\Hom(G_i\Gamma, X) \cong \Hom(G_i\Gamma,X \oplus L_0^i Y)
			\]
			With left to right isomorphism being $(inj_1^i \circ \dash)$
		\end{property}
		
		\begin{property}[H1]
			\[
				R_{i-1}^i(X \oplus_i L_0^i Y) \cong R_{i-1}^i X \oplus L_0^{i-1} Y
			\]
		\end{property}
		
		\begin{property}[H1r]
			\[
				R_{0}^i(X \oplus_i L_0^i Y) \cong R_{0}^i X \oplus_{i-1} L_0^{i-1} Y
			\]
			We use the sum that makes this equivalence to be an equality.
		\end{property}
		
	\subsection{Notations}
		\[
			R_i^j = R_{i}^{i+1} \circ R_{i+1}^j = R_{i}^{j-1} \circ R_{j-1}^{j} = R_{i}^{i+1} \circ ... \circ R_{j-1}^{j}
		\]
		\[
			L_i^j = L_{j-1}^{j} \circ L_{i}^{j-1} = L_{i+1}^{j} \circ L_{i}^{i+1} = L_{j-1}^{j} \circ ... \circ L_{i}^{i+1}
		\]
		
		In any category with a coproduct, for every morphisms $f : X \to Z$ and $g : Y \to Z$, we denote with $\{f;g\}$ the unique morphism from $X \oplus Y$ to $Z$ such that $\{f;g\} \circ \inj_1 = f$ and $\{f;g\} \circ \inj_2 = g$.	
	\subsection{Recursive definition of $\BB_i$}
		
		\[
			\BB_i := \left(X : \BB_{i-1}, \Cstr_i : \Hom_{\BB_{i-1}} (G_{i-1}\Gamma_i,X) \to (R_0^{i-1}X)_\UU \right)
		\]
		
		A morphism $(X,\Cstr_i) \to (X',\Cstr'_i)$ is a morphism $f : X \to X'$ in $\BB_{i-1}$ such that the following diagram commutes.
		
		\diagram{D1 $[a \mapsfrom i]$} 
		
		Identities and compositions are that of the category $\BB_{i-1}$, and categorical equalities are trivially derived from the diagram above.
		
	\subsection{W definition}
	
		We define a functor $W : \displaystyle\prod_{X : \BB_{i-1}} (\Set/\Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,X)) \to \BB_{i}$
		
		\[
			W(X,Y) := \left(X \oplus L_0^{i-1} \Hbar_{\Hom(G_{i-1}\Gamma_i,\dash)}(X,Y), \widetilde{\inj_2} \right)
		\]
		
		With $\widetilde{\inj_2}$ being defined by
		\[
		\begin{array}{lcl}
			\Hom(G_{i-1}\Gamma_i,X \oplus L_0^{i-1} \Hbar_\bullet(X,Y)) & \to^{\text{H3'}} & \Hom(G_{i-1}\Gamma_i,X)\\
			& = & \Hbar_\bullet(X,Y)_\UU \\
			& \to^{\inj_2^0} &  \left(R_0^{i-1}X \oplus \Hbar_\bullet(X,Y)\right)_\UU \\
			& \to^{\text{H1r}} & \left(R_0^{i-1}(X \oplus L_0^{i-1}\Hbar_\bullet(X,Y))\right)_\UU
		\end{array}
		\]
		
		The action on a morphism $(g,h)$ from $(X,Y)$ to $(X',Y')$ is the following:
		\[
			W(g,h) := \left(g \oplus L_0^{i-1} \Hbar_{\Hom(G_{i-1}\Gamma_i,\dash)}(g,h)\right)
		\]
		
		It is indeed a morphism from $\BB_{i}$ as it makes the following diagram commute.
		
		\diagram{D2}
		
	\subsection{E definition}
		
		We define $E : \BB_{i} \to \displaystyle\prod_{X : \BB_{i-1}} (\Set/\Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,X))$
		
		\[
			E(X) = (R_{i-1}^i X, (A,h))
		\]
		Where $(A,h)$ is defined as the following pullback:
		
		\diagram{D3a}
		
		The action on a morphism $f$ from $X$ to $X'$ is defined as $E(f) = (R_{i-1}^i f, !)$, with $!$ being the only morphism making the following diagram commute:
		
		\diagram{D3b}
		
	\subsection{W E adjunction}
		
		We have an adjunction $W \dashv E$.
		
		Let $(X,Y)$ be in $\displaystyle\prod_{X : \BB_{i-1}} (\Set/\Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,X))$ and $Z$ be in $\BB_i$.
		
		We will construct a natural isomorphism.
		\[
			\phi_{XYZ} : \Hom(W(X,Y),Z) \to \Hom((X,Y),E(Z))
		\]
		
		\subsubsection{Constructing $\phi_{XYZ}$}
		Let $f$ be in $\Hom(W(X,Y),Z)$.
		We want to construct $\phi_{XYZ}(f) : (X,Y) \to E(Z)$.
		
		The first component of $\phi_{XYZ}(f)$ is $R_{i-1}^i f \circ inj_1^{i-1} : X \to R_{i-1}^i Z$, with $R_{i-1}^i f$ being a morphism of $\BB_{i-1}$ from $R_{i-1}^i(W(X,Y)) = X \oplus_{i-1} L_0^{i-1}$ to $R_{i-1}^i Z$.
		
		The second component is defined through the universal property of the pullback defined by $E(Z)$ according to the following diagram:
		
		\diagram{D6}
		
		\subsubsection{Constructing $\phi^{-1}_{XYZ}$}
		
		Now, we take $(g,h)$ a morphism from $(X,Y)$ to $E(Z)$.
		
		We define $\phi^{-1}_{XYZ}(g,h)$ as a morphism of $\BB_i$ from $W(X,Y)$ to $Z$, i.e. a morphism of $\BB_{i-1}$ from $X \oplus_{i-1} L_0^{i-1} \Hbar (X,Y)$ to $R_0^{i-1}(Z)$ that makes a certain diagram commute:
		\[
			\phi^{-1}_{XYZ}(g,h) = \left\{g ; \eta_0^i \circ L_0^{i-1} \square \right\}
		\]
		
		Where $\square$ is a morphism $\Hbar (X,Y) \to R_0^i Z$ defined by the following diagram:
		
		\diagram{D7}
		
		
		This is indeed a morphism of $\BB_i$ from $W(X,Y)$ to $Z$ as it makes the following diagram commute
		
		\diagram{D8}
		
		We now have to show that $\phi_{XYZ}$ and $\phi_{XYZ}^{-1}$ do make a natural isomorphism.
		
		\subsubsection{Composition $\phi_{XYZ} \circ \phi_{XYZ}^{-1}$}
		
		The first component of $\phi_{XYZ} (\phi_{XYZ}^{-1}(g,h))$ is
		\[
			R_{i-1}^i(\left\{g ; \eta_0^i \circ L_0^{i-1} \square \right\}) \circ \inj_1^{i-1} = \left\{g ; \eta_0^i \circ L_0^{i-1} \square \right\} \circ \inj_1^{i-1} = g
		\]
		
		The second component of $\phi_{XYZ} (\phi_{XYZ}^{-1}(g,h))$ follows the following diagram
		
		\diagram{D9}
		
		The diagram commutes as the following equality holds:
		\[
			\left(\left\{g ; \eta_0^i \circ L_0^{i-1} \square \right\} \circ \inj^{i-1}_2\right)_\El = \left(\eta_0^i \circ L_0^{i-1} \square\right)_\El = (\eta_0^i)_\El \circ (L_0^{i-1} \square)_\El = \square_El = \pi_1 \circ h
		\]
		
		\todo{Justify $(\eta_0^i)_\El = id_{\BB_i}$ and $(L_0^i(f))_\El = f_\El$}
		
		So, as the square is a pullback, we get the complete equality
		\[
			\phi_{XYZ} (\phi_{XYZ}^{-1}(g,h)) = (g,h)
		\]
		
		\subsubsection{Composition $\phi_{XYZ}^{-1} \circ \phi_{XYZ}$}
		
		Now, the converse composition is
		
		\[
			 \phi_{XYZ}^{-1} (\phi_{XYZ}(f)) = \left\{R_{i-1}^i f \circ \inj_1^{i-1} ; \eta_0^i \circ L_0^{i-1} \square \right\}
		\]
		where $\square$ follows the following diagram
		
		\diagram{D10}
		
		We want to show that $\phi_{XYZ}^{-1} (\phi_{XYZ}(f))$. By definition of $\{;\}$ in $\BB_1$, it suffices to show that $\eta_0^i \circ L_0^{i-1} \square = R_{i-1}^i f \circ \inj_1^{i-1}$.
		
		So it suffices to show that
		\[
			\square = R_0^{i-1}(R_{i-1}^i f \circ \inj_2^{i-1}) \circ \varepsilon_0^{i-1} = R_0^i f \circ \left(R_0^{i-1} \inj_2^{i-1} \circ \varepsilon_0^{i-1}\right) = R_0^i f \circ \inj_2^0
		\]
		
		The two required equalities are proved by the diagram above:
		
		\begin{align*}
			\square_\El = \left(R_0^i f \circ \inj_2^0\right)_\El \\
			\square_\UU = \left(R_0^i f \circ \inj_2^0\right)_\UU
		\end{align*}
		
		\todo{Expliciter à un endroit que $\Cstr^{W(X,Y)} = inj_2^\Set \circ \left(\inj_1^{i-1} \circ \dash\right)$ (déduit de la définition et de la forme de l'iso H3' et H1r=id)}
		
		\todo{Show $R_0^{i-1} \inj_2^{i-1} \circ \varepsilon_0^{i-1} = \inj_2^0$}
		
		\subsubsection{Naturality}
		
		We want to show that the following diagram commutes, for any objects $X$,$Y$,$Z$,$X'$,$Y'$,$Z'$ and morphisms $f$,$g$,$h$.
		
		\diagram{D10.0}
		
		We take a morphism $\ii$ in $\Hom\left(W(X,Y),Z\right)$. We want to show that it is sent by the above diagram to the same morphism of $\Hom\left((X,Y),E(Z)\right)$.
		
		We first look at the first component of the result morphism.
		
		\[\begin{array}{rcl}
			\phi_{XYZ}(f \circ \ii \circ W(g,h))_1
			&=& R_{i-1}^i\left(f \circ \ii \circ (g \oplus L_0^{i-1} \Hbar(g,h))^+\right) \circ \inj_1^{i-1} \\
			&=& R_{i-1}^i f \circ R_{i-1}^i \ii \circ \left\{\inj_1^{i-1} \circ g; \dots\right\} \circ \inj_1^{i-1} \\
			&=& R_{i-1}^i f \circ R_{i-1}^i \ii \circ \inj_1^{i-1} \circ g \\
			&=& \left[E(f) \circ \phi_{X'Y'Z'}(\ii) \circ (g,h)\right]_1
		\end{array}\]
		
		The second components are defined as described by the following diagram
		
		\diagram{D10}
		
		The second projection of $\phi_{XYZ}(f \circ \ii \circ W(g,h))$ is defined by the pullback of $E(Z')$ commuting with the two path highlighted by the blue line. And that of $E(f) \circ \phi_{X'Y'Z'}(\ii) \circ (g,h)$ is defined by the circled path.
		As the diagram commutes and by pullback property, we get the equality.
		
	\subsection{Proof of H1 - Sum definition}
	
		We will define the sums of the form $X \oplus_i L_0^i Y$ in $\BB_i$.
		
		\[
			X \oplus_i L_0^i Y := \left(R_{i-1}^i \oplus_{i-1} L_0^{i-1} Y, (R_0^{i-1} \inj_1^{i-1})_\UU \circ \Cstr_i^X \circ (\inj_1^{i-1} \circ \dash)^{-1}\right)
		\]
		
		Here, $(\inj_1^{i-1} \circ \dash)^{-1}$ is the inverse of the isomorphism of hypothesis H3', and 
		
		The constructor goes as follows:
		\[
			\Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y) \equiv \Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,R_{i-1}^i X) \to (R_0^{i-1} X)_\UU \to (R_0^i (R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y))_\UU
		\]
		
		The first injector $X \to X \oplus_i L_0^i Y$ is defined as follows:
		\[
			\inj_1^i := \inj_1^{i-1} : R_{i-1}^i X \to R_{i-1}^i (X \oplus_i L_0^i Y) = R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y
		\]
		
		It is a morphism of $\BB_i$ as it makes the following diagram commute:
		
		\diagram{D4}
		
		The second injector is defined as follows:
		\[
			inj_2^i := (\eta_i \oplus_i \id_{L_0^i Y}) \circ L_{i-1}^i \inj_2^{i-1}
		\]
		
		Where $\eta_i$ is the counit of the adjunction $R_{i-1}^i \vdash L_{i-1}^i$, going from $L_{i-1}^i R_{i-1}^i X$ to $X$.
		
		This goes from $L_0^i Y = L_{i-1}^i L_0^{i-1} Y$ to $L_{i-1}^i(R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y)$, which is equivalent to $L_{i-1}^i R_{i-1}^i X \oplus_i L_0^i Y)$ as $L_{i-1}^i$ is a left-adjunct functor and therefore it preserves colimits; then goes to $X \oplus_i L_0^i Y$.
		
		We will now show that this definition is actually a definition of the coproduct in $\BB_i$.
		To that extent, we take two objects $X$ and $Z$ in $\BB_i$, $Y$ in $\TSet$ and two morphisms of $\BB_i$ $\varphi_1 : X \to Z$ and $\varphi_2 : L_0^i Y \to Z$.
		
		We define $\{\varphi_1 ; \varphi_2\}_{i	} = \{R_{i-1}^i \varphi_1 ; R_{i-1}^i \varphi_2 \circ \varepsilon^i_{L_0^{i-1} Y}\}_{i-1}$ a morphism of $\BB_i$ as it makes the following diagram commute:
		
		\diagram{D5}
		
		\todo{Justifier $R_{i-1}^i(\eta_i \oplus_i \id_{L_0^i Y}) = R_{i-1}^i \eta_i \oplus_{i-1} \id_{L_0^{i-1} Y}$ (with H1 ?)}
		
	
	\section{Summary}
		
		\lipsum[2-3]
	
	
	
	\section{Bibliography}
	\begingroup
	\renewcommand{\section}[2]{}%
	\printbibliography
	\endgroup
	
	\newpage
	\addappheadtotoc
	\appendix
	\addtocontents{toc}{\protect\setcounter{tocdepth}{-1}}
	\appendixpage
	
	
\end{document}