cat/doc/implementation.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}%
%
I also provide a 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.
In the interest of brevity I will not detail all the things I have
formalized.  Instead 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.

Categories whose type of arrows form a set 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}).  However this thesis 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 the arrows to be univalent.  Before we can define
this, I must introduce two additional 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 $\idToIso$ 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}
%
The function $\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 arrows ($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)
$$
%
We then 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.  Instead
the path type must be used directly.

The type \ref{eq:propIsPreCategory} is judgmentally the same as:
%
$$
∏_{a, b \tp \IsPreCategory} a ≡ b
$$
%
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
$$
%
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 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 of being a pre-category and the univalence condition.  Recall
that the univalence condition is indexed by the identity-proof.  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
$$
%
This path 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}.

Looking at the definition of $\lemPropF$ we have that $A =
\var{IsIdentity}\ \identity$ and $D = \Univalent$ to give the path at
hand.  We have shown that being a category is a proposition, a result
that holds for any choice of identity proof so it will also hold for
the witness obtained at an arbitrary point along $p$.  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
$$
%
In summary the heterogeneous path is inhabited by:
%
$$
\var{lemPropF}\ \var{propUnivalent}\ (\var{cong}\ p.\var{isIdentity})
$$
%
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
$$
This is 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
theorem -- i.e.\ provably holds) does not imply univalence of all
pre-category since morphisms in a category are not regular functions,
instead they can be thought of as a generalization hereof.  The
univalence criterion therefore is simply a way of restricting arrows
to behave like regular functions with respects to paths.

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 \defeq \idToIso\ (\iota, \inv{\iota}, \dots) \tp A ≡ B$$
%
From this equality we can get two further paths:
%
\begin{align*}
  p_{\var{dom}} & \tp \Arrow\ A\ X ≡ \Arrow\ B\ X \\
  p_{\var{cod}} & \tp \Arrow\ X\ A ≡ \Arrow\ X\ B
\end{align*}
%
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 (\idToIso\ p)_2 && \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$.  The subscript in term $(\idToIso\ p)_2$ is
intended to denote the inverse map $B → A$ from 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 (\idToIso\ p)_{2}
\end{equation}
%
Again $p_{\var{dom}}$ denotes the path $\Arrow\ A\ X ≡ \Arrow\ B\ X$
induced by $p$.  To prove this statement let $f$ and $p$ be given then
we 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}_{\var{dom}}}\ f
  ≡
  f \lll (\idToIso\ \widetilde{p})_{2}
\end{align}
The base-case therefore becomes
$d \tp \var{coe}\ \refl_{\var{dom}}\ f ≡ f \lll (\idToIso\ \refl)_{2}$
and is inhabited by:
\begin{align*}
  \var{coe}\ \refl_{\var{dom}}\ 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 (\idToIso\ \refl)_{2}
  && \text{By definition of $\idToIso$}\\
\end{align*}
%
To close the based-path-induction we must supply the value ``at the
other end''.  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}
%
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 rather than being
distracted by some intricate structure of the category.

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 a line above them.  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$ (and a witness to them being
inverses).  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 goes 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 concludes the proof that the opposite category is in fact a
category.  Now, to prove that opposite-of is an involution we must
show:
%
$$
∏_{\bC \tp \Category} \left(\bC^{\var{Op}}\right)^{\var{Op}} ≡ \bC
$$
%
The laws in $\left(\bC^{\var{Op}}\right)^{\var{Op}}$ get quite
involved.  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 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$.  Instead 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*}

Since $≃$ is an equivalence relation we can chain these equivalences
together.  Step one will be proven with the 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
for types.  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$.  We must finally prove:
%
\begin{align}
  \label{eq:equivIso}
  ∏_{f \tp A → B} \left( \isEquiv\ A\ B\ f ≃ \Isomorphism\ f \right)
\end{align}

Lets us first 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*}
%
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 of one another 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.  Instead, 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$.  To this end 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.  Instead 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$.
Since terminal objects are propositional in a proper category and
equivalences preserve homotopy level, then we know that products are
also 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 say
that a product is triple consisting of an object and a pair of arrows.
The object is denoted with $A × B$ in $\bC$ and is also referred to as
the product (object) of $A$ and $B$.  The arrows will be named $\pi_1
\tp A \x B → A$ and $\pi_2 \tp A \x B → B$ also 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}
%
The arrow $\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 construct the \nomenindex{span category}.  The type of
objects in this category shall 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_{\pairA} ,\ a_{\pairB}$ and $B ,\ b_{\pairA} ,\ b_{\pairB}$ in this
category will consist of an arrow from the underlying category $\pairf \tp
\Arrow\ A\ B$ satisfying:
%
\begin{align}
  \label{eq:pairArrowLaw}
  b_{\pairA} \lll f ≡ a_{\pairA} \x
  b_{\pairB} \lll f ≡ a_{\pairB}
\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_{\pairA} \lll (f \lll g)
  & ≡
  (c_{\pairA} \lll f) \lll g
  && \text{Associativity} \\
  & ≡
  b_{\pairA} \lll g
  && \text{$f$ satisfies \ref{eq:pairArrowLaw}} \\
  & ≡
  a_{\pairA}
  && \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 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}
%
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 for the purpose of this exposition
it will suffice to show the type of the path space.  Note that the
arrows in \ref{eq:productAssoc} are arrows between objects on the form
$\wideoverbar{A} = (A , a_{\pairA} , a_{\pairB})$ to $\wideoverbar{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 ≡ a_{\pairA} × d_{\pairB} \lll p\ i ≡ a_{\pairB}
\end{align}
%
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, instead 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}$.  This follows from the fact that $∏$ and $∑$ preserve
homotopical structure.  \ref{eq:productEqPrinc} gives us an equality
principle for arrows in this category.  The equality principle 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} using
\ref{eq:productAssocUnderlying}.

We must now prove that the arrows form a set:
%
$$
\isSet\ (\Arrow\ \wideoverbar{X}\ \wideoverbar{Y})
$$
%
Since pairs preserve homotopical structure this reduces to the
following two obligations: The first one is:
%
$$
\isSet\ (\bC.\Arrow\ X\ Y)
$$
%
which holds.  The other one is:
%
$$
∏_{f \tp \Arrow\ X\ Y}
\isSet\ \left( y_{\pairA} \lll f ≡ x_{\pairA}
× y_{\pairB} \lll f ≡ x_{\pairB}
\right)
$$
%
We get this from \ref{eq:productEqPrinc} and the fact that homotopical
structure is cumulative.

That concludes the proof that this is a valid pre-category.

\subsubsection{Univalence}
To prove that this is a proper category we must additionally prove the
univalence criterion.  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 instead 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}
%
The proof is a chain of isomorphisms between the types
\ref{eq:univ-0}, \ref{eq:univ-1}, \ref{eq:univ-2} and \ref{eq:univ-3}.
I will highlight the most interesting bits of this proof.  For the
full proof see the implementation in the same module:
%
\begin{center}
  \sourcelink{Cat.Categories.Span}
\end{center}

\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$.

\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}, \var{inv}_f)$.  We
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 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}$ are inverses, but this is of course just $\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}, \var{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 a proposition and that arrows (in both categories)
are sets.  The reader is referred to the implementation for the full
gory details.
%
\subsection{To have products is a property of a category}
%
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 object and two arrows.  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.  In particular we have $Y,
y_𝒜, y_ℬ$.  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.  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_ℬ}$.  We have picked as our center of
contraction $y_𝒜 \x y_ℬ , \phi_{y_𝒜 \x y_ℬ}$ we must now show that it
is contractible.  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_ℬ )
$$
%
We can construct $p$ from the universal property of $y_𝒜 \x y_ℬ$.  For
the latter we 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 is, in any category $\bC$ we have:
%
\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 briefly 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}
\label{sec:nat-trans}
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.  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$. This is the same notation as in \S\ref{sec:nat-trans}.
%
\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{\widehat{\identity}}{\EndoR} \\
    \joinNT  & \tp \NT{(\EndoR \oplus \EndoR)}{\EndoR}
\end{split}
\end{align}
%
Here $\NTsym$ denotes natural transformations and $\oplus$ means
functor composition.

Note that $\fmap$ is $\EndoR$'s map on arrows.  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 \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 mention
functors nor natural transformations.  All we have here is a regular
map on objects and a pair of arrows.
%
This data must satisfy:
%
\begin{align}
\label{eq:monad-kleisli-laws-0}
\bind\ \pure & ≡ \identity_{\omapR\ 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.  The third law is stated in terms of reverse
function composition to mirror the way in which it interacts with the
Kleisli arrow.
%
\subsection{Equivalence of formulations}
%
Both formulations mention a map called $\pure$.  This is of course no
coincidence as that arrow in the Kleisli formulation shall correspond
exactly to the map on arrows for the natural transformation in the
monoidal formulation.

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.  Instead 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 was omitted here but 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.  It thus
suffices to equate the data parts of \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}