827 lines
34 KiB
TeX
827 lines
34 KiB
TeX
% !TeX spellcheck = en_US
|
||
\documentclass[10pt,a4paper]{article}
|
||
|
||
\input{./header.tex}
|
||
|
||
% po4a: environment remark
|
||
% po4a: environment tikzpicture
|
||
% po4a: environment property
|
||
|
||
\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}
|
||
|
||
A Generalized Algebraic Theory (or GAT), first introduced by Cartmell \cite{CartmellGATs}, is a syntactic specification of an algebraic structure. From a GAT, one can define a category of models describing the models of the algebraic structure.
|
||
A GAT typically starts with a sort specification i.e. a list of sort declarations, eventually followed by a list of constructors.
|
||
In this document, we will not ask ourselves about the specific syntax of GATs, a \enquote{vague} definition is enough.
|
||
|
||
\paragraph{Sort specification}
|
||
|
||
A sort specification is a list of \emph{sort declarations} that are defined with \emph{parameters} with $\Set$ as its codomain.
|
||
|
||
We give an example of a classical sort specification for Type Theory. On the right column we give the interpretation of the sort declaration on models.
|
||
|
||
\vspace{1em}
|
||
\renewcommand\arraystretch{1.5}
|
||
\begin{tabular}{l|p{.5\textwidth}}
|
||
$\Con : \Set$ & A set of contexts\\
|
||
$\Ty : (\Gamma : \Con) \to \Set$ & For each context $\Gamma$, a set of types in this context\\
|
||
$\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set$ & For each context $\Gamma$ and each type $A$ in this context, a set of terms of this type.
|
||
\end{tabular}
|
||
\vspace{1em}
|
||
|
||
A model of this category is a triple
|
||
\begin{itemize}
|
||
\item A set $X_\Con$ of contexts
|
||
\item A family of sets $\left(X_\Ty\left(\Gamma\right)\right)_{\Gamma \in _\Con}$ of types, indexed by contexts
|
||
\item A family of sets $\left(X_\Tm\left(\Delta,A\right)\right)_{\Delta\in X_\Con,\: A \in X_\Ty\left(\Delta\right)}$ of terms, indexed by contexts and types.
|
||
\end{itemize}
|
||
|
||
\paragraph{Constructor specification}
|
||
We can also add constructors to a sort specification to make a complete GAT.
|
||
For example, for the previous sort specification, one can add the following constructors:
|
||
|
||
\vspace{1em}
|
||
\renewcommand\arraystretch{1.5}
|
||
\begin{tabular}{p{.37\textwidth}|p{.6\textwidth}}
|
||
$\operatorname{unit} : (\Gamma : \Con) \to \Ty\;\Gamma$ & In any context $\Gamma$, a type of $\Ty\;\Gamma$ called unit.\\
|
||
|
||
$\operatorname{tt}: (\Gamma : \Con) \to \Tm\;\Gamma\;(\operatorname{unit}\;\Gamma)$ & In any context $\Gamma$, we have a term whose type is the $\operatorname{unit}$ of this context ($\operatorname{unit}\;\Gamma$).
|
||
\end{tabular}
|
||
\vspace{1em}
|
||
|
||
This adds to the previous model two functions that \enquote{points} one element of the sets
|
||
\begin{itemize}
|
||
\item For each $\Gamma \in X_\Con$, an element $\operatorname{unit}\;\Gamma \in X_\Ty(\Gamma)$
|
||
\item For each $\Gamma \in X_\Con$, an element $\operatorname{tt}\;\Gamma \in X_\Tm(\Gamma,\operatorname{unit}\;\Gamma)$
|
||
\end{itemize}
|
||
|
||
Sort declarations describe the sets that the model contains, whereas the constructors describe elements of these sets.
|
||
|
||
\paragraph{Two-sortification}
|
||
|
||
There is a process that allows us to transform a GAT into a GAT with only two sorts.
|
||
The sort specification of the transformed GAT is always the same, and contains these two sort declarations:
|
||
|
||
\vspace{1em}
|
||
\begin{tabular}{p{0.37\textwidth}|p{0.5\textwidth}}
|
||
$\UU : \Set$ & The set of sorts \\
|
||
$\El : \mathcal{O} \to \Set$ & For every sort object $o$ in the set of sorts, a set called $\El(o)$ of objects corresponding to the sort object. We will write this set $\underline{o}$ rather than $\El(o)$.
|
||
\end{tabular}
|
||
\vspace{1em}
|
||
|
||
Then, we replace all occurrences of $\Set$ to $\mathcal{O}$, and we apply $\El$ to every parameter. For example, the Type Theory GAT presented above becomes that which follows:
|
||
|
||
\begin{tabular}{p{0.4\textwidth}|p{0.5\textwidth}}
|
||
$\Con : \mathcal{O}$ & One sort object is called \enquote{$\Con$} \\
|
||
$\Ty : (\Gamma : \underline{\Con}) \to \mathcal{O}$ &
|
||
For each object $\Gamma$ corresponding to the sort object $\Con$, another sort object called \enquote{$\Ty\;\Gamma$} \\
|
||
$\Tm : (\Gamma : \underline{\Con}) \to (A : \underline{\Ty\;\Delta}) \to \mathcal{O}$ &
|
||
For each object $\Gamma$ corresponding to the sort object $\Con$,
|
||
and for every object $A$ corresponding to the sort object $\Ty\;\Gamma$, another sort object called "$\Tm\;\Gamma\;A$"\\
|
||
$\operatorname{unit} : (\Gamma : \underline{\Con}) \to \underline{\Ty\;\Gamma}$ &
|
||
For each object $\Gamma$ corresponding to the sort object $\Con$, an object called "$\operatorname{unit} \Gamma$" corresponding to the sort object $\Ty\;\Gamma$\\
|
||
$\operatorname{tt}: (\Gamma : \underline{\Con}) \to \underline{\Tm\;(\operatorname{unit}\;\Gamma)}$ &
|
||
$\dots$
|
||
\end{tabular}
|
||
|
||
This process has been observed by Zongpu Szumi Xie \cite{AmbrusSzumiXie2sort}, and Philippo Sestini used it in his thesis \cite{SestiniPhD}:
|
||
|
||
\begin{quote}
|
||
Many instances of multi-sorted IITs [IITs are another type of GATs] can be reduced to equivalent two-sorted IITs, via a systematic reduction method originally observed by Zongpu (Szumi) Xie. We are not aware of a formal proof of this construction for arbitrary IITs, but we conjecture that it does apply to all instances of induction-induction and consequently that it shows two-sorted IITs are enough to represent any specifiable IIT.
|
||
\end{quote}
|
||
|
||
\paragraph{Goal}
|
||
|
||
The goal my internship was to formally study this transformation, and to try to find a relation between the semantics of a GAT and its two-sorted version.
|
||
|
||
We managed to construct a coreflection between a category of models and the category of models of the transformed GAT.
|
||
The existence of this coreflection is enough to prove what Sestini conjectured.
|
||
|
||
We will give a formal definition of this coreflection in next section. It will consist of an adjunction $F \vdash G$ between the category $\CC$ of the models of the GAT and the category $\BB$ of the models of the two-sortified GAT, where G is full and faithful.
|
||
The category $\BB$ will be built with a forgetful functor $R$ to $\BB_0$, the category of models of the two-sort sort specification $(\mathcal{O},\El)$. This forgetful $R$ functor is a composition of monadic functors, one for each sort constructor.
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM G1-0.json
|
||
% GENERATED LATEX
|
||
\input{graphs/G1-0.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
\section{Construction of the coreflection}
|
||
|
||
\subsection{Preliminaries}
|
||
|
||
\paragraph{Category of models of the two-sort sort specification}
|
||
|
||
The usual way of defining the category of models of the two-sort specification $\BB_0$ is by taking the category of families of sets. However, in order to have more elegant constructions, we will use a the category of models of the two-sort specification the category $\TSet$ of presheaves over the category with one arrow.
|
||
|
||
In the rest of the document, we will denote this category with one arrow as $\TT$. The objects and arrow of this category are pictured below.
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM G0.json
|
||
% GENERATED LATEX
|
||
\input{graphs/G0.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
With this formalisation, a model of the two-sort GAT is a functor $X : \TSet$, such that
|
||
\begin{itemize}
|
||
\item $X_\UU$ is the set of the \enquote{sort objects}
|
||
\item For each sort object $\Gamma \in X_\UU$, the set of objects corresponding to the sort object is $X_p^-1(\{\Gamma\}) \subset X_\El$
|
||
\end{itemize}
|
||
|
||
Therefore the categories of models of the transformed GATs will be built atop of this category $\BB_0 = \TSet$.
|
||
|
||
\paragraph{Grothendieck Construction}
|
||
For a category $\mathcal{C}$ and a functor $F : \mathcal{C} \to \Cat$, the Grothendieck construction is a category whose objects are pairs of
|
||
\begin{itemize}
|
||
\item $X$ an object of $\mathcal{C}$
|
||
\item an object of $F(X)$
|
||
\end{itemize}
|
||
|
||
The morphism $(X,Y) \to (X',Y')$ is therefore a pair of a morphism $f : X \to X'$ in $\mathcal{C}$ and a morphism $g : F(f)(Y) \to Y'$ in $H(X')$.
|
||
|
||
We will denote this category $(X : \mathcal{C}) \times F(X)$ as its objects are pairs. It can some times be found written as $\int^\mathcal{C} F$ or $\sqint^\mathcal{C} F$
|
||
|
||
\paragraph{Slice category}
|
||
For a category $\mathcal{C}$ and $X$ an object in that category, the slice category (or over category) $\mathcal{C}/A$ is a category whose objects are pairs of
|
||
\begin{itemize}
|
||
\item $Y$ an object of $\mathcal{C}$
|
||
\item an arrow $X \to Y$ of $\mathcal{C}$
|
||
\end{itemize}
|
||
|
||
A morphism $(Y,f) \to (Y',f')$ is a morphism $g : Y \to Y'$ such that $g \circ f = f'$.
|
||
|
||
We can deduce a functor $\left(\mathcal{C}/\dash\right) : \mathcal{C} \to \Cat$ from this construction.
|
||
|
||
If the category $\mathcal{C}$ is $\Set$, we have that $\Set/X \cong \Set^X$.
|
||
|
||
We will often concatenate the two method above to create from a category $\mathcal{C}$ and a functor $H : \mathcal{C} \to \Set$ a new category $(X : \mathcal{C}) \times \left(\Set\middle/H(X)\right)$.
|
||
|
||
\paragraph{$\Hbar$ functor}
|
||
|
||
Where $\Hbar_A$ is a functor $(X:C) \times (\Set/A(X)) \to \TSet$ defined as
|
||
\[
|
||
\Hbar_X(X,(Y,f)) = \TSetObject{Y}{f}{A(X)}
|
||
\]
|
||
The morphisms are translated as-is.
|
||
|
||
\begin{remark}
|
||
This functor can be constructed using the property of the Grothendieck construction
|
||
\end{remark}
|
||
|
||
\subsection{Constructing the categories}
|
||
|
||
We will construct both categories $\CC$ and $\BB$ recursively, adding new sorts one by one for each constructor. At each recursion step, we will build the categories, the adjunction, and keep some invariants that will be stated in \autoref{sec:hypotheses}.
|
||
|
||
At the i-th recursion step, we will build the category $\CC_i$ which is the category of models of the $i$ first sorts of the sort specification. $\BB_i$ will samewise be the category of models of the 2-sorted $i$ first sorts of the sort specification.
|
||
|
||
The overall recursive construction of the categories and of the adjunctions $F_i \vdash G_i$ is given below.
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM G1.json
|
||
% GENERATED LATEX
|
||
\input{graphs/G1.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
The first step of our recursion is the trivial adjunction $\lambda . \star \vdash \lambda . 1$ between the categories $\BB_0 = \TSet$ and $\CC_0 = 1$.
|
||
|
||
The functors $R_{i-1}^i$ are the forgetful monadic functors that forget about the $i$-th sort contsructor. They have a left adjoint denoted $L_{i-1}^i$.
|
||
As we can compose the adjunctions $R_0^1$,$R_1^2$,...,$R_{i-1}^i$, we will use the two following adjunctions
|
||
\[\begin{array}{c}
|
||
R_0^i = R_{0}^{i-1} \circ R_{i-1}^{i} = R_{0}^{1} \circ ... \circ R_{i-1}^{i}\\
|
||
L_0^i = L_{i-1}^{i} \circ L_{0}^{i-1} = L_{i-1}^{i} \circ ... \circ L_{0}^{1}
|
||
\end{array}\]
|
||
|
||
\begin{remark}
|
||
There is also an adjunction chain between $\CC_0$,$\dots$,$\CC_{i-1}$,$\CC_i$, but we don't use it in the proof.
|
||
\end{remark}
|
||
|
||
\subsubsection{Constructing $\CC_i$}
|
||
|
||
We construct the category $\CC_i$ as the following pair:
|
||
\[
|
||
\CC_i = (X : \CC_{i-1}) \times \left(\Set\middle/H_i\right) = (X : \CC_{i-1}) \times \left(\Set^{H_i}\right)
|
||
\]
|
||
and where $H_i$ is a specific representable functor $\CC_{i-1} \to \Set$, such that $H_i(X)$ is the set of parameters for the construction of the new sort.
|
||
|
||
\paragraph{$H_i$ functors for Type Theory}
|
||
I will give now an example of those $H_i$ objects for our type theory example. We begin with
|
||
\[
|
||
H_1(\star) = 1 \in \operatorname{Obj}(\Set)
|
||
\]
|
||
which corresponds to the fact that $\Con$ takes no parameter.
|
||
|
||
Therefore $\CC_1 = 1 \times \Set^1 = \Set$, and the set of a model corresponds to \enquote{the set of contexts}.
|
||
|
||
Then, we take the functor $H_2(X_\Con) = X_\Con$ (this means, that types need \emph{one} context to be built).
|
||
|
||
Therefore $\CC_2 = (X:\Set) \times \Set^X \cong \FamSet$, families of sets.
|
||
|
||
Finally, we take the functor $H_3(X_\Con,X_\Ty) = \sum_{\Gamma : X_\Con}X_\Ty(\Gamma)$ (this means that terms need \emph{one} context, and \emph{one} type of that context).
|
||
|
||
The final category $\CC_3$ is composed of triples $(X_\Con: \Set, X_\Ty : X_\Con \to \Set, X_\Tm : (\Delta: X_\Con) \to X_\Ty(\Delta) \to \Set)$
|
||
|
||
\begin{remark}
|
||
There is a way of getting the functor $H_i$ from the syntax, which is given in \autoref{sec:CtoSSetFiore}.
|
||
\end{remark}
|
||
|
||
\subsubsection{Constructing $\BB_i$}
|
||
|
||
\paragraph{The category} We construct the category $\BB_i$ as follows.
|
||
|
||
An object of $\BB_i$ is
|
||
\begin{itemize}
|
||
\item an object $X$ of $\BB_{i-1}$
|
||
\item a \enquote{sort constructor} $\Cstr_i$ as a function $H_i(F_{i-1}X) \to (R_0^{i-1}X)_\UU$
|
||
\newline
|
||
where $H_i$ is the functor $\CC_{i-1} \to \Set$ that describe the sort constructor being processed, and $F_{i-1}$ is the right part of the adjunction $\BB_{i-1} \to \CC_{i-1}$ that we are defining recursively at the same time.
|
||
This $H_i$ functor will be so that $H_i \circ F_{i-1} \circ \inj_1^{i-1}$ is an isomorphism. \inlinetodo{Pas déclaré ici, c'est grâve ?}
|
||
\end{itemize}
|
||
|
||
|
||
A morphism $(X,\Cstr_i) \to (X',\Cstr'_i)$ of $\BB_i$ is a morphism $f : X \to X'$ in $\BB_{i-1}$ such that the following diagram commutes.
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM D1.json
|
||
% GENERATED LATEX
|
||
\input{graphs/D1.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
Identities and compositions are that of the category $\BB_{i-1}$, and categorical equalities are trivially derived from the diagram above.
|
||
|
||
\paragraph{The adjunction}
|
||
We also define a functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$ that sends objects and morphisms to their first component. This functor is a \emph{right adjoint} of another functor we call $L_{i-1}^i$.
|
||
|
||
We will also denote $\eta_i^j : \mathbf{1} \to R_i^j L_i^j$ and $\varepsilon_i^j : L_i^j R_i^j \to \mathbf{1}$ to be the unit and counit of the adjunction $R_i^j \vdash L_i^j$.
|
||
|
||
\paragraph{The coproduct}
|
||
For an object $X$ in $\BB_i$ and $Y$ in $\BB_0$, there is a coproduct $X \oplus_i L_0^i Y$ in the category $\BB_{i-1}$. We will denote as $\inj_1^i : X \to X \oplus L_0^iY$ (resp. $\inj_2^i : L_0^iY \to X \oplus L_0^iY$) the first (resp. second) injector of the coproduct of $\BB_i$. For every morphism $f : X \to Z$ and $g : L_0^iY \to Z$, we will denote with $\{f;g\}$ the unique morphism from $X \oplus L_0^iY$ to $Z$ such that $\{f;g\} \circ \inj^i_1 = f$ and $\{f;g\} \circ \inj^i_2 = g$.
|
||
|
||
\begin{remark}
|
||
This adjunction and the existence of a coproduct comes from seeing $\BB_i$ being a category of algebras in $\BB_{i-1}$ over the morphism $inj_1 : G_{i-1}O_i \to G_{i-1}O_i \oplus L_0^{i-1} y\UU$. \inlinetodo{Ça ne marche plus du coup :/}
|
||
\end{remark}
|
||
|
||
|
||
\subsection{Induction Hypotheses}
|
||
|
||
In order to build and prove the adjunction, we will state some recurrence invariants that we will prove after having built objects.
|
||
|
||
\begin{property}[H1]
|
||
|
||
The canonical morphism
|
||
\[
|
||
\simpleArrow{R_{i-1}^i X \oplus L_0^{i-1} Y}{\left\{R_{i-1}^i \inj_1^i ; R_{i-1}^i \inj_2^i \circ \eta_{i-1}^i\right\}}{R_{i-1}^i(X \oplus_i L_0^i Y)}
|
||
\]
|
||
that we will denote as $\en_{i-1}^i$ is an isomorphism.
|
||
|
||
Its recursive version is the following isomorphism, denoted as $\en_0^i$
|
||
\[
|
||
\simpleArrow{ R_{0}^i X \oplus_0 Y}{\left\{R_0^i \inj_1^i ; R_0^i \inj_2^i \circ \eta_0^i\right\}}{R_0^i(X \oplus_i L_0^i Y)}
|
||
\]
|
||
\end{property}
|
||
|
||
\begin{property}[H3]
|
||
\[
|
||
\simpleArrow{F_i X}{F(\inj_1^i)}{F_i(X \oplus L_0^i Y)}
|
||
\]
|
||
is an isomorphism.
|
||
|
||
We will often this equality along with the $F_i \vdash G_i$ adjunction (for an object $O$ in $\CC_i$)
|
||
\[
|
||
\Hom(G_i O, X) \cong \Hom(O, F_i X) \cong \Hom(O, F_i(X \oplus L_0^i Y)) \cong \Hom(G_i O, X \oplus L_0^i Y)
|
||
\]
|
||
|
||
This new isomorphism is the following:
|
||
\[
|
||
\simpleArrow{\Hom(G_i O, X)}{(inj_1^i \circ \dash)}{\Hom(G_i O,X \oplus L_0^i Y)}
|
||
\]
|
||
|
||
\todo{Du coup techniquement, c'est une propriété de $H_i$. Faut réussir que c'est \emph{parce que} $H_i$ est représentable que l'on peut déduire H3' de H3.}
|
||
|
||
\end{property}
|
||
|
||
\subsection{Constructing the functors}
|
||
|
||
In order to use all the power of the recurrence, we will build the $F_i \vdash G_i$ adjunction using the $F_{i-1} \vdash G_{i-1}$ adjunction, following the diagram below.
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM G2.json
|
||
% GENERATED LATEX
|
||
\input{graphs/G2.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
\todo{$G_{i-1} \times \id$ et son compère, c'est bien legit ?}
|
||
|
||
The first part $G_{i-1} \times \id \dashv F_{i-1} \times \id$ is proven and defined as an adjunction from the previous step of the recurrence.
|
||
|
||
|
||
\subsubsection{W definition}
|
||
|
||
We define a functor $W : \left(X : \BB_{i-1}\right) \times \Set/H_i(F_{i-1}X) \to \BB_{i}$
|
||
|
||
The action on objects is as follows:
|
||
\[
|
||
W(X,Y) := \left(X \oplus L_0^{i-1} \Hbar_{H_iF_{i-1}}(X,Y), \widetilde{\inj_2} \right)
|
||
\]
|
||
|
||
With $\widetilde{\inj_2}$ being defined by \inlinetodo{Changer les noms des hypothèses H3' et H1r}
|
||
\[
|
||
\begin{array}{lcl}
|
||
H_iF_{i-1}(X \oplus L_0^{i-1} \Hbar_\bullet(X,Y)))
|
||
& \to^{\text{H3'}} & H_i(F_{i-1}X)\\
|
||
& = & \left(\Hbar_{H_iF_{i-1}}(X,Y)\right)_\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_{H_iF_{i-1}}(g,h)\right)
|
||
\]
|
||
|
||
It is indeed a morphism from $\BB_{i}$ as it makes the following diagram commute.
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM D2.json
|
||
% GENERATED LATEX
|
||
\input{graphs/D2.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
\subsubsection{E definition}
|
||
|
||
We define $E : \BB_{i} \to \left(X : \BB_{i-1}\right) \times (\Set/H_iF_{i-1}X)$
|
||
|
||
The action on objects is
|
||
\[
|
||
E(X) = (R_{i-1}^i X, (A,h))
|
||
\]
|
||
Where $(A,h)$ is defined as the following pullback:
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM D3a.json
|
||
% GENERATED LATEX
|
||
\input{graphs/D3a.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
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 (thanks to the pullback property):
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM D3b.json
|
||
% GENERATED LATEX
|
||
\input{graphs/D3b.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
\subsection{Proof of the adjunction}
|
||
|
||
We prove that $(W,E)$ make an adjunction showing that there is a natural isomorphism between $\Hom$ sets in both categories.
|
||
|
||
We want to construct for each $(X,Y)$ in $(X : \BB_{i-1}) \times (\Set/H_iF_{i-1}X)$ and $Z$ in $\BB_i$, an isomorphism $\phi_{XYZ}$.
|
||
|
||
\[
|
||
\phi_{XYZ} : \Hom(W(X,Y),Z) \to \Hom((X,Y),E(Z))
|
||
\]
|
||
|
||
I will give the construction of the isomorphisms and its inverse, the proofs are given in \autoref{apx:phi-WE-isnat}.
|
||
|
||
\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:
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM D6.json
|
||
% GENERATED LATEX
|
||
\input{graphs/D6.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
\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 ; \varepsilon_0^i \circ L_0^{i-1} \square \right\}
|
||
\]
|
||
|
||
Where $\square$ is a morphism $\Hbar (X,Y) \to R_0^i Z$ in $\TSet$ defined by the following diagram:
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM D7.json
|
||
% GENERATED LATEX
|
||
\input{graphs/D7.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
This is indeed a morphism of $\BB_i$ from $W(X,Y)$ to $Z$ as it makes the following diagram commute
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM D8.json
|
||
% GENERATED LATEX
|
||
\input{graphs/D8.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
We show in \autoref{apx:phi-WE-isnat} that $\phi_{XYZ}$ and $\phi_{XYZ}^{-1}$ do indeed make a natural isomorphism.
|
||
|
||
|
||
|
||
\subsubsection{Properties of the adjunction}
|
||
We have proven that $F_i \vdash G_i$ make a reflection, i.e. that $F_iG_i \cong \Id_{\CC_i}$.
|
||
|
||
The proof is given in \autoref{apx:FG-refl}.
|
||
|
||
\subsection{Proof of the hypotheses}
|
||
\subsubsection{Proof of H1}
|
||
|
||
\todo{Relire + réeexpliquer pourquoi ça prouve}
|
||
|
||
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:
|
||
\[
|
||
H_iF_{i-1}(R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y) \equiv
|
||
H_iF_{i-1}(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:
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM D4.json
|
||
% GENERATED LATEX
|
||
\input{graphs/D4.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
|
||
The second injector is defined as follows:
|
||
\[
|
||
inj_2^i := (\varepsilon_i \oplus_i \id_{L_0^i Y}) \circ L_{i-1}^i \inj_2^{i-1}
|
||
\]
|
||
|
||
Where $\varepsilon_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-adjoint 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 \eta^i_{L_0^{i-1} Y}\}_{i-1}$ a morphism of $\BB_i$ as it makes the following diagram commute:
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM D5.json
|
||
% GENERATED LATEX
|
||
\input{graphs/D5.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
|
||
\todo{Justifier $R_{i-1}^i(\varepsilon_i \oplus_i \id_{L_0^i Y}) = R_{i-1}^i \varepsilon_i \oplus_{i-1} \id_{L_0^{i-1} Y}$ (with H1 ?)}
|
||
|
||
\subsubsection{Proof of H3}
|
||
|
||
|
||
\section{Misc}
|
||
|
||
\subsection{Fiore's Category - Fibration of the category of sorts}
|
||
|
||
Fiore \cite{Fiore2008} describes \emph{sort specifications} as countable simple direct categories (i.e. countable categories where all the arrows follow an unique direction and hom-sets are finite). The models of a GAT then are the presheaves over that category $S$: $\left[S,\Set\right]$.
|
||
|
||
One can understand the correspondance between those categories and sort specifications as follows:
|
||
\begin{itemize}
|
||
\item An object of the category is a sort of the specification.
|
||
\item An arrow $x$ from an object $s$ to an object $s'$ is a parameter of the sort declaration of $s$ of the for $(x : s' \dots)$.
|
||
\item The parameter $y$ of a parameter $x$ of a sort specification (i.e. the sort declaration parameter has the form $(x: s' \dots \left[y=z\right] \dots)$) is given by $z = x \circ y$.
|
||
\end{itemize}
|
||
|
||
\begin{remark}
|
||
We ignore in this definition identity arrows, and we will do so in the rest of this document. Identities are the only arrows that are not «directed» in the direct category.
|
||
|
||
Interpreting the identity arrow would mean having a parameter of type $s$ to construct the sort $s$. which loops in a self-dependency.
|
||
|
||
You can assume in the rest of the document that the formalizations \enquote{all arrows} or \enquote{the arrows} pointing to/from exclude identity arrows.
|
||
\end{remark}
|
||
|
||
\todo{Éventuellement changer tous les paramètres par la forme complète, exemple
|
||
\[
|
||
\operatorname{eq}: (\Gamma : \Con) \to (A : \Ty \left[\Gamma=\Gamma\right]) \to \Tm \left[\Gamma=\Gamma\right] \left[A=A\right] \to \Tm \left[\Gamma=\Gamma\right] \left[A=A\right] \to \Ty \left[\Gamma=\Gamma\right]
|
||
\]
|
||
C'est bien plus verbeux et en pratique pas utilisé, mais permet de mieux voir la «composition» dans la catégorie de Fiore.}
|
||
\todo{Est-ce qu'on fait une notation \enquote{arrow*} pour dire «flèche qui n'est pas l'identité» pour plus de rigueur ?}
|
||
|
||
For example the category version of the specification of sorts of Type Theory given above is defined as:
|
||
|
||
\begin{itemize}
|
||
\item There is three objects called $\Con$,$\Ty$, and $\Tm$.
|
||
\item The arrows are defined as
|
||
\begin{itemize}
|
||
\item There is no arrow going out of $\Con$
|
||
\item There is one arrow going out of $\Ty$: $\Gamma$ pointing to $\Con$.
|
||
\item There is two arrows going out of $\Tm$: $\Delta$ pointing to $\Con$ and $\Gamma$ pointing to $\Ty$.
|
||
\end{itemize}
|
||
\item The $\Gamma$ parameter of $\Ty$ in the parameter $A$ of $\Tm$ is $\Delta$. Therefore, we have $\Delta = A \circ \Gamma$.
|
||
\end{itemize}
|
||
|
||
The category is pictured below:
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM B1.json
|
||
% GENERATED LATEX
|
||
\input{graphs/B1.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
\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}$.
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM D1.json
|
||
% GENERATED LATEX
|
||
\input{graphs/D1.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
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{$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)
|
||
\]
|
||
|
||
\todo{Show that those are the same functors as those defined recursively. Prove the adjunction/reflection infinitely ?}
|
||
|
||
|
||
\subsection{$H$ functors}
|
||
|
||
For every set $X$, 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{Overview}
|
||
|
||
\subsubsection{$\CC$ as presheaf category}
|
||
\label{sec:CtoSSetFiore}
|
||
We use the specification of sorts definition of Fiore \cite{Fiore2008}.
|
||
|
||
A specification of sorts is given by a sequence of functors $\Gamma_i : S_{i-1} \to \Set$. We construct the category $S_{i+1}$ by adding a single object $\alpha_{i+1}$ to the category $S_{i}$, along with morphisms $f : \alpha_j \to \alpha_{i+1}$ for $f \in \Gamma_{i+1}(\alpha_j)$ and $j \leq i$. The morphisms follow the composition condition, describing that every pair of morphisms $f : \alpha_j \to \alpha_{i+1}$ and $g : \alpha_k \to \alpha_{i+1}$ (i.e. $f\in\Gamma_{i+1}(\alpha_k)$ and $g\in\Gamma_{i+1}(\alpha_j)$) and for every morphism of $S_{i}$ $h : \alpha_j \to \alpha_k$, we have $\Gamma_{i+1}(h)(f) \circ f = g$.
|
||
|
||
We have define a sequence of direct categories $\emptyset = S_0 \subset S_1 \subset S_2 \subset \dots$ (with inclusions functors $I_i : S_{i+1} \to S_i$). We define the \enquote{final} direct category as $S = \bigcup S_i$
|
||
|
||
This definition is an isomorphism, so we can define a GAT categorically as any locally finite direct category.
|
||
|
||
Then the semantics of the GAT is described as the category of presheaves over $S$, written $[S, \Set]$.
|
||
|
||
Altenkirsch has another way of constructing the semantics of a specification of sorts \cite{Altenkirch2018}, and he also describes a way to describe constructors.
|
||
|
||
So we can construct the base category, which is that of families of sets.
|
||
|
||
|
||
In order to construct the $i$-th sort, we use a finite functor $\Gamma_i : S_{i-1} \to \Set$ describing entirely the sort declaration.
|
||
|
||
This functor is to be understood as $\Gamma_i(a)$ is the set of parameters of type $a$ for our new sort. In the above example, we would have $\Gamma_\Ty(\Con) = \{"\Gamma"\} = 1$ and $\Gamma_\Tm(\Con) = \{\Delta\}$,$\Gamma_\Tm(\Ty) = \{"A"\}$,$\Gamma_\Tm(\Gamma) = \left["A" \mapsto "\Delta"\right]$.
|
||
|
||
Then, to construct $S_i$, we add one object $i$ to $S_{i-1}$, along with morphisms $x : i \to a$ for every $x \in \Gamma_i(a)$ for every $a$ in $S_{i-1}$. We also add equalities
|
||
$s \circ x = x'$ for every $s : b \to a$ and $x \in \Gamma_i(a)$ and $x' \in \Gamma_i(b)$ where $\Gamma_i(s)(x') = x$.
|
||
|
||
\begin{remark}
|
||
We have that $\Hom_{S_i}(a,b) = \Gamma_b(a)$ or $(a/S_i)* \equiv \Gamma_a$.\inlinetodo{C'est sûr la deuxième partie ?}
|
||
|
||
This equality allows us to construct the $\Gamma_i$ functors from the final $S$ category.
|
||
\end{remark}
|
||
|
||
\section{Summary}
|
||
|
||
\lipsum[2-3]
|
||
|
||
|
||
|
||
\section{Bibliography}
|
||
\begingroup
|
||
\renewcommand{\section}[2]{}%
|
||
\printbibliography
|
||
\endgroup
|
||
|
||
\newpage
|
||
\addappheadtotoc
|
||
\appendix
|
||
\addtocontents{toc}{\protect\setcounter{tocdepth}{-1}}
|
||
\appendixpage
|
||
|
||
\section{$W \dashv E$ adjunction}
|
||
\label{apx:phi-WE-isnat}
|
||
|
||
|
||
\subsection{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 ; \varepsilon_0^i \circ L_0^{i-1} \square \right\}) \circ \inj_1^{i-1} = \left\{g ; \varepsilon_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
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM D9.json
|
||
% GENERATED LATEX
|
||
\input{graphs/D9.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
The diagram commutes as the following equality holds:
|
||
\[
|
||
\left(\left\{g ; \varepsilon_0^i \circ L_0^{i-1} \square \right\} \circ \inj^{i-1}_2\right)_\El = \left(\varepsilon_0^i \circ L_0^{i-1} \square\right)_\El = (\varepsilon_0^i)_\El \circ (L_0^{i-1} \square)_\El = \square_El = \pi_1 \circ h
|
||
\]
|
||
|
||
\todo{Justify $(\varepsilon_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)
|
||
\]
|
||
|
||
\subsection{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} ; \varepsilon_0^i \circ L_0^{i-1} \square \right\}
|
||
\]
|
||
where $\square$ follows the following diagram
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM D10.json
|
||
% GENERATED LATEX
|
||
\input{graphs/D10.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
We want to show that $\phi_{XYZ}^{-1} (\phi_{XYZ}(f))$. By definition of $\{;\}$ in $\BB_1$, it suffices to show that $\varepsilon_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 \eta_0^{i-1} = R_0^i f \circ \left(R_0^{i-1} \inj_2^{i-1} \circ \eta_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 \eta_0^{i-1} = \inj_2^0$}
|
||
|
||
\subsection{Naturality}
|
||
|
||
We want to show that the following diagram commutes, for any objects $X$,$Y$,$Z$,$X'$,$Y'$,$Z'$ and morphisms $f$,$g$,$h$.
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM D10.0.json
|
||
% GENERATED LATEX
|
||
\input{graphs/D10.0.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
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
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM D11.json
|
||
% GENERATED LATEX
|
||
\input{graphs/D11.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
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.
|
||
|
||
|
||
\section{$F_i \vdash G_i$ reflection}
|
||
\label{apx:FG-refl}
|
||
|
||
\todo{La preuve :/}
|
||
|
||
\end{document}
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|