1633 lines
59 KiB
TeX
1633 lines
59 KiB
TeX
\chapter{Category Theory}
|
||
\label{ch:implementation}
|
||
The source code for this formalization, including this report, is
|
||
available as open source software at:
|
||
%
|
||
\begin{center}
|
||
\gitlink
|
||
\end{center}
|
||
%
|
||
All modules imported for this formalization can be browsed at this
|
||
link\footnote{%
|
||
In case the linked sources are unavailable the html
|
||
documentation can be generated by navigating to the root directory
|
||
of the project and executing \texttt{make html}.%
|
||
}:
|
||
%
|
||
\begin{center}
|
||
\doclink
|
||
\end{center}
|
||
The concepts formalized in this development are:
|
||
%
|
||
\begin{center}
|
||
\begin{tabular}{ l l }
|
||
Name & Module \\
|
||
\hline
|
||
Equivalences & \sourcelink{Cat.Equivalence} \\
|
||
Categories & \sourcelink{Cat.Category} \\
|
||
Functors & \sourcelink{Cat.Category.Functor} \\
|
||
Products & \sourcelink{Cat.Category.Product} \\
|
||
Exponentials & \sourcelink{Cat.Category.Exponential} \\
|
||
Cartesian closed categories & \sourcelink{Cat.Category.CartesianClosed} \\
|
||
Natural transformations & \sourcelink{Cat.Category.NaturalTransformation} \\
|
||
Yoneda embedding & \sourcelink{Cat.Category.Yoneda} \\
|
||
Monads & \sourcelink{Cat.Category.Monad} \\
|
||
Kleisli Monads & \sourcelink{Cat.Category.Monad.Kleisli} \\
|
||
Monoidal Monads & \sourcelink{Cat.Category.Monad.Monoidal} \\
|
||
Voevodsky's construction & \sourcelink{Cat.Category.Monad.Voevodsky} \\
|
||
Opposite category & \sourcelink{Cat.Categories.Opposite} \\
|
||
Category of sets & \sourcelink{Cat.Categories.Sets} \\
|
||
Span category & \sourcelink{Cat.Categories.Span} \\
|
||
\end{tabular}
|
||
\end{center}
|
||
%
|
||
\begin{samepage}
|
||
Furthermore the following items have been partly formalized:
|
||
%
|
||
\begin{center}
|
||
\begin{tabular}{ l l }
|
||
Name & Module \\
|
||
\hline
|
||
Category of categories & \sourcelink{Cat.Categories.Cat} \\
|
||
Category of relations & \sourcelink{Cat.Categories.Rel} \\
|
||
Category of functors & \sourcelink{Cat.Categories.Fun} \\
|
||
Free category & \sourcelink{Cat.Categories.Free} \\
|
||
Monoids & \sourcelink{Cat.Category.Monoid} \\
|
||
\end{tabular}
|
||
\end{center}
|
||
\end{samepage}%
|
||
%
|
||
As well as a range of various results about these. E.g.\ I have shown
|
||
that the category of sets has products. In the following I aim to
|
||
demonstrate some of the techniques employed in this formalization and
|
||
in the interest of brevity I will not detail all the things I have
|
||
formalized. In stead I have selected parts of this formalization that
|
||
highlight some interesting proof techniques relevant to doing proofs
|
||
in Cubical Agda. This chapter will focus on the definition of
|
||
\emph{categories}, \emph{equivalences}, the \emph{opposite category},
|
||
the \emph{category of sets}, \emph{products}, the \emph{span category}
|
||
and the two formulations of \emph{monads}.
|
||
|
||
One technique employed throughout this formalization is the idea of
|
||
distinguishing types with more or less homotopical structure. To do
|
||
this I have followed the following design-principle: I have split
|
||
concepts up into things that represent \emph{data} and \emph{laws}
|
||
about this data. The idea is that we can provide a proof that the laws
|
||
are mere propositions. As an example a category is defined to have two
|
||
members: $\var{raw}$ which is a collection of the data and
|
||
$\var{isCategory}$ which asserts some laws about that data.
|
||
|
||
This allows me to reason about things in a more ``standard
|
||
mathematical way'', where one can reason about two categories by
|
||
simply focusing on the data. This is achieved by creating a function
|
||
embodying the equality principle for a given type.
|
||
|
||
For the rest of this chapter I will present some of these results. For
|
||
didactic reasons no source-code has been included in this chapter. To
|
||
see the formal definitions the reader is referred to the
|
||
implementation which is linked in the tables above.
|
||
|
||
\section{Categories}
|
||
\label{sec:categories}
|
||
The data for a category consist of a type for the sort of objects; a
|
||
type for the sort of arrows; an identity arrow and a composition
|
||
operation for arrows. Another record encapsulates some laws about
|
||
this data: associativity of composition, identity law for the identity
|
||
morphism. These are standard constituents of a category and can be
|
||
found in typical mathematical expositions on the topic. We shall
|
||
impose one further requirement on what it means to be a category,
|
||
namely that the type of arrows form a set.
|
||
|
||
Such categories are called \nomen{1-categories}{1-category}. It is
|
||
possible to relax this requirement. This would lead to the notion of
|
||
higher categories (\cite[p. 307]{hott-2013}). For the purpose of this
|
||
thesis however, this report will restrict itself to
|
||
1-categories\index{1-category}. Generalizing this work to higher
|
||
categories would be a very natural extension of this work.
|
||
|
||
Raw categories satisfying all of the above requirements are called a
|
||
\nomenindex{pre-categories}. As a further requirement to be a proper category we
|
||
require it to be univalent. Before we can define this, I must introduce two more
|
||
definitions: If we let $p$ be a witness to the identity law, which formally is:
|
||
%
|
||
\begin{equation}
|
||
\label{eq:identity}
|
||
\var{IsIdentity} ≜
|
||
∏_{A, B \tp \Object} ∏_{f \tp \Arrow\ A\ B}
|
||
\left(\id \lll f ≡ f\right) \x \left(f \lll \id ≡ f\right)
|
||
\end{equation}
|
||
%
|
||
Then we can construct the identity isomorphism $\idIso \tp (\identity,
|
||
\identity, p) \tp A ≊ A$ for any object $A$. Here $≊$
|
||
denotes isomorphism on objects (whereas $\cong$ denotes isomorphism on
|
||
types). This will be elaborated further on in sections
|
||
\S\ref{sec:equiv} and \S\ref{sec:univalence}. Moreover due to
|
||
substitution for paths we can construct an isomorphism from \emph{any}
|
||
path:
|
||
%
|
||
\begin{equation}
|
||
\idToIso \tp A ≡ B → A ≊ B
|
||
\end{equation}
|
||
%
|
||
The univalence criterion for categories states that this map must be an
|
||
equivalence. The requirement is similar to univalence for types, but where
|
||
isomorphism on objects play the role of equivalence on types. Formally:
|
||
%
|
||
\begin{align}
|
||
\label{eq:cat-univ}
|
||
\isEquiv\ (A ≡ B)\ (A ≊ B)\ \idToIso
|
||
\end{align}
|
||
%
|
||
Note that \ref{eq:cat-univ} is \emph{not} the same as:
|
||
%
|
||
\begin{equation}
|
||
\label{eq:cat-univalence}
|
||
%% \tag{Univalence, category}
|
||
(A ≡ B) ≃ (A ≊ B)
|
||
\end{equation}
|
||
%
|
||
However the two are logically equivalent: One can construct the latter
|
||
from the former simply by ``forgetting'' that $\idToIso$ plays the
|
||
role of the equivalence. The other direction is more involved and will
|
||
be discussed in section \S\ref{sec:univalence}.
|
||
|
||
In summary the definition of a category is the following collection of
|
||
data:
|
||
%
|
||
\begin{align}
|
||
\Object & \tp \Type \\
|
||
\Arrow & \tp \Object → \Object → \Type \\
|
||
\identity & \tp \Arrow\ A\ A \\
|
||
\lll & \tp \Arrow\ B\ C → \Arrow\ A\ B → \Arrow\ A\ C
|
||
\end{align}
|
||
%
|
||
And laws:
|
||
%
|
||
\begin{align}
|
||
%% \tag{associativity}
|
||
h \lll (g \lll f) ≡ (h \lll g) \lll f \\
|
||
%% \tag{identity}
|
||
\left(
|
||
\identity \lll f ≡ f
|
||
\right)
|
||
\x
|
||
\left(
|
||
f \lll \identity ≡ f
|
||
\right)
|
||
\\
|
||
\label{eq:arrows-are-sets}
|
||
%% \tag{arrows are sets}
|
||
\isSet\ (\Arrow\ A\ B)\\
|
||
\tag{\ref{eq:cat-univ}}
|
||
\isEquiv\ (A ≡ B)\ (A ≊ B)\ \idToIso
|
||
\end{align}
|
||
%
|
||
$\lll$ denotes arrow composition (right-to-left), and reverse function
|
||
composition (left-to-right, diagrammatic order) is denoted $\rrr$. The objects
|
||
($A$, $B$ and $C$) and arrow ($f$, $g$, $h$) are implicitly universally
|
||
quantified.
|
||
|
||
With all this in place it is now possible to prove that all the laws
|
||
are indeed mere propositions. Most of the proofs simply use the fact
|
||
that the type of arrows are sets. This is because most of the laws are
|
||
a collection of equations between arrows in the category. And since
|
||
such a proof does not have any content exactly because the type of
|
||
arrows form a set, two witnesses must be the same. All the proofs are
|
||
really quite mechanical. Let us have a look at one of them: Proving
|
||
that \ref{eq:identity} is a mere proposition:
|
||
%
|
||
\begin{equation}
|
||
\isProp\ \var{IsIdentity}
|
||
\end{equation}
|
||
%
|
||
There are multiple ways to do this. Perhaps one of the more intuitive proofs
|
||
is by way of the `combinators' $\propPi$ and $\propSig$ presented in sections
|
||
\S\ref{sec:propPi} and \S\ref{sec:propSig}:
|
||
%
|
||
\begin{align*}
|
||
\propPi & \tp \left(∏_{a \tp A} \isProp\ (P\ a)\right) → \isProp\ \left(∏_{a \tp A} P\ a\right)
|
||
\\
|
||
\propSig & \tp \isProp\ A → \left(∏_{a \tp A} \isProp\ (P\ a)\right) → \isProp\ \left(∑_{a \tp A} P\ a\right)
|
||
\end{align*}
|
||
%
|
||
The proof goes like this: We `eliminate' the 3 function abstractions
|
||
by applying $\propPi$ three times. So our proof obligation becomes:
|
||
%
|
||
$$
|
||
\isProp\ \left( \left( \id \comp f ≡ f \right) \x \left( f \comp \id ≡ f \right) \right)
|
||
$$
|
||
%
|
||
Then we eliminate the (non-dependent) sigma-type by applying $\propSig$ giving
|
||
us the two obligations $\isProp\ (\id \comp f ≡ f)$ and $\isProp\ (f \comp
|
||
\id ≡ f)$ which follows from the type of arrows being a
|
||
set.
|
||
|
||
This example illustrates nicely how we can use these combinators to
|
||
reason about `canonical' types like $∑$ and $∏$. Similar
|
||
combinators can be defined at the other homotopic levels. These
|
||
combinators are however not applicable in situations where we want to
|
||
reason about other types e.g.\ types we have defined ourselves. For
|
||
instance, after we have proven that all the projections of
|
||
pre-categories are propositions, we would like to bundle this up to
|
||
show that the type of pre-categories is also a proposition. Formally:
|
||
%
|
||
\begin{equation}
|
||
\label{eq:propIsPreCategory}
|
||
\isProp\ \IsPreCategory
|
||
\end{equation}
|
||
%
|
||
Where the definition of $\IsPreCategory$ is the triple:
|
||
%
|
||
\begin{align*}
|
||
\var{isAssociative} & \tp \var{IsAssociative}\\
|
||
\isIdentity & \tp \var{IsIdentity}\\
|
||
\var{arrowsAreSets} & \tp \var{ArrowsAreSets}
|
||
\end{align*}
|
||
%
|
||
Each corresponding to the first three laws for categories. Note that
|
||
since $\IsPreCategory$ is not formulated with a chain of sigma-types
|
||
we will not have any combinators available to help us here. In stead
|
||
the path type must be used directly.
|
||
|
||
The type \ref{eq:propIsPreCategory} is judgmentally the same as:
|
||
%
|
||
$$
|
||
∏_{a, b \tp \IsPreCategory} a ≡ b
|
||
$$
|
||
%
|
||
So to prove the proposition let $a, b \tp \IsPreCategory$ be given. To
|
||
prove the equality $a ≡ b$ is to give a continuous path from the
|
||
index-type into the path-space. I.e.\ a function $\I →
|
||
\IsPreCategory$. This path must satisfy being being judgmentally the
|
||
same as $a$ at the left endpoint and $b$ at the right endpoint. We
|
||
know we can form a continuous path between all projections of $a$ and
|
||
$b$, this follows from the type of all the projections being mere
|
||
propositions. For instance, the path between $a.\isIdentity$ and
|
||
$b.\isIdentity$ is simply formed by:
|
||
%
|
||
$$
|
||
\propIsIdentity\ a.\isIdentity\ b.\isIdentity
|
||
\tp
|
||
a.\isIdentity ≡ b.\isIdentity
|
||
$$
|
||
%
|
||
So to give the continuous function $\I → \IsPreCategory$, which is our goal, we
|
||
introduce $i \tp \I$ and proceed by constructing an element of $\IsPreCategory$
|
||
by using the fact that all the projections are propositions to generate paths
|
||
between all projections. Once we have such a path e.g.\ $p \tp a.\isIdentity
|
||
≡ b.\isIdentity$ we can eliminate it with $i$ and thus obtain $p\ i \tp
|
||
(p\ i).\isIdentity$. This element satisfies exactly that it corresponds to the
|
||
corresponding projections at either endpoint. Thus the element we construct at
|
||
$i$ becomes the triple:
|
||
%
|
||
\begin{equation}
|
||
\label{eq:proof-prop-IsPreCategory}
|
||
\begin{aligned}
|
||
& \var{propIsAssociative} && a.\var{isAssociative}\
|
||
&& b.\var{isAssociative} && i \\
|
||
& \propIsIdentity && a.\isIdentity\
|
||
&& b.\isIdentity && i \\
|
||
& \var{propArrowsAreSets} && a.\var{arrowsAreSets}\
|
||
&& b.\var{arrowsAreSets} && i
|
||
\end{aligned}
|
||
\end{equation}
|
||
%
|
||
I have found this to be a general pattern when proving things in
|
||
homotopy type theory, namely that you have to wrap and unwrap
|
||
equalities at different levels. It is worth noting that proving this
|
||
theorem with the regular inductive equality type would already not be
|
||
possible, since we at least need functional
|
||
extensionality\index{functional extensionality} (the projections are
|
||
all $∏$-types). Assuming we had functional extensionality
|
||
available to us as an axiom, we would use functional extensionality
|
||
\TODO{in reverse?} to retrieve the equalities in $a$ and $b$,
|
||
pattern-match on them to see that they are both $\refl$ and then close
|
||
the proof with $\refl$. Of course this theorem is not so interesting
|
||
in the setting of ITT since we know a priori that equality proofs are
|
||
unique.
|
||
|
||
The situation is a bit more complicated when we have a dependent type.
|
||
For instance, when we want to show that $\IsCategory$ is a mere
|
||
proposition. The type $\IsCategory$ is a record with two fields, a
|
||
witness to being a pre-category and the univalence condition. Recall
|
||
that the univalence condition is indexed by the identity-proof. So to
|
||
follow the same recipe as above, let $a, b \tp \IsCategory$ be given,
|
||
to show them equal, we now need to give two paths. One homogeneous:
|
||
%
|
||
$$
|
||
p \tp a.\isPreCategory ≡ b.\isPreCategory
|
||
$$
|
||
%
|
||
and one heterogeneous:
|
||
%
|
||
$$
|
||
\Path\ (\lambda\; i → (p\ i).Univalent)\ a.\isPreCategory\ b.\isPreCategory
|
||
$$
|
||
%
|
||
Which depends on the choice of $p$. The first of these we can provide since, as
|
||
we have shown, $\IsPreCategory$ is a proposition. However, even though
|
||
$\Univalent$ is also a proposition, we cannot use this directly to show the
|
||
latter. This is because $\isProp$ talks about non-dependent paths. So we need to
|
||
'promote' the result that univalence is a proposition to a heterogeneous path.
|
||
To this end we can use $\lemPropF$, which was introduced in \S\ref{sec:lemPropF}.
|
||
|
||
In this case $A = \var{IsIdentity}\ \identity$ and $B = \Univalent$. We have
|
||
shown that being a category is a proposition, a result that holds for any choice
|
||
of identity proof. Finally we must provide a proof that the identity proofs at
|
||
$a$ and $b$ are indeed the same, this we can extract from $p$ by applying
|
||
congruence of paths:
|
||
%
|
||
$$
|
||
\congruence\ \isIdentity\ p
|
||
$$
|
||
%
|
||
And this finishes the proof that being-a-category is a mere proposition
|
||
(\ref{eq:propIsPreCategory}).
|
||
|
||
When we have a proper category we can make precise the notion of
|
||
``identifying isomorphic types''. That is, we can construct the
|
||
function:
|
||
%
|
||
$$
|
||
\isoToId \tp (A ≊ B) → (A ≡ B)
|
||
$$
|
||
%
|
||
A perhaps somewhat surprising application of this is that we can show that
|
||
terminal objects are propositional:
|
||
%
|
||
\begin{align}
|
||
\label{eq:termProp}
|
||
\isProp\ \var{Terminal}
|
||
\end{align}
|
||
%
|
||
It follows from the usual observation that any two terminal objects are
|
||
isomorphic - and since categories are univalent, so are they equal. The proof is
|
||
omitted here, but the curious reader can check the implementation for the
|
||
details. It is in the module:
|
||
%
|
||
\begin{center}
|
||
\sourcelink{Cat.Category}
|
||
\end{center}
|
||
|
||
\section{Equivalences}
|
||
\label{sec:equiv}
|
||
The usual notion of a function $f \tp A → B$ having an inverses is:
|
||
%
|
||
\begin{equation}
|
||
\label{eq:isomorphism}
|
||
∑_{g \tp B → A} \left( f \comp g ≡ \identity \right) \x \left( g \comp f ≡ \identity \right)
|
||
\end{equation}
|
||
%
|
||
This is defined in \cite[p. 129]{hott-2013} where it is referred to as the a
|
||
``quasi-inverse''. We shall refer to the type \ref{eq:isomorphism} as
|
||
$\Isomorphism\ f$. This also gives rise to the following type:
|
||
%
|
||
\begin{equation}
|
||
A \cong B ≜ ∑_{f \tp A → B} \Isomorphism\ f
|
||
\end{equation}
|
||
%
|
||
At the same place \cite{hott-2013} gives an ``interface'' for what the judgment
|
||
$\isEquiv \tp (A → B) → \MCU$ must provide:
|
||
%
|
||
\begin{align}
|
||
\var{fromIso} & \tp \Isomorphism\ f → \isEquiv\ f \\
|
||
\var{toIso} & \tp \isEquiv\ f → \Isomorphism\ f \\
|
||
\label{eq:propIsEquiv}
|
||
&\mathrel{\ } \isEquiv\ f
|
||
\end{align}
|
||
%
|
||
The maps $\var{fromIso}$ and $\var{toIso}$ naturally extend to these maps:
|
||
%
|
||
\begin{align}
|
||
\var{fromIsomorphism} & \tp A \cong B → A ≃ B \\
|
||
\var{toIsomorphism} & \tp A ≃ B → A \cong B
|
||
\end{align}
|
||
%
|
||
Having this interface gives us both: a way to think rather abstractly about how
|
||
to work with equivalences and a way to use ad hoc definitions of equivalences.
|
||
The specific instantiation of $\isEquiv$ as defined in \cite{cubical-agda} is:
|
||
%
|
||
$$
|
||
isEquiv\ f ≜ ∏_{b \tp B} \isContr\ (\fiber\ f\ b)
|
||
$$
|
||
where
|
||
$$
|
||
\fiber\ f\ b ≜ ∑_{a \tp A} \left( b ≡ f\ a \right)
|
||
$$
|
||
%
|
||
I give its definition here mainly for completeness, because as I stated we can
|
||
move away from this specific instantiation and think about it more abstractly
|
||
once we have shown that this definition actually works as an equivalence.
|
||
|
||
The implementation of $\var{fromIso}$ can be found in
|
||
\cite{cubical-agda} where it is known as $\var{gradLemma}$. The
|
||
implementation of $\var{fromIso}$ as well as the proof that this
|
||
equivalence is a proposition (\ref{eq:propIsEquiv}) can be found in my
|
||
implementation.
|
||
|
||
We say that two types $A\;B \tp \Type$ are equivalent exactly if there exists an
|
||
equivalence between them:
|
||
%
|
||
\begin{equation}
|
||
\label{eq:equivalence}
|
||
A ≃ B ≜ ∑_{f \tp A → B} \isEquiv\ f
|
||
\end{equation}
|
||
%
|
||
Note that the term equivalence here is overloaded referring both to the map $f
|
||
\tp A → B$ and the type $A ≃ B$. The notion of an isomorphism is
|
||
similarly conflated as isomorphism can refer to the type $A \cong B$ as well as
|
||
the the map $A → B$ that witness this. I will use these conflated terms when
|
||
it is clear from the context what is being referred to.
|
||
|
||
Both $\cong$ and $≃$ form equivalence relations (no pun intended).
|
||
|
||
\section{Univalence}
|
||
\label{sec:univalence}
|
||
As noted in the introduction the univalence for types $A\; B \tp \Type$ states
|
||
that:
|
||
%
|
||
$$
|
||
\var{Univalence} ≜ (A ≡ B) ≃ (A ≃ B)
|
||
$$
|
||
%
|
||
As mentioned the univalence criterion for some category $\bC$ says that for all
|
||
\emph{objects} $A\;B$ we must have:
|
||
$$
|
||
\isEquiv\ (A ≡ B)\ (A ≊ B)\ \idToIso
|
||
$$
|
||
And I mentioned that this was logically equivalent to
|
||
%
|
||
$$
|
||
(A ≡ B) ≃ (A ≊ B)
|
||
$$
|
||
%
|
||
Given that we saw in the previous section that we can construct an equivalence
|
||
from an isomorphism it suffices to demonstrate:
|
||
%
|
||
$$
|
||
(A ≡ B) \cong (A ≊ B)
|
||
$$
|
||
%
|
||
That is, we must demonstrate that there is an isomorphism (on types) between
|
||
equalities and isomorphisms (on arrows). It is worthwhile to dwell on this for a
|
||
few seconds. This type looks very similar to univalence for types and is
|
||
therefore perhaps a bit more intuitive to grasp the implications of. Of course
|
||
univalence for types (which is a proposition -- i.e.\ provable) does not imply
|
||
univalence of all pre-category since morphisms in a category are not regular
|
||
functions -- in stead they can be thought of as a generalization hereof. The univalence criterion therefore is simply a way of restricting arrows
|
||
to behave similarly to maps.
|
||
|
||
I will now mention a few helpful theorems that follow from univalence that will
|
||
become useful later.
|
||
|
||
Obviously univalence gives us an isomorphism between $A ≡ B$ and $A
|
||
≊ B$. I will name these for convenience:
|
||
%
|
||
$$
|
||
\idToIso \tp A ≡ B → A ≊ B
|
||
$$
|
||
%
|
||
$$
|
||
\isoToId \tp A ≊ B → A ≡ B
|
||
$$
|
||
%
|
||
The next few theorems are variations on theorem 9.1.9 from \cite{hott-2013}. Let
|
||
an isomorphism $A ≊ B$ in some category $\bC$ be given. Name the
|
||
isomorphism $\iota \tp A → B$ and its inverse $\inv{\iota} \tp B → A$.
|
||
Since $\bC$ is a category (and therefore univalent) the isomorphism induces a
|
||
path $p \tp A ≡ B$. From this equality we can get two further paths:
|
||
$p_{\var{dom}} \tp \Arrow\ A\ X ≡ \Arrow\ B\ X$ and
|
||
$p_{\var{cod}} \tp \Arrow\ X\ A ≡ \Arrow\ X\ B$. We
|
||
then have the following two theorems:
|
||
%
|
||
\begin{align}
|
||
\label{eq:coeDom}
|
||
\var{coeDom} & \tp ∏_{f \tp A → X}
|
||
\var{coe}\ p_{\var{dom}}\ f ≡ f \lll \inv{\iota}
|
||
\\
|
||
\label{eq:coeCod}
|
||
\var{coeCod} & \tp ∏_{f \tp A → X}
|
||
\var{coe}\ p_{\var{cod}}\ f ≡ \iota \lll f
|
||
\end{align}
|
||
%
|
||
I will give the proof of the first theorem here, the second one is analogous.
|
||
%
|
||
\begin{align*}
|
||
\var{coe}\ p_{\var{dom}}\ f
|
||
& ≡ f \lll \inv{(\idToIso\ p)} && \text{lemma} \\
|
||
& ≡ f \lll \inv{\iota}
|
||
&& \text{$\idToIso$ and $\isoToId$ are inverses}\\
|
||
\end{align*}
|
||
%
|
||
In the second step we use the fact that $p$ is constructed from the isomorphism
|
||
$\iota$ -- $\inv{(\idToIso\ p)}$ denotes the map $B → A$ induced by the
|
||
isomorphism $\idToIso\ p \tp A \cong B$. The helper-lemma is similar to
|
||
what we are trying to prove but talks about paths rather than isomorphisms:
|
||
%
|
||
\begin{equation}
|
||
\label{eq:coeDomIso}
|
||
∏_{f \tp \Arrow\ A\ B} ∏_{p \tp A ≡ B}
|
||
\var{coe}\ p_{\var{dom}}\ f ≡ f \lll \inv{(\idToIso\ p)}
|
||
\end{equation}
|
||
%
|
||
Again $p_{\var{dom}}$ denotes the path $\Arrow\ A\ X ≡
|
||
\Arrow\ B\ X$ induced by $p$. To prove this statement I let $f$ and $p$ be
|
||
given and then invoke based-path-induction. The induction will be based at $A
|
||
\tp \Object$ Let $\widetilde{B} \tp \Object$ and $\widetilde{p} \tp A
|
||
≡ \widetilde{B}$ be given. The family that we perform induction over will
|
||
be:
|
||
%
|
||
\begin{align}
|
||
D\ \widetilde{B}\ \widetilde{p} ≜
|
||
%% ∏_{\widetilde{B} \tp \Object}
|
||
%% ∏_{\widetilde{p} \tp A ≡ \widetilde{B}}
|
||
\var{coe}\ {\widetilde{p}}^*\ f
|
||
≡
|
||
f \lll \inv{(\idToIso\ \widetilde{p})}
|
||
\end{align}
|
||
The base-case therefore becomes
|
||
$d \tp \var{coe}\ \refl^*\ f ≡ f \lll \inv{(\idToIso\ \refl)}$
|
||
and is inhabited by:
|
||
\begin{align*}
|
||
\var{coe}\ \refl^*\ f
|
||
& ≡ f
|
||
&& \text{$\refl$ is a neutral element for $\var{coe}$}\\
|
||
& ≡ f \lll \identity \\
|
||
& ≡ f \lll \var{subst}\ \refl\ \identity
|
||
&& \text{$\refl$ is a neutral element for $\var{subst}$}\\
|
||
& ≡ f \lll \inv{(\idToIso\ \refl)}
|
||
&& \text{By definition of $\idToIso$}\\
|
||
\end{align*}
|
||
%
|
||
To close the based-path-induction we must supply the value ``at the other''. In
|
||
this case this is simply $B \tp \Object$ and $p \tp A ≡ B$ which we have.
|
||
In summary the proof of \ref{eq:coeDomIso} is the term:
|
||
%
|
||
\begin{equation}
|
||
\label{eq:pathJ-example}
|
||
\pathJ\ D\ d\ B\ p
|
||
\end{equation}
|
||
%
|
||
And this finishes the proof of \ref{eq:coeDomIso} and thus \ref{eq:coeDom}.
|
||
%
|
||
\section{Categories}
|
||
\subsection{Opposite category}
|
||
\label{op-cat}
|
||
The first category I will present is a pure construction on categories. Given
|
||
some category we can construct its dual, called the opposite category. Starting
|
||
with a simple example allows us to focus on how we work with equivalences and
|
||
univalence in a very simple category where the structure of the category is
|
||
rather simple.
|
||
|
||
Let $\bC$ be some category, we then define the opposite category
|
||
$\bC^{\var{Op}}$. It has the same objects, but the type of arrows are flipped,
|
||
that is to say an arrow from $A$ to $B$ in the opposite category corresponds to
|
||
an arrow from $B$ to $A$ in the underlying category. The identity arrow is the
|
||
same as the one in the underlying category (they have the same type). Function
|
||
composition will be reverse function composition from the underlying category.
|
||
|
||
I will refer to things in terms of the underlying category, unless they have an
|
||
over-bar. So e.g.\ $\idToIso$ is a function in the underlying category and the
|
||
corresponding thing is denoted $\wideoverbar{\idToIso}$ in the opposite
|
||
category.
|
||
|
||
Showing that this forms a pre-category is rather straightforward.
|
||
%
|
||
$$
|
||
h \rrr (g \rrr f) ≡ h \rrr g \rrr f
|
||
$$
|
||
%
|
||
Since $\rrr$ is reverse function composition this is just the symmetric version
|
||
of associativity.
|
||
%
|
||
$$
|
||
\identity \rrr f ≡ f \x f \rrr \identity ≡ f
|
||
$$
|
||
%
|
||
This is just the swapped version of identity.
|
||
|
||
Finally, that the arrows form sets just follows by flipping the order of the
|
||
arguments. Or in other words; since $\Arrow\ A\ B$ is a set for all $A\;B \tp
|
||
\Object$ then so is $Arrow\ B\ A$.
|
||
|
||
Now, to show that this category is univalent is not as straightforward. Luckily
|
||
section \S\ref{sec:equiv} gave us some tools to work with equivalences. We saw
|
||
that we can prove this category univalent by giving an inverse to
|
||
$\wideoverbar{\idToIso} \tp (A ≡ B) → (A \wideoverbar{≊} B)$.
|
||
From the original category we have that $\idToIso \tp (A ≡ B) → (A \cong
|
||
B)$ is an isomorphism. Let us denote its inverse with $\isoToId \tp (A
|
||
≊ B) → (A ≡ B)$. If we squint we can see what we need is a way to
|
||
go between $\wideoverbar{≊}$ and $≊$.
|
||
|
||
An inhabitant of $A ≊ B$ is simply an arrow $f \tp \Arrow\ A\ B$
|
||
and its inverse $g \tp \Arrow\ B\ A$. In the opposite category $g$ will
|
||
play the role of the isomorphism and $f$ will be the inverse. Similarly we can
|
||
go in the opposite direction. I name these maps $\shufflef \tp (A ≊
|
||
B) → (A \wideoverbar{≊} B)$ and $\shufflef^{-1} \tp (A
|
||
\wideoverbar{≊} B) → (A ≊ B)$ respectively.
|
||
|
||
As the inverse of $\wideoverbar{\idToIso}$ I will pick $\wideoverbar{\isoToId}
|
||
≜ \isoToId \comp \shufflef$. The proof that they are inverses go as
|
||
follows:
|
||
%
|
||
\begin{align*}
|
||
\wideoverbar{\isoToId} \comp \wideoverbar{\idToIso} & =
|
||
\isoToId \comp \shufflef \comp \wideoverbar{\idToIso}
|
||
\\
|
||
%% ≡⟨ cong (λ \; φ → φ x) (cong (λ \; φ → η ⊙ shuffle ⊙ φ) (funExt lem)) ⟩ \\
|
||
%
|
||
& ≡
|
||
\isoToId \comp \shufflef \comp \inv{\shufflef} \comp \idToIso
|
||
&& \text{lemma} \\
|
||
%% ≡⟨⟩ \\
|
||
& ≡
|
||
\isoToId \comp \idToIso
|
||
&& \text{$\shufflef$ is an isomorphism} \\
|
||
& ≡
|
||
\identity
|
||
&& \text{$\isoToId$ is an isomorphism}
|
||
\end{align*}
|
||
%
|
||
The other direction is analogous.
|
||
|
||
The lemma used in step 2 of this proof states that $\wideoverbar{idToIso} ≡
|
||
\inv{\shufflef} \comp \idToIso$. This is a rather straightforward proof
|
||
since being-an-inverse-of is a proposition, so it suffices to show that their
|
||
first components are equal, but this holds judgmentally.
|
||
|
||
This finished the proof that the opposite category is in fact a category. Now,
|
||
to prove that that opposite-of is an involution we must show:
|
||
%
|
||
$$
|
||
∏_{\bC \tp \Category} \left(\bC^{\var{Op}}\right)^{\var{Op}} ≡ \bC
|
||
$$
|
||
%
|
||
As we have seen the laws in $\left(\bC^{\var{Op}}\right)^{\var{Op}}$ get quite
|
||
involved\footnote{We have not even seen the full story because we have used
|
||
this `interface' for equivalences.}. Luckily since being-a-category is a mere
|
||
proposition, we need not concern ourselves with this bit when proving the above.
|
||
We can use the equality principle for categories that let us prove an equality
|
||
just by giving an equality on the data-part. So, given a category $\bC$ all we
|
||
must provide is the following proof:
|
||
%
|
||
$$
|
||
\var{raw}\ \left(\bC^{\var{Op}}\right)^{\var{Op}} ≡ \var{raw}\ \bC
|
||
$$
|
||
%
|
||
And these are judgmentally the same. I remind the reader that the left-hand side
|
||
is constructed by flipping the arrows, which judgmentally is an involution.
|
||
|
||
\subsection{Category of sets}
|
||
The category of sets has as objects, not types, but only those types that are
|
||
homotopic sets. This is encapsulated in Agda with the following type:
|
||
%
|
||
$$\Set ≜ ∑_{A \tp \MCU} \isSet\ A$$
|
||
%
|
||
The more straightforward notion of a category where the objects are types is
|
||
not a valid \mbox{(1-)category}. This stems from the fact that types in cubical
|
||
Agda types can have higher homotopic structure.
|
||
|
||
Univalence does not follow immediately from univalence for types:
|
||
%
|
||
$$(A ≡ B) ≃ (A ≃ B)$$
|
||
%
|
||
Because here $A, B \tp \Type$ whereas the objects in this category have the type
|
||
$\Set$ so we cannot form the type $\var{hA} ≃ \var{hB}$ for objects
|
||
$\var{hA}\;\var{hB} \tp \Set$. In stead I show that this category
|
||
satisfies:
|
||
%
|
||
$$
|
||
(\var{hA} ≡ \var{hB}) ≃ (\var{hA} ≊ \var{hB})
|
||
$$
|
||
%
|
||
Which, as we saw in section \S\ref{sec:univalence}, is sufficient to show that the
|
||
category is univalent. The way that I have shown this is with a three-step
|
||
process. For objects $(A, s_A)\; (B, s_B) \tp \Set$ I show the following chain
|
||
of equivalences:
|
||
%
|
||
\begin{align*}
|
||
((A, s_A) ≡ (B, s_B))
|
||
& ≃ (A ≡ B) && \ref{eq:equivPropSig} \\
|
||
& ≃ (A ≃ B) && \text{Univalence} \\
|
||
& ≃ ((A, s_A) ≊ (B, s_B)) && \text{\ref{eq:equivSig} and \ref{eq:equivIso}}
|
||
\end{align*}
|
||
|
||
And since $≃$ is an equivalence relation we can chain these equivalences
|
||
together. Step one will be proven with the following lemma:
|
||
%
|
||
\begin{align}
|
||
\label{eq:equivPropSig}
|
||
\left(∏_{a \tp A} \isProp\ (P\ a)\right) → ∏_{x\;y \tp ∑_{a \tp A} P\ a} (x ≡ y) ≃ (\fst\ x ≡ \fst\ y)
|
||
\end{align}
|
||
%
|
||
The lemma states that for pairs whose second component are mere propositions
|
||
equality is equivalent to equality of the first components. In this case the
|
||
type-family $P$ is $\isSet$ which itself is a proposition for any type $A \tp
|
||
\Type$. Step two is univalence. Step three will be proven with the following
|
||
lemma:
|
||
%
|
||
\begin{align}
|
||
\label{eq:equivSig}
|
||
∏_{a \tp A} \left( P\ a ≃ Q\ a \right) → ∑_{a \tp A} P\ a ≃ ∑_{a \tp A} Q\ a
|
||
\end{align}
|
||
%
|
||
Which says that if two type-families are equivalent at all points, then pairs
|
||
with identical first components and these families as second components will
|
||
also be equivalent. For our purposes $P ≜ \isEquiv\ A\ B$ and $Q ≜
|
||
\Isomorphism$. So we must finally prove:
|
||
%
|
||
\begin{align}
|
||
\label{eq:equivIso}
|
||
∏_{f \tp A → B} \left( \isEquiv\ A\ B\ f ≃ \Isomorphism\ f \right)
|
||
\end{align}
|
||
|
||
First, lets prove \ref{eq:equivPropSig}: Let $propP \tp ∏_{a \tp A} \isProp\ (P\ a)$ and $x\;y \tp ∑_{a \tp A} P\ a$ be given. Because
|
||
of $\var{fromIsomorphism}$ it suffices to give an isomorphism between
|
||
$x ≡ y$ and $\fst\ x ≡ \fst\ y$:
|
||
%
|
||
%% FIXME: Too much alignement?
|
||
\begin{equation*}
|
||
\begin{aligned}
|
||
f & ≜ \congruence\ \fst
|
||
&& \tp x ≡ y && → \fst\ x ≡ \fst\ y \\
|
||
g & ≜ \var{lemSig}\ \var{propP}\ x\ y
|
||
&& \tp \fst\ x ≡ \fst\ y && → x ≡ y
|
||
\end{aligned}
|
||
\end{equation*}
|
||
%
|
||
\TODO{Is it confusing that I use point-free style here?}Here $\var{lemSig}$ is
|
||
a lemma that says that if the second component of a pair is a proposition, it
|
||
suffices to give a path between its first components to construct an equality of
|
||
the two pairs:
|
||
%
|
||
\begin{align*}
|
||
\var{lemSig} \tp \left( ∏_{x \tp A} \isProp\ (B\ x) \right) →
|
||
∏_{u\; v \tp ∑_{a \tp A} B\ a}
|
||
\left( \fst\ u ≡ \fst\ v \right) → u ≡ v
|
||
\end{align*}
|
||
%
|
||
The proof that these are indeed inverses has been omitted. The details
|
||
can be found in the module:
|
||
\begin{center}
|
||
\sourcelink{Cat.Categories.Sets}
|
||
\end{center}
|
||
|
||
Now to prove \ref{eq:equivSig}: Let $e \tp ∏_{a \tp A} \left( P\ a
|
||
≃ Q\ a \right)$ be given. To prove the equivalence, it suffices
|
||
to give an isomorphism between $∑_{a \tp A} P\ a$ and $∑_{a \tp
|
||
A} Q\ a$, but since they have identical first components it suffices
|
||
to give an isomorphism between $P\ a$ and $Q\ a$ for all $a \tp A$.
|
||
This is exactly what we can get from the equivalence $e$.\QED
|
||
|
||
Lastly we prove \ref{eq:equivIso}. Let $f \tp A → B$ be given. For the maps we
|
||
choose:
|
||
%
|
||
\begin{align*}
|
||
\var{toIso}
|
||
& \tp \isEquiv\ f → \Isomorphism\ f \\
|
||
\var{fromIso}
|
||
& \tp \Isomorphism\ f → \isEquiv\ f
|
||
\end{align*}
|
||
%
|
||
As mentioned in section \S\ref{sec:equiv}. These maps are not in general inverses
|
||
of each other. In stead, we will use the fact that $A$ and $B$ are sets. The first thing we must prove is:
|
||
%
|
||
\begin{align*}
|
||
\var{fromIso} \comp \var{toIso} ≡ \identity_{\isEquiv\ f}
|
||
\end{align*}
|
||
%
|
||
For this we can use the fact that being-an-equivalence is a mere proposition.
|
||
For the other direction:
|
||
%
|
||
\begin{align*}
|
||
\var{toIso} \comp \var{fromIso} ≡ \identity_{\Isomorphism\ f}
|
||
\end{align*}
|
||
%
|
||
We will show that $\Isomorphism\ f$ is also a mere proposition. To this
|
||
end, let $X\;Y \tp \Isomorphism\ f$ be given. Name the maps $x\;y \tp B
|
||
→ A$ respectively. Now, the proof that $X$ and $Y$ are the same is a pair of
|
||
paths: $p \tp x ≡ y$ and $\Path\ (\lambda\; i →
|
||
\var{AreInverses}\ f\ (p\ i))\ \mathcal{X}\ \mathcal{Y}$ where $\mathcal{X}$
|
||
and $\mathcal{Y}$ denotes the witnesses that $x$ (respectively $y$) is an
|
||
inverse to $f$. The path $p$ is inhabited by:
|
||
%
|
||
\begin{align*}
|
||
x
|
||
& = x \comp \identity \\
|
||
& ≡ x \comp (f \comp y)
|
||
&& \text{$y$ is an inverse to $f$} \\
|
||
& ≡ (x \comp f) \comp y \\
|
||
& ≡ \identity \comp y
|
||
&& \text{$x$ is an inverse to $f$} \\
|
||
& = y
|
||
\end{align*}
|
||
%
|
||
For the other (dependent) path we can prove that being-an-inverse-of is a
|
||
proposition and then use $\lemPropF$. So we prove the generalization:
|
||
%
|
||
\begin{align}
|
||
\label{eq:propAreInversesGen}
|
||
∏_{g \tp B → A} \isProp\ (\var{AreInverses}\ f\ g)
|
||
\end{align}
|
||
%
|
||
But $\var{AreInverses}\ f\ g$ is a pair of equations on arrows, so we use
|
||
$\propSig$ and the fact that both $A$ and $B$ are sets to close this proof.
|
||
|
||
%% \subsection{Category of categories}
|
||
|
||
%% Note that this category does in fact not exist. In stead I provide
|
||
%% the definition of the ``raw'' category as well as some of the laws.
|
||
|
||
%% Furthermore I provide some helpful lemmas about this raw category.
|
||
%% For instance I have shown what would be the exponential object in
|
||
%% such a category.
|
||
|
||
%% These lemmas can be used to provide the actual exponential object
|
||
%% in a context where we have a witness to this being a category. This
|
||
%% is useful if this library is later extended to talk about higher
|
||
%% categories.
|
||
|
||
\section{Products}
|
||
\label{sec:products}
|
||
In the following a technique for using categories to prove properties will be
|
||
demonstrated. The goal in this section is to show that products are
|
||
propositions:
|
||
%
|
||
$$
|
||
∏_{\bC \tp \Category} ∏_{A\;B \tp \Object} \isProp\ (\var{Product}\ \bC\ A\ B)
|
||
$$
|
||
%
|
||
Where $\var{Product}\ \bC\ A\ B$ denotes the type of products of objects $A$
|
||
and $B$ in the category $\bC$. I do this by constructing a category whose
|
||
terminal objects are equivalent to products in $\bC$, and since terminal objects
|
||
are propositional in a proper category and equivalences preserve homotopy level,
|
||
then we know that products also are propositions. But before we get to that,
|
||
we recall the definition of products.
|
||
|
||
\subsection{Definition of products}
|
||
Given a category $\bC$ and two objects $A$ and $B$ in $\bC$ we define the
|
||
product (object) of $A$ and $B$ to be an object $A \x B$ in $\bC$ and two arrows
|
||
$\pi_1 \tp A \x B → A$ and $\pi_2 \tp A \x B → B$ called the projections of
|
||
the product. The projections must satisfy the following property:
|
||
|
||
For all $X \tp Object$, $f \tp \Arrow\ X\ A$ and $g \tp \Arrow\ X\ B$ we have
|
||
that there exists a unique arrow $\pi \tp \Arrow\ X\ (A \x B)$ satisfying
|
||
%
|
||
\begin{align}
|
||
\label{eq:umpProduct}
|
||
%% ∏_{X \tp Object} ∏_{f \tp \Arrow\ X\ A} ∏_{g \tp \Arrow\ X\ B}\\
|
||
%% \uexists_{f \x g \tp \Arrow\ X\ (A \x B)}
|
||
\pi_1 \lll \pi ≡ f \x \pi_2 \lll \pi ≡ g
|
||
\end{align}
|
||
%
|
||
$\pi$ is called the product (arrow) of $f$ and $g$.
|
||
|
||
\subsection{Span category}
|
||
Given a base category $\bC$ and two objects in this category $\pairA$ and
|
||
$\pairB$ we can construct the \nomenindex{span category}:
|
||
|
||
The type of objects in this category will be an object in the underlying
|
||
category, $X$, and two arrows (also from the underlying category)
|
||
$\Arrow\ X\ \pairA$ and $\Arrow\ X\ \pairB$.
|
||
|
||
\newcommand\pairf{\ensuremath{f}}
|
||
\newcommand\pairFst{\mathcal{\pi_1}}
|
||
\newcommand\pairSnd{\mathcal{\pi_2}}
|
||
|
||
An arrow between objects $A ,\ a_0 ,\ a_1$ and $B ,\ b_0 ,\ b_1$ in this
|
||
category will consist of an arrow from the underlying category $\pairf \tp
|
||
\Arrow\ A\ B$ satisfying:
|
||
%
|
||
\begin{align}
|
||
\label{eq:pairArrowLaw}
|
||
b_0 \lll f ≡ a_0 \x
|
||
b_1 \lll f ≡ a_1
|
||
\end{align}
|
||
|
||
The identity morphism is the identity morphism from the underlying category.
|
||
This choice satisfies \ref{eq:pairArrowLaw} because of the right-identity law
|
||
from the underlying category.
|
||
|
||
For composition of arrows $f \tp \Arrow\ A\ B$ and $g \tp \Arrow\ B\ C$ we
|
||
choose $g \lll f$ and we must now verify that it satisfies
|
||
\ref{eq:pairArrowLaw}:
|
||
%
|
||
\begin{align*}
|
||
c_0 \lll (f \lll g)
|
||
& ≡
|
||
(c_0 \lll f) \lll g
|
||
&& \text{Associativity} \\
|
||
& ≡
|
||
b_0 \lll g
|
||
&& \text{$f$ satisfies \ref{eq:pairArrowLaw}} \\
|
||
& ≡
|
||
a_0
|
||
&& \text{$g$ satisfies \ref{eq:pairArrowLaw}} \\
|
||
\end{align*}
|
||
%
|
||
Now we must verify the category-laws. For all the laws we will follow the
|
||
pattern of using the law from the underlying category, and that the type of
|
||
arrows form a set. For instance, to prove associativity we must prove that
|
||
%
|
||
\begin{align}
|
||
\label{eq:productAssoc}
|
||
\overline{h} \lll (\overline{g} \lll \overline{f})
|
||
≡
|
||
(\overline{h} \lll \overline{g}) \lll \overline{f}
|
||
\end{align}
|
||
%
|
||
Here $\lll$ refers to the `embellished' composition and $\overline{f}$,
|
||
$\overline{g}$ and $\overline{h}$ are triples consisting of arrows from the
|
||
underlying category ($f$, $g$ and $h$) and a pair of witnesses to
|
||
\ref{eq:pairArrowLaw}.
|
||
%% Luckily those winesses are paths in the hom-set of the
|
||
%% underlying category which is a set, so these are mere propositions.
|
||
The proof obligations is consists of two things. The first one is:
|
||
%
|
||
\begin{align}
|
||
\label{eq:productAssocUnderlying}
|
||
h \lll (g \lll f)
|
||
≡
|
||
(h \lll g) \lll f
|
||
\end{align}
|
||
%
|
||
And the other proof obligation is that the witness to \ref{eq:pairArrowLaw} for
|
||
the left-hand-side and the right-hand-side are the same.
|
||
|
||
The proof of the first goal comes directly from the underlying category. The
|
||
type of the second goal is very complicated. I will not write it out in full
|
||
here, but it suffices to show the type of the path-space. Note that the arrows
|
||
in \ref{eq:productAssoc} are arrows from $\mathcal{A} = (A , a_{\pairA} ,
|
||
a_{\pairB})$ to $\mathcal{D} = (D , d_{\pairA} , d_{\pairB})$ where
|
||
$a_{\pairA}$, $a_{\pairB}$, $d_{\pairA}$ and $d_{\pairB}$ are arrows in the
|
||
underlying category. Given that $p$ is the chosen proof of
|
||
\ref{eq:productAssocUnderlying} we then have that the witness to
|
||
\ref{eq:pairArrowLaw} vary over the type:
|
||
%
|
||
\begin{align}
|
||
\label{eq:productPath}
|
||
λ \; i → d_{\pairA} \lll p\ i ≡ 2 a_{\pairA} × d_{\pairB} \lll p\ i ≡ a_{\pairB}
|
||
\end{align}
|
||
%
|
||
And these paths are in the type of the hom-set of the underlying category, so
|
||
they are mere propositions. We cannot apply the fact that arrows in $\bC$ are
|
||
sets directly, however, since $\isSet$ only talks about non-dependent paths, in
|
||
stead we generalize \ref{eq:productPath} to:
|
||
%
|
||
\begin{align}
|
||
\label{eq:productEqPrinc}
|
||
∏_{f \tp \Arrow\ X\ Y} \isProp\ \left( y_{\pairA} \lll f ≡ x_{\pairA} × y_{\pairB} \lll f ≡ x_{\pairB} \right)
|
||
\end{align}
|
||
%
|
||
For all objects $X , x_{\pairA} , x_{\pairB}$ and $Y , y_{\pairA} , y_{\pairB}$,
|
||
but this follows from pairs preserving homotopical structure and arrows in the
|
||
underlying category being sets. This gives us an equality principle for arrows
|
||
in this category that says that to prove two arrows $f, f_0, f_1$ and $g, g_0,
|
||
g_1$ equal it suffices to give a proof that $f$ and $g$ are equal.
|
||
%% %
|
||
%% $$
|
||
%% ∏_{(f, f_0, f_1)\; (g,g_0,g_1) \tp \Arrow\ X\ Y} f ≡ g \to (f, f_0, f_1) ≡ (g,g_0,g_1)
|
||
%% $$
|
||
%% %
|
||
And thus we have proven \ref{eq:productAssoc} simply with
|
||
\ref{eq:productAssocUnderlying}.
|
||
|
||
Now we must prove that arrows form a set:
|
||
%
|
||
$$
|
||
\isSet\ (\Arrow\ \mathcal{X}\ \mathcal{Y})
|
||
$$
|
||
%
|
||
Since pairs preserve homotopical structure this reduces to:
|
||
%
|
||
$$
|
||
\isSet\ (\Arrow_{\bC}\ X\ Y)
|
||
$$
|
||
%
|
||
Which holds. And
|
||
%
|
||
$$
|
||
∏_{f \tp \Arrow\ X\ Y}
|
||
\isSet\ \left( y_{\pairA} \lll f ≡ x_{\pairA}
|
||
× y_{\pairB} \lll f ≡ x_{\pairB}
|
||
\right)
|
||
$$
|
||
%
|
||
This we get from \ref{eq:productEqPrinc} and the fact that homotopical structure
|
||
is cumulative.
|
||
|
||
This finishes the proof that this is a valid pre-category.
|
||
|
||
\subsubsection{Univalence}
|
||
To prove that this is a proper category it must be shown that it is univalent.
|
||
That is, for any two objects $\mathcal{X} = (X, x_{\mathcal{A}} , x_{\mathcal{B}})$
|
||
and $\mathcal{Y} = Y, y_{\mathcal{A}}, y_{\mathcal{B}}$ I will show:
|
||
%
|
||
\begin{align}
|
||
(\mathcal{X} ≡ \mathcal{Y}) \cong (\mathcal{X} ≊ \mathcal{Y})
|
||
\end{align}
|
||
|
||
I do this by showing that the following sequence of types are isomorphic.
|
||
|
||
The first type is:
|
||
%
|
||
\begin{align}
|
||
\label{eq:univ-0}
|
||
(X , x_{\mathcal{A}} , x_{\mathcal{B}}) ≡ (Y , y_{\mathcal{A}} , y_{\mathcal{B}})
|
||
\end{align}
|
||
%
|
||
The next types will be the triple:
|
||
%
|
||
\begin{align}
|
||
\label{eq:univ-1}
|
||
\begin{split}
|
||
p \tp & X ≡ Y \\
|
||
& \Path\ (λ \; i → \Arrow\ (p\ i)\ \mathcal{A})\ x_{\mathcal{A}}\ y_{\mathcal{A}} \\
|
||
& \Path\ (λ \; i → \Arrow\ (p\ i)\ \mathcal{B})\ x_{\mathcal{B}}\ y_{\mathcal{B}}
|
||
\end{split}
|
||
%% \end{split}
|
||
\end{align}
|
||
|
||
The next type is very similar, but in stead of a path we will have an
|
||
isomorphism, and create a path from this:
|
||
%
|
||
\begin{align}
|
||
\label{eq:univ-2}
|
||
\begin{split}
|
||
\var{iso} \tp & X ≊ Y \\
|
||
& \Path\ (λ \; i → \Arrow\ (\widetilde{p}\ i)\ \mathcal{A})\ x_{\mathcal{A}}\ y_{\mathcal{A}} \\
|
||
& \Path\ (λ \; i → \Arrow\ (\widetilde{p}\ i)\ \mathcal{B})\ x_{\mathcal{B}}\ y_{\mathcal{B}}
|
||
\end{split}
|
||
\end{align}
|
||
%
|
||
Where $\widetilde{p} ≜ \isoToId\ \var{iso} \tp X ≡ Y$.
|
||
|
||
Finally we have the type:
|
||
%
|
||
\begin{align}
|
||
\label{eq:univ-3}
|
||
(X , x_{\mathcal{A}} , x_{\mathcal{B}}) ≊ (Y , y_{\mathcal{A}} , y_{\mathcal{B}})
|
||
\end{align}
|
||
|
||
\emph{Proposition} \ref{eq:univ-0} is isomorphic to \ref{eq:univ-1}: This is
|
||
just an application of the fact that a path between two pairs $a_0, a_1$ and
|
||
$b_0, b_1$ corresponds to a pair of paths between $a_0,b_0$ and $a_1,b_1$ (check
|
||
the implementation for the details).
|
||
|
||
\emph{Proposition} \ref{eq:univ-1} is isomorphic to \ref{eq:univ-2}:
|
||
This proof of this has been omitted but can be found in the module:
|
||
%
|
||
\begin{center}%
|
||
\sourcelink{Cat.Categories.Span}
|
||
\end{center}
|
||
%
|
||
\emph{Proposition} \ref{eq:univ-2} is isomorphic to \ref{eq:univ-3}: For this I
|
||
will show two corollaries of \ref{eq:coeCod}: For an isomorphism $(\iota,
|
||
\inv{\iota}, \var{inv}) \tp A \cong B$, arrows $f \tp \Arrow\ A\ X$, $g \tp
|
||
\Arrow\ B\ X$ and a heterogeneous path between them, $q \tp \Path\ (\lambda\; i
|
||
→ p_{\var{dom}}\ i)\ f\ g$, where $p_{\var{dom}} \tp \Arrow\ A\ X ≡
|
||
\Arrow\ B\ X$ is a path induced by $\var{iso}$, we have the following two
|
||
results
|
||
%
|
||
\begin{align}
|
||
\label{eq:domain-twist-0}
|
||
f & ≡ g \lll \iota \\
|
||
\label{eq:domain-twist-1}
|
||
g & ≡ f \lll \inv{\iota}
|
||
\end{align}
|
||
%
|
||
The proof is omitted but can be found in the module:
|
||
\begin{center}
|
||
\sourcelink{Cat.Category}
|
||
\end{center}
|
||
|
||
Now we can prove the equivalence in the following way: Given $(f, \inv{f},
|
||
\var{inv}_f) \tp X \cong Y$ and two heterogeneous paths
|
||
%
|
||
\begin{align*}
|
||
p_{\mathcal{A}} & \tp \Path\ (\lambda\; i → p_{\var{dom}}\ i)\ x_{\mathcal{A}}\ y_{\mathcal{A}}\\
|
||
%
|
||
q_{\mathcal{B}} & \tp \Path\ (\lambda\; i → p_{\var{dom}}\ i)\ x_{\mathcal{B}}\ y_{\mathcal{B}}
|
||
\end{align*}
|
||
%
|
||
all as in \ref{eq:univ-2}. I use $p_{\var{dom}}$ here again to mean the path
|
||
induced by the isomorphism $f, \inv{f}$. I must now construct an isomorphism
|
||
$(X, x_{\mathcal{A}}, x_{\mathcal{B}}) ≊ (Y, y_{\mathcal{A}}, y_{\mathcal{B}})$
|
||
as in \ref{eq:univ-3}. That is, an isomorphism in the present category. I remind
|
||
the reader that such a gadget is a triple. The first component shall be:
|
||
%
|
||
\begin{align}
|
||
f \tp \Arrow\ X\ Y
|
||
\end{align}
|
||
%
|
||
To show that this choice fits the bill I must now verify that it satisfies
|
||
\ref{eq:pairArrowLaw}, which in this case becomes:
|
||
%
|
||
\begin{align}
|
||
(y_{\mathcal{A}} \lll f ≡ x_{\mathcal{A}}) × (y_{\mathcal{B}} \lll f ≡ x_{\mathcal{B}})
|
||
\end{align}
|
||
%
|
||
Which, since $f$ is an isomorphism and $p_{\mathcal{A}}$ (resp.\ $p_{\mathcal{B}}$)
|
||
is a path varying according to a path constructed from this isomorphism, this is
|
||
exactly what \ref{eq:domain-twist-0} gives us.
|
||
%
|
||
The other direction is quite analogous. We choose $\inv{f}$ as the morphism and
|
||
prove that it satisfies \ref{eq:pairArrowLaw} with \ref{eq:domain-twist-1}.
|
||
|
||
We must now show that this choice of arrows indeed form an isomorphism. Our
|
||
equality principle for arrows in this category (\ref{eq:productEqPrinc}) gives
|
||
us that it suffices to show that $f$ and $\inv{f}$, this is exactly
|
||
$\var{inv}_f$.
|
||
|
||
This concludes the first direction of the isomorphism that we are constructing.
|
||
For the other direction we are given the isomorphism:
|
||
%
|
||
$$
|
||
(f, \inv{f}, \var{inv}_f, \var{inv}_{\inv{f}})
|
||
\tp
|
||
(X, x_{\mathcal{A}}, x_{\mathcal{B}}) ≊ (Y, y_{\mathcal{A}}, y_{\mathcal{B}})
|
||
$$
|
||
%
|
||
Projecting out the first component gives us the isomorphism
|
||
%
|
||
$$
|
||
(\fst\ f, \fst\ \inv{f}
|
||
, \congruence\ \fst\ \var{inv}_f
|
||
, \congruence\ \fst\ \var{inv}_{\inv{f}}
|
||
)
|
||
\tp X ≊ Y
|
||
$$
|
||
%
|
||
This gives rise to the following paths:
|
||
%
|
||
\begin{align}
|
||
\begin{split}
|
||
\widetilde{p} & \tp X ≡ Y \\
|
||
\widetilde{p}_{\mathcal{A}} & \tp \Arrow\ X\ \mathcal{A} ≡ \Arrow\ Y\ \mathcal{A} \\
|
||
\widetilde{p}_{\mathcal{B}} & \tp \Arrow\ X\ \mathcal{B} ≡ \Arrow\ Y\ \mathcal{B}
|
||
\end{split}
|
||
\end{align}
|
||
%
|
||
It then remains to construct the two paths:
|
||
%
|
||
\begin{align}
|
||
\begin{split}
|
||
\label{eq:product-paths}
|
||
& \Path\ (λ \; i → \widetilde{p}_{\mathcal{A}}\ i)\ x_{\mathcal{A}}\ y_{\mathcal{A}}\\
|
||
& \Path\ (λ \; i → \widetilde{p}_{\mathcal{B}}\ i)\ x_{\mathcal{B}}\ y_{\mathcal{B}}
|
||
\end{split}
|
||
\end{align}
|
||
%
|
||
This is achieved with the following lemma:
|
||
%
|
||
\begin{align}
|
||
∏_{a \tp A} ∏_{b \tp B} ∏_{q \tp A ≡ B} \var{coe}\ q\ a ≡ b →
|
||
\Path\ (λ \; i → q\ i)\ a\ b
|
||
\end{align}
|
||
%
|
||
Which is used without proof. See the implementation for the details.
|
||
|
||
\ref{eq:product-paths} is then proven with the propositions:
|
||
%
|
||
\begin{align}
|
||
\begin{split}
|
||
%% \label{eq:product-paths}
|
||
\var{coe}\ \widetilde{p}_{\mathcal{A}}\ x_{\mathcal{A}} ≡ y_{\mathcal{A}}\\
|
||
\var{coe}\ \widetilde{p}_{\mathcal{B}}\ x_{\mathcal{B}} ≡ y_{\mathcal{B}}
|
||
\end{split}
|
||
\end{align}
|
||
%
|
||
The proof of the first one is:
|
||
%
|
||
\begin{align*}
|
||
\var{coe}\ \widetilde{p}_{\mathcal{A}}\ x_{\mathcal{A}}
|
||
& ≡ x_{\mathcal{A}} \lll \fst\ \inv{f} && \text{\ref{eq:coeDom} and the isomorphism $f, \inv{f}$} \\
|
||
& ≡ y_{\mathcal{A}} && \text{\ref{eq:pairArrowLaw} for $\inv{f}$}
|
||
\end{align*}
|
||
%
|
||
We have now constructed the maps between \ref{eq:univ-0} and \ref{eq:univ-1}. It
|
||
remains to show that they are inverses of each other. To cut a long story short,
|
||
the proof uses the fact that isomorphism-of is propositional and that arrows (in
|
||
both categories) are sets. The reader is referred to the implementation for the
|
||
gory details.
|
||
%
|
||
\subsection{Products are propositions}
|
||
%
|
||
Now that we have constructed the span category\index{span category} I
|
||
will demonstrate how to use this to prove that products are
|
||
propositions. On the face of it this may seem surprising. Products
|
||
look like they are a structure on categories. After all it consist of
|
||
a select element and two arrows given some two objects. If formulated
|
||
in set theory this would be the case but in the present setting
|
||
univalence of categories give us that products are properties. I will
|
||
show this by showing that terminal objects in the span category are
|
||
equivalent to products:
|
||
%
|
||
\begin{align}
|
||
\var{Terminal} ≃ \var{Product}\ ℂ\ \mathcal{A}\ \mathcal{B}
|
||
\end{align}
|
||
%
|
||
And as always we do this by constructing an isomorphism:
|
||
%
|
||
In the direction $\var{Terminal} → \var{Product}\ ℂ\ \mathcal{A}\ \mathcal{B}$
|
||
we are given a terminal object $X, x_𝒜, x_ℬ$. $X$ will be the product-object and
|
||
$x_𝒜, x_ℬ$ will be the product arrows, so it just remains to verify that this is
|
||
indeed a product. That is, for an object $Y$ and two arrows $y_𝒜 \tp
|
||
\Arrow\ Y\ 𝒜$, $y_ℬ\ \Arrow\ Y\ ℬ$ we must find a unique arrow $f \tp
|
||
\Arrow\ Y\ X$ satisfying:
|
||
%
|
||
\begin{align}
|
||
\label{eq:pairCondRev}
|
||
%% \begin{split}
|
||
( x_𝒜 \lll f ≡ y_𝒜 )
|
||
\x
|
||
( x_ℬ \lll f ≡ y_ℬ )
|
||
%% \end{split}
|
||
\end{align}
|
||
%
|
||
Since $X, x_𝒜, x_ℬ$ is a terminal object there is a \emph{unique} arrow from
|
||
this object to any other object, so also $Y, y_𝒜, y_ℬ$ in particular (which is
|
||
also an object in the span category). The arrow we will play the role of $f$ and
|
||
it immediately satisfies \ref{eq:pairCondRev}. Any other arrow satisfying these
|
||
conditions will be equal since $f$ is unique.
|
||
|
||
For the other direction we are now given a product $X, x_𝒜, x_ℬ$. Again this
|
||
will be the terminal object. So now it remains that for any other object there
|
||
is a unique arrow from that object into $X, x_𝒜, x_ℬ$. Let $Y, y_𝒜, y_ℬ$ be
|
||
another object. As the arrow $\Arrow\ Y\ X$ we choose the product-arrow $y_𝒜 \x
|
||
y_ℬ$. Since this is a product-arrow it satisfies \ref{eq:pairCondRev}. Let us
|
||
name the witness to this $\phi_{y_𝒜 \x y_ℬ}$. So we have picked as our center of
|
||
contraction $y_𝒜 \x y_ℬ , \phi_{y_𝒜 \x y_ℬ}$ we must now show that it is
|
||
contractible. So let $f \tp \Arrow\ X\ Y$ and $\phi_f$ be given (here $\phi_f$
|
||
is the proof that $f$ satisfies \ref{eq:pairCondRev}). The proof will be a pair
|
||
of proofs:
|
||
%
|
||
\begin{alignat}{3}
|
||
p \tp & \Path\ (\lambda\; i → \Arrow\ X\ Y)\quad
|
||
&& f\quad && y_𝒜 \x y_ℬ \\
|
||
& \Path\ (\lambda\; i → \Phi\ (p\ i))\quad
|
||
&& \phi_f\quad && \phi_{y_𝒜 \x y_ℬ}
|
||
\end{alignat}
|
||
%
|
||
Here $\Phi$ is given as:
|
||
$$
|
||
∏_{f \tp \Arrow\ Y\ X}
|
||
( x_𝒜 \lll f ≡ y_𝒜 )
|
||
×
|
||
( x_ℬ \lll f ≡ y_ℬ )
|
||
$$
|
||
%
|
||
$p$ follows from the universal property of $y_𝒜 \x y_ℬ$. For the latter we will
|
||
again use the same trick we did in \ref{eq:propAreInversesGen} and prove this
|
||
more general result:
|
||
%
|
||
$$
|
||
∏_{f \tp \Arrow\ Y\ X} \isProp\ (
|
||
( x_𝒜 \lll f ≡ y_𝒜 )
|
||
×
|
||
( x_ℬ \lll f ≡ y_ℬ )
|
||
)
|
||
$$
|
||
%
|
||
Which follows from arrows being sets and pairs preserving such. Thus we can
|
||
close the final proof with an application of $\lemPropF$.
|
||
|
||
This concludes the proof $\var{Terminal} ≃
|
||
\var{Product}\ ℂ\ \mathcal{A}\ \mathcal{B}$ and since we have that equivalences
|
||
preserve homotopic levels along with \ref{eq:termProp} we get our final result.
|
||
That in any category:
|
||
%
|
||
\begin{align}
|
||
∏_{A, B \tp \Object} \isProp\ (\var{Product}\ \bC\ A\ B)
|
||
\end{align}
|
||
%
|
||
\section{Functors and natural transformations}
|
||
For the sake of completeness I will mention the definition of functors
|
||
and natural transformations. Please refer to the implementation for
|
||
the full details.
|
||
%
|
||
\subsection{Functors}
|
||
Given two categories $\bC$ and $\bD$ a functor consists of the
|
||
following data:
|
||
%
|
||
\begin{align*}
|
||
\omapF & \tp ℂ.\Object → 𝔻.\Object \\
|
||
\fmap & \tp ℂ.\Arrow\ A\ B → 𝔻.\Arrow\ (\omapF\ A)\ (\omapF\ B)
|
||
\end{align*}
|
||
%
|
||
And the following laws:
|
||
\begin{align*}
|
||
\fmap\ ℂ.\identity & ≡ 𝔻.identity \\
|
||
\fmap\ (g \clll f) & ≡ \fmap\ g \dlll \fmap\ f
|
||
\end{align*}
|
||
%
|
||
The implementation can be found here:
|
||
%
|
||
\begin{center}
|
||
\sourcelink{Cat.Category.Functor}
|
||
\end{center}
|
||
\subsection{Natural Transformation}
|
||
Given two functors between categories $\bC$ and $\bD$. Name them
|
||
$\FunF$ and $\FunG$. A natural transformation is a family of arrows:
|
||
%
|
||
\begin{align*}
|
||
∏_{C \tp ℂ.\Object} \bD.\Arrow\ (\omapF\ C)\ (\omapG\ C)
|
||
\end{align*}
|
||
%
|
||
This family of arrows can be seen as the data. If $\theta$ is a
|
||
natural transformation $\theta\ C$ will be called the component (of
|
||
$\theta$) at $C$. The laws of this family of morphism is the
|
||
naturality condition:
|
||
%
|
||
\begin{align*}
|
||
∏_{f \tp ℂ.\Arrow\ A\ B}
|
||
(θ\ B) \dlll (\FunF.\fmap\ f) ≡ (\FunG.\fmap\ f) \dlll (θ\ A)
|
||
\end{align*}
|
||
%
|
||
The implementation can be found here:
|
||
%
|
||
\begin{center}
|
||
\sourcelink{Cat.Category.NaturalTransformation}
|
||
\end{center}
|
||
|
||
\section{Monads}
|
||
\label{sec:monads}
|
||
In this section I present two formulations of monads. The two representations
|
||
are referred to as the monoidal- and Kleisli- representation respectively or
|
||
simply monoidal monads and Kleisli monads for short. We then show that the two
|
||
formulations are equivalent, which due to univalence gives us a path between the
|
||
two types.
|
||
|
||
Let a category $\bC$ be given. In the remainder of this sections all
|
||
objects and arrows will implicitly refer to objects and arrows in this
|
||
category. I will also use the notation $\EndoR$ to refer to an
|
||
endofunctor on this category. Its map on objects will be denoted
|
||
$\omapR$ and its map on arrows will be denoted $\fmap$. Likewise I
|
||
will use the notation $\pureNT$ to refer to a natural transformation
|
||
and its component at a given (implicit) object will be denoted
|
||
$\pure$.
|
||
%
|
||
\subsection{Monoidal formulation}
|
||
The monoidal formulation of monads consists of the following data:
|
||
%
|
||
\begin{align}
|
||
\label{eq:monad-monoidal-data}
|
||
\begin{split}
|
||
\EndoR & \tp \Functor\ ℂ\ \bC \\
|
||
\pureNT & \tp \NT{\EndoR^0}{\EndoR} \\
|
||
\joinNT & \tp \NT{\EndoR^2}{\EndoR}
|
||
\end{split}
|
||
\end{align}
|
||
%
|
||
Here $\NTsym$ denotes natural transformations, the super-script in $\EndoR^2$
|
||
Denotes the composition of $\EndoR$ with itself. By the same token $\EndoR^0$ is
|
||
a curious way of denoting the identity functor. This notation has been chosen
|
||
for didactic purposes.
|
||
|
||
Denote the arrow-map of $\EndoR$ as $\fmap$, then this data must satisfy the
|
||
following laws:
|
||
%
|
||
\begin{align}
|
||
\label{eq:monad-monoidal-laws-0}
|
||
\join \lll \fmap\ \join
|
||
& ≡ \join \lll \join \\
|
||
\label{eq:monad-monoidal-laws-1}
|
||
\join \lll \pure\ & ≡ \identity \\
|
||
\label{eq:monad-monoidal-laws-2}
|
||
\join \lll \fmap\ \pure & ≡ \identity
|
||
\end{align}
|
||
\newcommand\monoidallaws{\ref{eq:monad-monoidal-laws-0}, \ref{eq:monad-monoidal-laws-1} and \ref{eq:monad-monoidal-laws-2}}%
|
||
%
|
||
The implicit arguments to the arrows above have been left out and the objects
|
||
they range over are universally quantified.
|
||
|
||
\subsection{Kleisli formulation}
|
||
%
|
||
The Kleisli-formulation consists of the following data:
|
||
%
|
||
\begin{align}
|
||
\begin{split}
|
||
\label{eq:monad-kleisli-data}
|
||
\omapR & \tp \Object → \Object \\
|
||
\pure & \tp % ∏_{X \tp Object}
|
||
\Arrow\ X\ (\omapR\ X) \\
|
||
\bind & \tp % ∏_{X\;Y \tp Object} → \Arrow\ X\ (\omapR\ Y)
|
||
\Arrow\ (\omapR\ X)\ (\omapR\ Y)
|
||
\end{split}
|
||
\end{align}
|
||
%
|
||
The objects $X$ and $Y$ are implicitly universally quantified. With this data we can construct the \nomenindex{Kleisli arrow}:
|
||
%
|
||
\begin{align*}
|
||
\fish & \tp \Arrow\ A\ (\omapR\ B)
|
||
→ \Arrow\ B\ (\omapR\ C)
|
||
→ \Arrow\ A\ (\omapR\ C) \\
|
||
f \fish g & ≜ f \rrr (\bind\ g)
|
||
\end{align*}
|
||
%
|
||
It is interesting to note here that this formulation does not talk about natural
|
||
transformations or other such constructs from category theory. All we have here
|
||
is a regular maps on objects and a pair of arrows.
|
||
%
|
||
This data must satisfy:
|
||
%
|
||
\begin{align}
|
||
\label{eq:monad-kleisli-laws-0}
|
||
\bind\ \pure & ≡ \identity_{\EndoR\ X} \\
|
||
\label{eq:monad-kleisli-laws-1}
|
||
\pure \fish f & ≡ f \\
|
||
\label{eq:monad-kleisli-laws-2}
|
||
(\bind\ f) \rrr (\bind\ g) & ≡ \bind\ (f \fish g)
|
||
\end{align}
|
||
\newcommand\kleislilaws{\ref{eq:monad-kleisli-laws-0}, \ref{eq:monad-kleisli-laws-1} and \ref{eq:monad-kleisli-laws-2}}%
|
||
%
|
||
Here likewise the arrows $f \tp \Arrow\ X\ (\omapR\ Y)$ and $g \tp
|
||
\Arrow\ Y\ (\omapR\ Z)$ are universally quantified as well as the
|
||
objects they range over.
|
||
%
|
||
\subsection{Equivalence of formulations}
|
||
%
|
||
The notation I have chosen here in the report
|
||
overloads e.g.\ $\pure$ to both refer to a natural transformation and an arrow.
|
||
This is of course not a coincidence as the arrow in the Kleisli formulation
|
||
shall correspond exactly to the map on arrows from the natural transformation
|
||
called $\pure$.
|
||
|
||
In the monoidal formulation we can define $\bind$:
|
||
%
|
||
\newcommand\joinX{\wideoverbar{\join}}%
|
||
\newcommand\bindX{\wideoverbar{\bind}}%
|
||
\newcommand\EndoRX{\wideoverbar{\EndoR}}%
|
||
\newcommand\pureX{\wideoverbar{\pure}}%
|
||
\newcommand\fmapX{\wideoverbar{\fmap}}%
|
||
\begin{align}
|
||
\bind\ f ≜ \join \lll \fmap\ f
|
||
\end{align}
|
||
%
|
||
And likewise in the Kleisli formulation we can define $\join$:
|
||
%
|
||
\begin{align}
|
||
\join ≜ \bind\ \identity
|
||
\end{align}
|
||
%
|
||
It now remains to show that this construction indeed gives rise to a
|
||
monad. This will be done in two steps. First we will assume that we
|
||
have a monad in the monoidal form; $(\EndoR, \pure, \join)$ and then
|
||
show that $(\omapR, \pure, \bind)$ is indeed a monad in the Kleisli
|
||
form. In the second part we will show the other direction.
|
||
|
||
\subsubsection{Monoidal to Kleisli}
|
||
Let $(\EndoR, \pureNT, \joinNT)$ be given as in \ref{eq:monad-monoidal-data}
|
||
satisfying the laws \monoidallaws. For the data of the Kleisli
|
||
formulation we pick:
|
||
%
|
||
\begin{align}
|
||
\begin{split}
|
||
\omapR & ≜ \omapR \\
|
||
\pure & ≜ \pure \\
|
||
\bind\ f & ≜ \join \lll \fmap\ f
|
||
\end{split}
|
||
\end{align}
|
||
%
|
||
Again $\omapR$ is the object map of the endo-functor $\EndoR$, $\pure$
|
||
and $\join$ are the arrows from the natural transformations $\pureNT$
|
||
and $\joinNT$ respectively and $\fmap$ is the map on arrows of the
|
||
endofunctor $\EndoR$. It now just remains to verify the laws
|
||
\kleislilaws. For \ref{eq:monad-kleisli-laws-0}:
|
||
%
|
||
\begin{align*}
|
||
\bind\ \pure & =
|
||
\join \lll (\fmap\ \pure) \\
|
||
& ≡ \identity && \text{By \ref{eq:monad-monoidal-laws-2}}
|
||
\end{align*}
|
||
%
|
||
For \ref{eq:monad-kleisli-laws-1}:
|
||
%
|
||
\begin{align*}
|
||
\pure \fish f
|
||
& = %%%
|
||
\pure \ggg \bind\ f \\ & =
|
||
\bind\ f \lll \pure \\ & =
|
||
\join \lll \fmap\ f \lll \pure \\ & ≡
|
||
\join \lll \pure \lll f && \text{$\pure$ is a natural transformation} \\ & ≡
|
||
\identity \lll f && \text{By \ref{eq:monad-monoidal-laws-1}} \\ & ≡
|
||
f && \text{Left identity}
|
||
\end{align*}
|
||
%
|
||
For \ref{eq:monad-kleisli-laws-2}:
|
||
\begin{align*}
|
||
\bind\ g \rrr \bind\ f & =
|
||
\bind\ f \lll \bind\ g
|
||
\\ & =
|
||
%% %%%%
|
||
\join \lll \fmap\ g \lll \join \lll \fmap\ f
|
||
\\ & ≡
|
||
\join \lll \join \lll (\fmap \comp \fmap)\ f \lll \fmap\ g
|
||
&& \text{$\join$ is a natural transformation} \\ & ≡
|
||
\join \lll \fmap\ \join \lll (\fmap \comp \fmap)\ f \lll \fmap\ g
|
||
&& \text{By \ref{eq:monad-monoidal-laws-0}} \\ & ≡
|
||
\join \lll \fmap\ \join \lll \fmap\ (\fmap\ f) \lll \fmap\ g
|
||
&& \text{} \\ & ≡
|
||
\join \lll \fmap\ (\join \lll \fmap\ f \lll g)
|
||
&& \text{Distributive law for functors} \\ & =
|
||
\join \lll \fmap\ (\join \lll \fmap\ f \lll g) \\ & =
|
||
%%%%
|
||
\bind\ (\bind\ f \lll g) \\ & =
|
||
\bind\ (g \rrr \bind\ f) \\ & =
|
||
\bind\ (g \fish f)
|
||
\end{align*}
|
||
%
|
||
The construction can be found in the module:
|
||
\begin{center}
|
||
\sourcelink{Cat.Category.Monad.Monoidal}
|
||
\end{center}
|
||
%
|
||
\subsubsection{Kleisli to Monoidal}
|
||
For the other direction we are given $(\omapR, \pure, \bind)$ as in
|
||
\ref{eq:monad-kleisli-data} satisfying the laws \kleislilaws. For the data of
|
||
the monoidal formulation we pick:
|
||
%
|
||
\begin{align}
|
||
\begin{split}
|
||
\EndoR & ≜ (\omapR, \bind\ (\pure \lll f)) \\
|
||
\pure & ≜ \pure \\
|
||
\join & ≜ \bind\ \identity
|
||
\end{split}
|
||
\end{align}
|
||
%
|
||
We must now not only show the monad laws given for the monoidal
|
||
formulation (\monoidallaws), we must also verify that $\EndoR$ is a
|
||
functor and that $\pure$ and $\join$ are natural transformations. I
|
||
will ommit this here. In stead we shall see how these two mappings are
|
||
indeed inverses. The full construction can be found in the module:
|
||
\begin{center}
|
||
\mbox{\sourcelink{Cat.Category.Monad.Kleisli}}
|
||
\end{center}
|
||
%
|
||
\subsubsection{Equivalence}
|
||
To prove that the two formulations are equivalent we must demonstrate
|
||
that the two mappings sketched above are indeed inverses of each
|
||
other. To recap, these maps are:
|
||
%
|
||
\begin{align*}
|
||
\toKleisli & \tp \var{Kleisli} → \var{Monoidal} \\
|
||
\toKleisli & ≜ \lambda\ (\omapR, \pure, \bind)
|
||
→ (\EndoR, \pure, \bind\ \identity)
|
||
\end{align*}
|
||
%
|
||
Where $\EndoR ≜ (\omapR, \bind\ (\pure \lll f))$. The proof that
|
||
this is indeed a functor is left implicit as well as the monad laws.
|
||
Likewise the proof that $\pure$ and $\bind\ \identity$ are natural
|
||
transformations are left implicit. The inverse map will be:
|
||
%
|
||
\begin{align*}
|
||
\toMonoidal & \tp \var{Monoidal} → \var{Kleisli} \\
|
||
\toMonoidal & ≜ \lambda\ (\EndoR, \pureNT, \joinNT)
|
||
→ (\omapR, \pure, \bind)
|
||
\end{align*}
|
||
%
|
||
Where $\bind\ f ≜ \join \lll \fmap\ f$. Again the monad laws are
|
||
left implicit. Now we must show:
|
||
%
|
||
\begin{align}
|
||
\label{eq:monad-forwards}
|
||
\toKleisli \comp \toMonoidal & ≡ \identity \\
|
||
\label{eq:monad-backwards}
|
||
\toMonoidal \comp \toKleisli & ≡ \identity
|
||
\end{align}
|
||
%
|
||
For \ref{eq:monad-forwards} let $(\omapR, \pure, \bind)$ be a monad in
|
||
the Kleisli form. Since being-a-monad is a proposition\footnote{The
|
||
proof can be found in the implementation.} we get an
|
||
equality-principle for kleisli-monads that say that to equate two such
|
||
monads it suffices to equate their data-part. So it suffices to equate
|
||
the data-parts of the \ref{eq:monad-forwards}. Such a proof is a
|
||
triple equating the three projections of \ref{eq:monad-kleisli-data}.
|
||
The first two hold definitionally -- essentially one just wraps and
|
||
unwraps the morphism in a functor. For the last equation a little more
|
||
work is required:
|
||
%
|
||
\begin{align*}
|
||
\join \lll \fmap\ f & =
|
||
\fmap\ f \rrr \join \\ & =
|
||
\bind\ (f \rrr \pure) \rrr \bind\ \identity
|
||
&& \text{By definition of $\fmap$ and $\join$} \\ & ≡
|
||
\bind\ (f \rrr \pure \fish \identity)
|
||
&& \text{By \ref{eq:monad-kleisli-laws-2}} \\ & ≡
|
||
\bind\ (f \rrr \identity)
|
||
&& \text{By \ref{eq:monad-kleisli-laws-1}} \\ & =
|
||
\bind\ f
|
||
\end{align*}
|
||
%
|
||
For the other direction (\ref{eq:monad-backwards}) we are given a
|
||
monad in the monoidal form; $(\EndoR, \pureNT, \joinNT)$. The various
|
||
equality-principles again give us that it is sufficient to equate the
|
||
data-part of the above. That is, we only need to verify that the
|
||
following pieces of data: $\omapR$, $\fmap$, $\pure$ and $\join$ get
|
||
mapped correctly. To see the full details check the implementation in
|
||
the module:
|
||
%
|
||
\begin{center}
|
||
\sourcelink{Cat.Category.Monad}
|
||
\end{center}
|