856 lines
35 KiB
TeX
856 lines
35 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 $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 declaration therefore describes the sets that the model contains.
|
||
|
||
\paragraph{Constructor specification}
|
||
We can also add constructors to a sort specification to make a complete GAT. Those constructors rather describe elements of the sets contained in the model, previously defined by the sort declaration.
|
||
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$, an element$\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.
|
||
\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 has not been formally justified, although it has been used like in Phipippo Sestini's thesis.
|
||
|
||
\todo{choose}
|
||
|
||
\begin{quote}
|
||
Many instances of multi-sorted IITs [IITs are variants 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 undestrand the relationship between the categories of models of an original GAT and the category of models of the transformed GAT, in order to legitimate this transformation.
|
||
|
||
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)$. This forgetful $R$ functor is a composition of monadic functors, one for each sort declaration.
|
||
|
||
\todo{J'ai toujours pas regardé les terms constructors, je peux le mettre, mais je ne serais pas sûr de pouvoir le défendre}
|
||
|
||
\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, we will rather 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.
|
||
|
||
\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 the equivalence $\Set/X \simeq \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 formal construction of the Grothendieck construction as a pullback in the category of categories $\Cat$
|
||
\end{remark}
|
||
|
||
\subsection{Constructing the categories}
|
||
|
||
We will construct both categories $\CC$ and $\BB$ sort declaration by sort declaration in one big recursive process. At each step, we will build the categories $\CC_i$ and $\BB_i$, the adjunction $F_i \vdash G_i$, 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. Likewise, $\BB_i$ will 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 category with one object and one morphism (i.e. the terminal element of $\Cat$). $\lambda. \star$ is the terminal morphism of this object, and its right adjoint sends the only object of $1$ to the terminal object of the category $\TSet$.
|
||
|
||
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(X)\right) = (X : \CC_{i-1}) \times \left(\Set^{H_i(X)}\right)
|
||
\]
|
||
and where $H_i$ is a specific functor $\CC_{i-1} \to \Set$, such that $H_i(X)$ is the set of parameters for the construction of the new sort.
|
||
|
||
\todo{Do we need this functor to be representable. If so, precise it}
|
||
|
||
\paragraph{$H_i$ functors for our Type Theory example}
|
||
Let us give 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 :/}
|
||
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,\Rtsc)
|
||
&=& F_iW_i(G_{i-1}X,\Rtsc)\\
|
||
&=& F_i(G_{i-1}X \oplus L_0^{i-1}H_\bullet(G_{i-1}X,\Rtsc),\widetilde{\inj_2})\\
|
||
&=&(F_{i-1} \times \id)\left(G_{i-1}X \oplus L_0^{i-1}\Hbar_\bullet(G_{i-1}X,\Rtsc),(A,h)\right)\\
|
||
&=&\left(F_{i-1}(G_{i-1}X \oplus L_0^{i-1}\Hbar_\bullet(G_{i-1}X,\Rtsc)),(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 using the two isomorphisms given by the induction hypothesis and hypothesis H3.
|
||
|
||
\begin{center}
|
||
% YADE DIAGRAM E2.json
|
||
% GENERATED LATEX
|
||
\input{graphs/E2.tex}
|
||
% END OF GENERATED LATEX
|
||
\end{center}
|
||
|
||
\end{document}
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|