739 lines
32 KiB
TeX
739 lines
32 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{Sort specification}
|
||
|
||
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 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 : \Set$
|
||
\item A family of sets $\left(X_\Ty\left(\Gamma\right)\right)_{\Gamma \in _\Con}$
|
||
\item A family of sets $\left(X_\Tm\left(\Delta,A\right)\right)_{\Delta\in X_\Con,\: A \in X_\Ty\left(\Delta\right)}$
|
||
\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{eq}: (\Gamma : \Con) \to (A : \Ty\;\Gamma) \to$
|
||
|
||
$\qquad\Tm\;\Gamma A \to \Tm\;\Gamma A \to \Ty\;\Gamma$ & In any context $\Gamma$ and type $A$ in this context, for every terms $t$,$u$ of the type $A$, we have a type $\operatorname{eq} \Gamma A t u$ describing the equality of the terms.
|
||
\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$, for each $A \in X_\Ty(\Gamma)$, for each elements $u,v \in X_\Tm(\Gamma,A)$, an element $\operatorname{eq}\;\Gamma\;A\;u\;v \in X_\Ty(\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. This process is used by Philippo Sestini in his thesis \cite{SestiniPhD} refering the work of Zongpu Szumi Xie \cite{AmbrusSzumiXie2sort}:
|
||
|
||
\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}
|
||
|
||
The goal of this document is to prove semantically that this transformation makes sense. More specifically, we prove that this transformation is a left adjunct functor of a coreflection. This is enough to prove what Sestini conjectured, i.e. that the initial object in the 2-sort category creates back the initial object of the primary category \cite[5. General]{nlab:reflective_subcategory}.
|
||
|
||
We will now present this transformation. The sort specification of the transformed GAT is always the same, and contains two sort declarations (as planned):
|
||
|
||
\vspace{1em}
|
||
\begin{tabular}{p{0.37\textwidth}|p{0.5\textwidth}}
|
||
$\mathcal{O} : \Set$ & The set of sorts \\
|
||
$\underline{\;\bullet\;} : \mathcal{O} \to \Set$ & For every sort object $o$ in the set of sorts, a set called $\underline{o}$ of objects corresponding to the sort object.
|
||
\end{tabular}
|
||
\vspace{1em}
|
||
|
||
Category of models of this two-sort specification are intuitively the category of families of set $\FamSet$, composed of pairs $\left(X_0:\Set,X_1: X_0 \to \Set\right)$.
|
||
|
||
Then, we replace all occurrences of $\Set$ to $\mathcal{O}$, and we apply underline 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 \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 \enquote{$\operatorname{unit} \Gamma$} corresponding to the sort object $\Ty\;\Gamma$\\
|
||
$\operatorname{eq}: (\Gamma : \underline{\Con}) \to (A : \underline{\Ty\;\Gamma}) \to$ \newline
|
||
$\qquad\underline{\Tm\;\Gamma A} \to \underline{\Tm\;\Gamma A} \to \underline{\Ty\;\Gamma}$ &
|
||
$\dots$
|
||
\end{tabular}
|
||
|
||
\paragraph{$\FamSet$ as functors}
|
||
|
||
In the rest of the document, we will denote the simple category containing two elements and one non-identity arrow between them 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}
|
||
|
||
The functors over this categories are equivalent to families of sets, using the following mapping :
|
||
|
||
\[
|
||
\begin{array}{l|l}
|
||
X_\UU = X_0 & X_0 = X_\UU \\
|
||
X_\El = \displaystyle\coprod_{A\in X_0}X_1(A) & X_1 = A \mapsto X_p^{-1}(\{A\})\\
|
||
X_p = (A,B) \mapsto A &
|
||
\end{array}
|
||
\]
|
||
|
||
Therefore the categories of sorts of the transformed GATs will be built atop of the category $\TSet$ rather than atop of the category $\FamSet$ as it makes the formal proofs more elegant.
|
||
|
||
\paragraph{Goal}
|
||
|
||
The goal of this document is to make a relation between the category of models of the GAT $\CC$ and the category of models of the two-sortified GAT $\BB$. This relation will be an adjunction $F \vdash G$ that we will prove to be a coreflection.
|
||
|
||
The category $\BB$ is built with an adjunction $R \vdash L$ to the category of models of the simple two-sort specification of sorts $\TSet$.
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM G1-0.json
|
||
% GENERATED LATEX
|
||
\input{graphs/G1-0.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
\subsection{Constructing the categories}
|
||
|
||
We will construct both categories $\CC$ and $\BB$ recursively, adding new sorts one by one.
|
||
The categories $\CC_i$ are described as in Fiore's paper \cite{Fiore2008}, and the categories $\BB_i$ are constructed atop of the category $\TSet$ with a method inspired by the category of models described by Altenkirch et al. \cite{Altenkirch2018}.
|
||
|
||
The overall 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$.
|
||
|
||
\subsubsection{Constructing $\CC_i$}
|
||
|
||
We construct the category $\CC_i$ as the following pair:
|
||
\[
|
||
\CC_i = (X : \CC_{i-1}) \times \Set^{\Hom(O_i,X)} \qquad\text{(this is a dependent coproduct)}
|
||
\]
|
||
where $O_i$ is a specific object of the category $\CC_{i-1}$, such that $\Hom(O_i,X)$ is the set of parameters for the construction of the new sort.
|
||
|
||
For example, for our type theory example, we first have
|
||
\[
|
||
O_1 = \star \in \operatorname{Obj}(\CC_0) = \operatorname{Obj}(1)
|
||
\]
|
||
so $\Hom(O_1,X) = 1$, which corresponds to the fact that $\Con$ takes no parameter.
|
||
|
||
Therefore $\CC_1 = 1 \times \Set^1 = \Set$
|
||
|
||
Then, we take the singleton object $O_2 = 1$ (this means, that types need \emph{one} context to be built), and so, for a set $X_\Con$, $\Hom(O_2,X_\Con) \cong X_\Con$, which corresponds to the fact that $\Ty$ take one $\Con$ as a parameter.
|
||
|
||
Therefore $\CC_2 = (X:\Set) \times \Set^X \cong \FamSet$.
|
||
|
||
Finally, we take the object $O_3 = (1, \lambda \star . 1)$ (this means that terms need \emph{one} context, and \emph{one} type of that context). With this object, for a pair $(X_\Con,X_\Ty)$ in $\CC_2$, we have $\Hom(O_3,(X_\Con,X_\Ty)) \cong \left(\Gamma: X_\Con, A: X_\Ty(\Gamma)\right)$.
|
||
|
||
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 object $O_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 $\Hom_{\BB_{i-1}} (G_{i-1}O_i,X) \to (R_0^{i-1}X)_\UU$
|
||
\newline
|
||
where $O_i$ is the object of $\CC_{i-1}$ that describe the sort constructor being processed, and $G_{i-1}$ is the left part of the adjunction $\CC_{i-1} \to \BB_{i-1}$ that we are defining recursively at the same time.
|
||
\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 adjunct} of another functor we call $L_{i-1}^i$.
|
||
|
||
As we can compose the adjunctions $R_0^1$,$R_1^2$,...,$R_{i-1}^i$, we will create the two following syntactic sugars for the composed adjunctions.
|
||
\[\begin{array}{c}
|
||
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}
|
||
\end{array}\]
|
||
|
||
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$.
|
||
\end{remark}
|
||
|
||
|
||
\subsection{Constructing the adjunction}
|
||
We will now construct the adjunction $F_i \vdash G_i$ at the step $i$.
|
||
|
||
\subsubsection{Hypotheses}
|
||
|
||
In order to build and prove the adjunction, we will state hypotheses that we will progressively prove during our building of $\BB_i$, $F_i$, and $G_i$.
|
||
|
||
\begin{property}[H1]
|
||
\[
|
||
\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)}
|
||
\]
|
||
is an equivalence.
|
||
\end{property}
|
||
|
||
\begin{property}[H1r]
|
||
\[
|
||
\simpleArrow{ R_{0}^i X \oplus_{i-1} Y}{\left\{R_{i-1}^i \inj_1^i ; \eta_{i-1}^i\right\}}{R_{i-1}^i(X \oplus_i L_0^i Y)}
|
||
\]
|
||
is an equivalence.
|
||
|
||
This property is proven easily by recursion over previous property H1.
|
||
\end{property}
|
||
|
||
\begin{property}[H3]
|
||
\[
|
||
\simpleArrow{F_i X}{F(\inj_1^i)}{F_i(X \oplus L_0^i Y)}
|
||
\]
|
||
is an equivalence.
|
||
\end{property}
|
||
|
||
\begin{property}[H3']
|
||
\[
|
||
\simpleArrow{\Hom(G_i\Gamma, X)}{(inj_1^i \circ \dash)}{\Hom(G_i\Gamma,X \oplus L_0^i Y)}
|
||
\]
|
||
is an equivalence.
|
||
|
||
This proven with the adjunction property of $F_i \vdash G_i$ and H3, as w have that
|
||
\[
|
||
\Hom(G_i \Gamma, X) \cong \Hom(\Gamma, F_i X) \cong \Hom(\Gamma, F_i(X \oplus L_0^i Y)) \cong \Hom(G_i \Gamma, X \oplus L_0^i Y)
|
||
\]
|
||
\end{property}
|
||
|
||
\subsubsection{Decomposing the proof}
|
||
|
||
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}
|
||
|
||
The category $\left[S_i, \Set\right]$ is seen as the category $\left[S_{i-1},\Set\right]$ to which we have added an object along with morphisms described by $\Gamma_i$. The morphisms we added to the object $X$ have the shape of the slice category of the set $\Hom(\Gamma_i,X)$.
|
||
|
||
The first part $G_{i-1} \times \id \dashv F_{i-1} \times \id$ is proven and defined as an adjunction from the last step of the recurrence.
|
||
|
||
We will now define the two functors.
|
||
|
||
|
||
\subsubsection{W definition}
|
||
|
||
We define a functor $W : \displaystyle\sum_{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.
|
||
|
||
\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 \displaystyle\sum_{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:
|
||
|
||
\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}
|
||
|
||
|
||
\subsubsection{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 $\displaystyle\prod_{X : \BB_{i-1}} (\Set/\Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,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}.
|
||
|
||
\paragraph{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}
|
||
|
||
\paragraph{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$ 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.
|
||
|
||
|
||
|
||
\subsection{$F \vdash G$ make a reflection}
|
||
|
||
\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:
|
||
|
||
\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-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 \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 ?)}
|
||
|
||
\subsection{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.
|
||
|
||
|
||
\end{document}
|
||
|
||
|
||
|
||
|