1022 lines
40 KiB
TeX
1022 lines
40 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 to understand the rest of the document.
|
|
|
|
\paragraph{Sort specification}
|
|
|
|
A sort specification is a list of \emph{sort declarations}, composed of \emph{parameters} and $\Set$ as their codomain.
|
|
|
|
We give an example of a sort specification for Type Theory. On the right column we give the interpretation of the sort declarations as components of the models of the GAT.
|
|
|
|
\vspace{1em}
|
|
\renewcommand\arraystretch{1.5}
|
|
\begin{tabular}{l|p{.5\textwidth}}
|
|
$\Con : \Set$ & A set of contexts $X_\Con$\\
|
|
$\Ty : (\Gamma : \Con) \to \Set$ & For each context $\Gamma \in X_\Con$, a set $X_\Ty(\Gamma)$ of types in this context\\
|
|
$\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set$ & For each context $\Gamma \in X_\Con$ and each type $A \in X_\Ty(\Gamma)$ in this context, a set $X_\Tm(\Gamma,A)$ of terms of this type.
|
|
\end{tabular}
|
|
\vspace{1em}
|
|
|
|
A sort specification therefore specifies the differents families of sets contained in a model, and how they relate to each other in terms of indexing.
|
|
|
|
\paragraph{Constructor specification}
|
|
We can also add constructors to a sort specification. They are composed of parameters (the same kind as sort declarations) and of a codomain which is a sort defined in a previous sort declaration. Those constructors specify elements of the sets contained in the model.
|
|
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 \in X_\Con$, a type $\operatorname{unit}(\Gamma) \in X_\Ty(\Gamma)$.\\
|
|
|
|
$\operatorname{tt}: (\Gamma : \Con) \to \Tm\;\Gamma\;(\operatorname{unit}(\Gamma))$ & In any context $\Gamma \in X_\Con$, an element $\operatorname{tt}(\Gamma) \in X_\Tm(\Gamma,\operatorname{unit}(\Gamma))$.
|
|
\end{tabular}
|
|
\vspace{1em}
|
|
|
|
\paragraph{Two-sortification}
|
|
|
|
It was observed \cite{AmbrusSzumiXie2sort} that one can transform any GAT into a GAT with only two sorts. We will present this transformation.
|
|
|
|
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 $o$.
|
|
\end{tabular}
|
|
\vspace{1em}
|
|
|
|
|
|
|
|
Then, we replace all occurrences of $\Set$ to $\mathcal{O}$, and we apply $\El$ to every parameter. We write $\underline{o}$ rather than $\El(o)$ in order to ease reading. 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 \enquote{$\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 is useful when studying GATs, as it allows to restrict a study to GATs with only two sorts without loss of generality. Filippo Sestini noticed that in his thesis \cite{SestiniPhD}, although they didn't prove it.
|
|
|
|
\begin{quote}
|
|
Many instances of multi-sorted IITs [IITs are a variant 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 of my internship was to study and understand the relationship between the categories of models of an original GAT and the category of models of the transformed \enquote{two-sortified} GAT, in order to legitimate this transformation. In this document, we will only study sort specifications (i.e. lists of sort declaration, with no constructors).
|
|
|
|
We constructed a coreflection between those two categories, whose formal definition is given in next section. It consists 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$ is equipped with a forgetful functor $R$ to $\BB_0$, the category of models of the two-sort sort specification $(\mathcal{O},\El)$.
|
|
|
|
\begin{center}
|
|
% YADE DIAGRAM G1-0.json
|
|
% GENERATED LATEX
|
|
\input{graphs/G1-0.tex}
|
|
% END OF GENERATED LATEX
|
|
\end{center}
|
|
|
|
\section{Constructing the coreflection}
|
|
|
|
\paragraph{Structure of the proof}
|
|
|
|
We will formalize the transformation for \emph{sort specifications} (i.e. lists of sort declarations).
|
|
|
|
This proof is an induction on the number of sorts taken into account. At each step, we will add a new sort declaration, represented by a functor $H_i$ described later (\autoref{sec:constructingCategory}).
|
|
|
|
At the $i$-th recursion step, we will build the following objects :
|
|
\begin{itemize}
|
|
\setlength\itemsep{-1ex}
|
|
\item The category of models of the GAT $\CC_i$
|
|
\item The category of models of the transformed GAT $\BB_i$
|
|
\item A forgetful functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$ that creates limits. In our type theory example, $R_1^2$ is a functor from the category of models of $(\mathcal{O},\El,\Con,\Ty,\Tm)$ to the category of models of $(\mathcal{O},\El,\Con,\Ty)$.
|
|
|
|
Those functors compose themselves into a functor $R_0^i : \BB_i \to \BB_0$, that also creates limits:
|
|
\[
|
|
R_0^i := R^1_0 \circ \dots \circ R_{i-1}^i
|
|
\]
|
|
\item An operator $\tl^i : \BB_i \times \BB_0 \to \BB_i$ along with a morphism $\inj_\tl^i : X \to X \tl^i Y$ for every $X,Y$ in $\BB_i \times \BB_0$, such that the canonical morphism $\en_{i-1}^i : (R_{i-1}^i X) \tl^{i-1} Y \to R_{i-1}^i (X \tl^i Y)$ is an isomorphism. This operation follows a specific universal property: For every morphisms $g : X \to Z$ and $h : Y \to R_0^iZ$, there is an unique morphism $\{g;h\}$ such that the two following diagrams commute:
|
|
\label{sec:tlUniversalProperty}
|
|
|
|
\begin{center}
|
|
% YADE DIAGRAM TlUniversal.json
|
|
% GENERATED LATEX
|
|
\input{graphs/TlUniversal.tex}
|
|
% END OF GENERATED LATEX
|
|
\end{center}
|
|
|
|
where $\en_0^i$ is the following composition:
|
|
|
|
\[\en_0^i := R_0^{i-1} \en_{i-1}^i \circ \dots \circ R_0^1\en_1^2 \circ \en_0^1 : (R_0^i X) \oplus Y = (R_0^i X) \tl^0 Y \to R_0^i (X \tl^i Y)\]
|
|
|
|
And where $\inj_2$ is the second injector of $\oplus$, the coproduct of the category $\BB_0 = \TSet$. We will define $\tl^0$ to be $\oplus$, so the equality above holds.
|
|
|
|
The operator is also defined on morphisms, such that for any morphism $g : X \to X'$ in $\BB_i$ and $h : Y \to Y'$ in $\BB_0$, there is a morphism $g \tl^i h : X \tl^i Y \to X' \tl^i Y'$ in $\BB_i$.
|
|
|
|
\item A functor $F_i : \BB_i \to \CC_i$
|
|
\item A functor $G_i : \CC_i \to \BB_i$
|
|
\item An adjunction between them $F_i \vdash G_i$
|
|
\item A proof that $F_iG_i \cong \Id_{\CC_i}$ (i.e. $F_i \vdash G_i$ make up a coreflection)
|
|
\item A proof that $F_i\inj_\tl^i$ is an isomorphism. The inverse isomorphism will be denoted as $(F_i\inj_\tl^i)^{-1}$
|
|
\end{itemize}
|
|
|
|
Here is a figure that describes the recursive construction of some of the above objects
|
|
\begin{center}
|
|
% YADE DIAGRAM G1.json
|
|
% GENERATED LATEX
|
|
\input{graphs/G1.tex}
|
|
% END OF GENERATED LATEX
|
|
\end{center}
|
|
|
|
\subsection{Preliminaries}
|
|
|
|
\paragraph{Grothendieck Construction}
|
|
For a category $\mathcal{C}$ and a functor $F : \mathcal{C} \to \Cat$, the Grothendieck construction of $F$ 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.
|
|
|
|
\paragraph{Slice category}
|
|
For a category $\mathcal{C}$ and $X$ an object in that category, the slice category (or over category) $\mathcal{C}/X$ is a category whose objects are pairs of
|
|
\begin{itemize}
|
|
\item $Y$ an object of $\mathcal{C}$
|
|
\item an arrow $Y \to X$ of $\mathcal{C}$
|
|
\end{itemize}
|
|
|
|
A morphism $(Y,f) \to (Y',f')$ is a morphism $g : Y \to Y'$ such that $f' \circ g = f$.
|
|
|
|
We can define a functor $\left(\mathcal{C}/\dash\right) : \mathcal{C} \to \Cat$ from this construction.
|
|
|
|
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{Slice category over a set}
|
|
|
|
When the category $\mathcal{C}$ is $\Set$, we have the equivalence
|
|
\[\Set/X \simeq \Set^X\]
|
|
|
|
This equivalence is described by the following correspondence of objects.
|
|
An object $(Y,f)$ of $\Set/X$ is transformed into the family of sets $A : X \to \Set$ defined by
|
|
\[
|
|
A(x) := f^{-1}(\{x\}) = \text{the coimage by f of the singleton $\{x\}$}
|
|
\]
|
|
|
|
Conversly, a familiy of sets $A : X \to \Set$ is transformed into the following object of $\Set/X$
|
|
\begin{center}
|
|
% YADE DIAGRAM EquivSetXSetX.json
|
|
% GENERATED LATEX
|
|
\input{graphs/EquivSetXSetX.tex}
|
|
% END OF GENERATED LATEX
|
|
\end{center}
|
|
|
|
where $\coprod$ is the coproduct of $\Set$ and $\pi_1$ is the first projection of the coproduct.
|
|
|
|
Morphisms are translated using the same logic.
|
|
|
|
\paragraph{Category of models of the two-sort sort specification}
|
|
\label{sec:categoryOfModelsOfTwoSorts}
|
|
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 $\FamSet$, defined as $(X:\Set) \times \Set^X$. However, we will rather use another category : $\TSet$, the category of presheaves over the category $\TT$, the category with two object and one non-trivial arrow between them. The objects and morphism of $\TT$ are described below:
|
|
|
|
\begin{center}
|
|
% YADE DIAGRAM CategoryTT.json
|
|
% GENERATED LATEX
|
|
\input{graphs/CategoryTT.tex}
|
|
% END OF GENERATED LATEX
|
|
\end{center}
|
|
|
|
This category is equivalent to the catgegory $\FamSet$, as $(X : \Set) \times \Set^X$ is equivalent to $(X : \Set) \times (\Set/X)$ (as seen above), which is isomorphic to $\TSet$ (both categories consists of two sets and one arrow between them).
|
|
|
|
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{$K$ functor}
|
|
|
|
We define a helper functor $K : (X:C) \times (\Set/A(X)) \to \TSet$ defined as follows
|
|
\[
|
|
K_X(X,(Y,f)) = \TSetObject{Y}{f}{A(X)}
|
|
\]
|
|
The morphisms are translated as-is.
|
|
|
|
\begin{remark}
|
|
This functor can be constructed using the formal construction of the Grothendieck construction as a pullback in the category of categories $\Cat$
|
|
\end{remark}
|
|
|
|
\subsection{Initialization}
|
|
In this subsection, we will build the objects of the first step of our induction. This will correspond to the empty sort specification, i.e. the induction step $i = 0$.
|
|
|
|
\begin{itemize}
|
|
\setlength\itemsep{-1ex}
|
|
\item $\CC_0$ is $\one$, the category with only one object $\star$ and one trivial morphism (i.e. the terminal category of $\Cat$), because the empty sort specification only has one model.
|
|
\item $\BB_0$ is $\TSet$, the category of models of the $(\mathcal{O},\El)$ sort specification (see dedicated paragraph in last subsection for a description).
|
|
\item The universal property of $\tl^0$ is that of the coproduct. Therefore, we will define $\tl^0 : \BB_0 \times \BB_0 \to \BB_0$ to be the coproduct $\oplus$ of $\TSet$, with $\inj_\tl^0 : X \to X \oplus Y$ being the first injector of the coproduct. The second injector of the coproduct $\oplus$ will be refered as $\inj_2$.
|
|
\item $F_0 : \TSet \to \one$ is the terminal functor of $\Cat$
|
|
\item $G_0 : \one \to \TSet$ is the functor that sends the only object of $\one$ to the initial object of $\TSet$: $0_\TSet$
|
|
\item For $X$ an object of $\TSet$, we have
|
|
\[\Hom(G_0 \star,X) = \Hom(0_\TSet,X) \cong \one \cong \Hom(\star,F_0 X)\]
|
|
(reminder: $\star$ is the only object of $\one$)
|
|
Therefore, we have that $F_0 \vdash G_0$.
|
|
\item $F_0G_0 : \one \to \one$ so $F_0G_0 = \Id_\one$ as $\one$ is terminal in $\Cat$
|
|
\item $F_i\inj_1 = \id_\star$ which is an isomorphism
|
|
\end{itemize}
|
|
|
|
|
|
\subsection{Inductive Step: Constructing the categories}
|
|
|
|
\label{sec:constructingCategory}
|
|
In this part, i will show how we construct recursively both categories $\CC_i$ and $\BB_i$, along with the functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$. We will use the loop invariants that we expressed in the introduction of this section.
|
|
|
|
In order to construct the categories, we need some object describing the specific sort we are adding to the categories. This object is a specific functor $H_i : \CC_{i-1} \to \Set$. Those functors are the same that Altenkirsh and al. \cite{Altenkirch2018} used in their paper to describe a specification of sorts.
|
|
We suppose that those $H_i$ functors are given.
|
|
|
|
\begin{remark}
|
|
There is a way of getting the functor $H_i$ from the syntax, which is described in \autoref{sec:HiFromSyntax}.
|
|
\end{remark}
|
|
|
|
\subsubsection{Constructing $\CC_i$}
|
|
|
|
We construct the category $\CC_i$ as the following Grothendieck pair:
|
|
\[
|
|
\CC_i := (X : \CC_{i-1}) \times \left(\Set\middle/H_i(X)\right)
|
|
\]
|
|
and where $H_i$ is the specific functor described above.
|
|
|
|
\paragraph{An example of $H_i$ functors}
|
|
Let us now give an example of those $H_i$ objects for our type theory example.
|
|
|
|
\[
|
|
\boxed{\Con : \Set}
|
|
\]
|
|
We begin with the following functor, corresponding to the sort declaration above
|
|
\[
|
|
H_1(\star) = 1 \in \Set
|
|
\]
|
|
|
|
This corresponds to the fact that $\Con$ takes no parameter.
|
|
|
|
Therefore $\CC_1 = 1 \times \Set^1 \simeq \Set$, which is as expected: a model $X$ consists of a set $X_\Con$.
|
|
|
|
\[
|
|
\boxed{\Ty : (\Gamma : \Con) \to \Set}
|
|
\]
|
|
|
|
Then, we take the functor $H_2(X) = X_\Con$, corresponding to the sort declaration above. This functor means that types need \emph{one} context to be built.
|
|
|
|
Therefore $\CC_2 = (X:\Set) \times (\Set/X) \simeq (X:\Set) \times (\Set^X) = \FamSet$, a model $X$ is a family of sets $\left(X_\Ty(\Gamma)\right)_{\Gamma \in X_\Con}$, as expected.
|
|
|
|
\[
|
|
\boxed{\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set}
|
|
\]
|
|
|
|
Finally, we take the functor $H_3(X) = \sum_{\Gamma : X_\Con}X_\Ty(\Gamma)$. It means that terms need \emph{one} context, and \emph{one} type of that context.
|
|
|
|
An object of that final category $\CC_3$ is a triple
|
|
\[
|
|
(X_\Con: \Set, X_\Ty : X_\Con \to \Set, X_\Tm : (\Delta: X_\Con) \to X_\Ty(\Delta) \to \Set)
|
|
\]
|
|
\subsubsection{Constructing $\BB_i$}
|
|
|
|
We construct the category $\BB_i$ as follows.
|
|
|
|
An object of $\BB_i$ is a pair of:
|
|
\begin{itemize}
|
|
\item an object $X$ of $\BB_{i-1}$
|
|
\item a \enquote{sort constructor} $\Cstr^X$ as a function $H_iF_{i-1}X \to (R_0^{i-1}X)_\UU$
|
|
\newline
|
|
where $H_i$ is the functor $\CC_{i-1} \to \Set$ described above and $F_{i-1}$ is the right part of the adjunction $\BB_{i-1} \to \CC_{i-1}$ that we have defined at the previous induction step.
|
|
\end{itemize}
|
|
|
|
If we have an object $X$ of $\BB_i$, the first component is denoted as $R_{i-1}^iX$, which is an object of $\BB_{i-1}$, and the second component is denoted as $\Cstr^X : R_{i-1}^i X \to (R_0^iX)_\UU$.
|
|
|
|
A morphism $X \to X'$ of $\BB_i$ is a morphism $f : R_{i-1}^iX \to R_{i-1}^iX'$ 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}
|
|
|
|
For a morphism $f : X \to X'$ of $\BB_i$, we denote as $R_{i-1}^if$ the underlying morphism $R_{i-1}^i X \to R_{i-1}^i X'$.
|
|
|
|
Identities and compositions are that of the category $\BB_{i-1}$, and categorical equalities are trivially derived from the diagram above.
|
|
|
|
$R_{i-1}^i$ acts on objects and morphisms, and induces a functor $\BB_i \to \BB_{i-1}$. The induced functor is monadic, and therefore preserves limits.
|
|
|
|
\subsection{Inductive step: Constructing the functors $F_i$ and $G_i$}
|
|
|
|
The adjunction $F_i \vdash G_i$ is built using the two functors from the adjunction $F_{i-1} \vdash G_{i-1}$ defined in the previous induction step. We use them to define the first part of the adjunction, and we compose them with two adjoint functors $W$ and $E$ that we will define in this section. The overall construction for this induction step is as follows:
|
|
|
|
\begin{center}
|
|
% YADE DIAGRAM G2.json
|
|
% GENERATED LATEX
|
|
\input{graphs/G2.tex}
|
|
% END OF GENERATED LATEX
|
|
\end{center}
|
|
|
|
Where
|
|
\[
|
|
(F_{i-1} \times \id)(X,\underset{y : Y \to F_{i-1}(X)}{(Y,y)}) = (F_{i-1}X,\underset{y : Y \to F_{i-1}X}{(Y,y)})
|
|
\]
|
|
\[
|
|
(F_{i-1} \times \id)(f,g) = (F_{i-1}f,g)
|
|
\]
|
|
and
|
|
\[
|
|
(G_{i-1} \times (H_i\eta_{i-1} \circ \dash))(X,\underset{y : Y \to H_iX}{(Y,y)}) = (G_{i-1}X,\underset{Y : Y \to H_i X \to H_iF_{i-1}(G_{i-1}X)}{(Y,H_i\eta_{i-1} \circ y)})
|
|
\]
|
|
\[
|
|
(G_{i-1} \times (H_i\eta_{i-1} \circ \dash))(f,g) = (G_{i-1}f,g)
|
|
\]
|
|
with $\eta_{i-1} : X \to F_{i-1}G_{i-1}X$ being the unit of the adjunction $F_{i-1} \vdash G_{i-1}$.
|
|
|
|
These equations define two functors, that create the following adjunction:
|
|
\[F_{i-1} \times \id \vdash G_{i-1} \times (H_i\eta_{i-1} \circ \dash)\]
|
|
|
|
The unit of this adjunction is $\eta_{i-1} \times (H_i\eta_{i-1}\circ \dash)$ and its counit is $\varepsilon_{i-1} \times \id$, where $\varepsilon_{i-1}$ is the counit of the adjunction $F_{i-1} \vdash G_{i-1}$
|
|
|
|
\subsubsection{W definition}
|
|
|
|
We define a functor $W : \left(\left(X : \BB_{i-1}\right) \times \Set/H_iF_{i-1}X\right) \to \BB_{i}$
|
|
|
|
The action on objects is as follows:
|
|
\[
|
|
W(X,Y) := \left(X \tl^{i-1} K_{H_iF_{i-1}}(X,Y), \widetilde{\inj_2} \right)
|
|
\]
|
|
|
|
With $\widetilde{\inj_2}$ being defined by the composition
|
|
\begin{center}
|
|
% YADE DIAGRAM Wdef.json
|
|
% GENERATED LATEX
|
|
\input{graphs/Wdef.tex}
|
|
% END OF GENERATED LATEX
|
|
\end{center}
|
|
|
|
The action on a morphism $(g,h)$ from $(X,Y)$ to $(X',Y')$ is the following:
|
|
\[
|
|
W(g,h) := \left(g \tl^{i-1} K_{H_iF_{i-1}}(g,h)\right)
|
|
\]
|
|
|
|
It is indeed a morphism of $\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{Inductive Step: Proof of the adjunction}
|
|
|
|
In this subsection, we prove that $(W,E)$ make an adjunction by 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$, a natural isomorphism $\phi_{XYZ}$.
|
|
|
|
\[
|
|
\phi_{XYZ} : \Hom(W(X,Y),Z) \to \Hom((X,Y),E(Z))
|
|
\]
|
|
|
|
I will present how the isomorphisms and its inverse are constructed. The proof that $\phi_{XYZ}$ and $\phi_{XYZ}^{-1}$ are inverse one of the other, and that they are natural 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 defined as the following composition:
|
|
|
|
\begin{center}
|
|
% YADE DIAGRAM PhiXYZFirstComponent.json
|
|
% GENERATED LATEX
|
|
\input{graphs/PhiXYZFirstComponent.tex}
|
|
% END OF GENERATED LATEX
|
|
\end{center}
|
|
|
|
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)$.
|
|
|
|
The morphism $\phi^{-1}_{XYZ}(g,h)$ of $\BB_i$ from $W(X,Y)$ to $Z$ is a morphism of $\BB_{i-1}$ from $X \tl^{i-1} K_{H_iF_{i-1}} (X,Y)$ to $R_{i-1}^i(Z)$ that make a specific diagram commute. We build this morphism using the universal property of $\tl^{i-1}$, stated in \autoref{sec:tlUniversalProperty}
|
|
|
|
\[
|
|
\phi^{-1}_{XYZ}(g,h) := \left\{g ; \square \right\}
|
|
\]
|
|
|
|
\todo{Est-ce qu'il faut que j'écrive $R_{i-1}^i\phi^{-1}_{XYZ}(g,h) := ...$ pour être plus «homogène» ?}
|
|
|
|
Where $\square$ is a morphism $K_{H_iF_{i-1}} (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}
|
|
|
|
Finally, we check that $\phi^{-1}_{XYZ}(g,h)$ is a morphism of $\BB_i$ from $W(X,Y)$ to $Z$, i.e. that it makes the following diagram commute:
|
|
|
|
\begin{center}
|
|
% YADE DIAGRAM D8.json
|
|
% GENERATED LATEX
|
|
\input{graphs/D8.tex}
|
|
% END OF GENERATED LATEX
|
|
\end{center}
|
|
|
|
In order to complete this proof, we need to show that
|
|
\begin{itemize}
|
|
\item $\phi_{XYZ}^{-1} \circ \phi_{XYZ} (f) = f$
|
|
\item $\phi_{XYZ} \circ \phi_{XYZ}^{-1} (g,h) = (g,h)$
|
|
\item $\phi_{XYZ}$ is natural.
|
|
\end{itemize}
|
|
|
|
The proofs of these statements are given in \autoref{apx:phi-WE-isnat}.
|
|
|
|
|
|
|
|
\subsubsection{Coreflection}
|
|
|
|
We have proven that this newly created adjunction $F_i \vdash G_i$ create a coreflection. It means that $F_iG_i \cong \Id_{\CC_i}$, or equivalently that $G_i$ is full and faithful.
|
|
|
|
The proof is that statement is given in \autoref{apx:FG-refl}.
|
|
|
|
\subsection{Inductive step: $\tl^i$}
|
|
|
|
\label{sec:coproductConstr}
|
|
|
|
\paragraph{Constructing the objects}
|
|
We will define the $\tl^i$ operator of two objects $X$ from $\BB_i$ and $Y$ from $\BB_0$ as follows:
|
|
\[
|
|
X \tl_i Y := \left((R_{i-1}^i X) \tl^{i-1} Y, (R_0^{i-1} \inj_\tl^{i-1})_\UU \circ \Cstr_i^X \circ (H_iF_{i-1}\inj_\tl^{i-1})^{-1}\right)
|
|
\]
|
|
|
|
The constructor goes as follows:
|
|
|
|
\begin{center}
|
|
% YADE DIAGRAM TlConstructor.json
|
|
% GENERATED LATEX
|
|
\input{graphs/TlConstructor.tex}
|
|
% END OF GENERATED LATEX
|
|
\end{center}
|
|
|
|
The injector $\inj_\tl^i : X \to X \tl^i Y$ is defined as follows:
|
|
\[
|
|
\inj_\tl^i := \inj_\tl^{i-1} : R_{i-1}^i X \to R_{i-1}^i (X \tl^i Y) = R_{i-1}^i X \tl^{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}
|
|
|
|
\paragraph{Universal Property}
|
|
We will now show that that the universal property stated in \autoref{sec:tlUniversalProperty} holds.
|
|
To that end, we take two objects $X$ and $Z$ in $\BB_i$, $Y$ in $\BB_0$, a morphism $g : X \to Z$ in $\BB_i$ and a morphism $h : Y \to R_0^iZ$ in $\BB_0$. We want to build a morphism $\{g,h\}$ of $\BB_i$ such that the following two diagrams commute.
|
|
|
|
\begin{center}
|
|
% YADE DIAGRAM TlUniversal.json
|
|
% GENERATED LATEX
|
|
\input{graphs/TlUniversal.tex}
|
|
% END OF GENERATED LATEX
|
|
\end{center}
|
|
|
|
We define $\{g ; h\}_i = \{R_{i-1}^i g ; h\}_{i-1}$. This is 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}
|
|
|
|
With this definition, the isomorphism $\en_{i-1}^i : (R_{i-1}^i X) \tl^{i-1} Y \to R_{i-1}^i(X \tl^i Y)$ is simply the identity morphism.
|
|
|
|
\paragraph{Building morphisms}
|
|
|
|
For any two morphisms $g : X \to X'$ of $\BB_i$ and $h : Y \to Y'$ of $\BB_0$, we will create a morphism $X \tl^i Y \to X' \tl^i Y'$ as follows:
|
|
\[
|
|
g\tl^ih := R_{i-1}^ig \tl^{i-1} h
|
|
\]
|
|
\todo{Même question d'homogénéité}
|
|
|
|
This is indeed a morphism of $\BB_i$ as it makes the following diagram commute:
|
|
|
|
\begin{center}
|
|
% YADE DIAGRAM TlDefOnMorphisms.json
|
|
% GENERATED LATEX
|
|
\input{graphs/TlDefOnMorphisms.tex}
|
|
% END OF GENERATED LATEX
|
|
\end{center}
|
|
|
|
\paragraph{Composition with $F_i$}
|
|
We finally need to prove, for any objects $X$ in $\BB_i$ and $Y$ in $\TSet$, that the morphism
|
|
$F_i(\inj_\tl^i) : F_iX \to F_i(X \tl^i Y)$ is an isomorphism.
|
|
|
|
Morphisms $\BB_{i}$ are morphisms of $\BB_{i-1}$ that follows some equations, and composition is the same. Moreover, we know from the definition above that $R_{i-1^i} \inj_\tl^i := \inj_\tl^{i-1}$.
|
|
|
|
So, we just need to know that $R_{i-1}^i(F_{i-1}\inj_\tl^i)$ is an isomorphism.
|
|
|
|
\[
|
|
R_{i-1}^iF_i\inj_\tl^i = \left[(F_{i-1} \times \id) (E(\inj_\tl^i))\right]_1 = \left[(F_{i-1} \times \id) (R_{i-1}^i \inj_\tl^i,!)\right]_1 = F_{i-1} \inj_\tl^{-1}
|
|
\]
|
|
|
|
And we know from the previous induction step that $F_{i-1}\inj_\tl^{i-1}$ is an isomorphism. Therefore, $F_i\inj_\tl^i$ is an isomorphism.
|
|
|
|
\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), \lambda a.\lambda \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{Adding 2-transformation of constructors}
|
|
\label{sec:constructors2trans}
|
|
\todo{Describe the process}
|
|
|
|
\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}
|
|
|
|
\subsection{Consructing the $H_i$ functors from the syntax}
|
|
\label{sec:HiFromSyntax}
|
|
|
|
\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(\phi_{XYZ}^{-1}(g,h)) \circ \inj_\tl^{i-1} = \left\{g ; \square \right\} \circ \inj_\tl^{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}
|
|
|
|
|
|
\todo{Justifier que la partie du haut commute, i.e. que \[
|
|
(R_0^{i-1}\{g,\square\})_\El \circ (\en_0^i)_\El \circ (\inj_2)_\El = \square_\El
|
|
\]}
|
|
|
|
The diagram commutes, and so we can deduce that the second component of $\phi_{XYZ}(f)$ is $h$, by proprty of the pullback $E(Z)$
|
|
|
|
\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_\tl^{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)) = f$. By definition of $\{;\}$ in $\BB_i$, it suffices to show that $\square = R_0^i f \circ \en_0^{i-1} \circ \inj_2$.
|
|
|
|
The two required equalities are proved by the diagram above:
|
|
|
|
\begin{align*}
|
|
\square_\El = \left(R_0^i f \circ \en_0^{i-1} \circ \inj_2\right)_\El \\
|
|
\square_\UU = \left(R_0^i f \circ \en_0^{i-1} \circ \inj_2\right)_\UU
|
|
\end{align*}
|
|
|
|
\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_{X'Y'Z'}(f \circ \ii \circ W(g,h))_1
|
|
&=& R_{i-1}^i\left(f \circ \ii \circ (g \tl^{i-1} K_\bullet(g,h))^+\right) \circ \inj_\tl^{i-1} \\
|
|
&=& R_{i-1}^i f \circ R_{i-1}^i \ii \circ (g \tl^{i-1} K_\bullet(g,h)) \circ \inj_\tl^{i-1} \\
|
|
&=& R_{i-1}^i f \circ R_{i-1}^i \ii \circ \inj_\tl^{i-1} \circ g \\
|
|
&=& \left[E(f) \circ \phi_{XYZ}(\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 inner blue line. And that of $\phi_{X'Y'Z'}(\ii)$ is defined by the red outer line.
|
|
The outer squares commute, and therefore, by the pullback property, we get that
|
|
\[
|
|
\phi_{X'Y'Z'}(f\circ\ii\circ W(g,h))_2 = \left[E(f) \circ \phi_{XYZ}(\ii) \circ (g,h)\right]_2
|
|
\]
|
|
|
|
And thus we have naturality.
|
|
|
|
|
|
\section{$F_i \vdash G_i$ reflection}
|
|
\label{apx:FG-refl}
|
|
|
|
We want to find, for each object $(X,(B,g))$ of $\CC_i = (X : \CC_{i-1}) \times (\Set/H_i(X))$, an isomorphism $(X,(B,g)) \to F_iG_i(X,(B,g))$. $g$ is a morphism from $B$ to $H_i(X)$
|
|
|
|
\[\begin{array}{rcl}
|
|
F_iG_i(X,(B,g))
|
|
&=& F_iW_i(G_{i-1}X,(B,H_i\eta_{i-1}\circ g))\\
|
|
&=& F_i\left(G_{i-1}X \tl^{i-1}K_\bullet(G_{i-1}X,(B,H_i\eta_{i-1}\circ g)),\widetilde{\inj_2}\right)\\
|
|
&=&(F_{i-1} \times \id)\left(G_{i-1}X \tl^{i-1}K_\bullet(G_{i-1}X,(B,H_i\eta_{i-1}\circ g)),(A,h)\right)\\
|
|
&=&\left(F_{i-1}(G_{i-1}X \tl^{i-1}K_\bullet(G_{i-1}X,(B,H_i\eta_{i-1}\circ g))),(A,h)\right)
|
|
\end{array}\]
|
|
|
|
Where $(A,h)$ is the pullback defined as
|
|
\begin{center}
|
|
% YADE DIAGRAM E1.json
|
|
% GENERATED LATEX
|
|
\input{graphs/E1.tex}
|
|
% END OF GENERATED LATEX
|
|
\end{center}
|
|
|
|
We can extend this pullback with the two isomorphisms $\en_0^i$ and $H_iF_{i-1}(\inj_\tl^{i-1})$ in another pullback. This new pullback is over the injection morphism $\inj_2$ of the coproduct of $\TSet$, so the new pullback object is the second component of the $\bullet \oplus B$ i.e. $B$.
|
|
|
|
\begin{center}
|
|
% YADE DIAGRAM E2.json
|
|
% GENERATED LATEX
|
|
\input{graphs/E2.tex}
|
|
% END OF GENERATED LATEX
|
|
\end{center}
|
|
|
|
The first component of the isomorphism is the following isomorphism, where $\eta_{i-1}^{FG}$ if the counit of the adjunction $F_{i-1} \vdash G_{i-1}$, that we know to be an isomorphism from the induction hypothesis.
|
|
|
|
\begin{center}
|
|
% YADE DIAGRAM E3.json
|
|
% GENERATED LATEX
|
|
\input{graphs/E3.tex}
|
|
% END OF GENERATED LATEX
|
|
\end{center}
|
|
|
|
And the second component is made using the isomorphism constructed by the pullback, that makes the diagram commute.
|
|
\begin{center}
|
|
% YADE DIAGRAM E4.json
|
|
% GENERATED LATEX
|
|
\input{graphs/E4.tex}
|
|
% END OF GENERATED LATEX
|
|
\end{center}
|
|
|
|
|
|
\end{document}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|