cat/doc/implementation.tex

This implementation formalizes the following concepts:
%
\begin{itemize}
\item Core categorical concepts
\subitem Categories
\subitem Functors
\subitem Products
\subitem Exponentials
\subitem Cartesian closed categories
\subitem Natural transformations
\subitem Yoneda embedding
\subitem Monads
\subsubitem Monoidal monads
\subsubitem Kleisli monads
\subsubitem Voevodsky's construction
\item Category of \ldots
\subitem Homotopy sets
\subitem Categories -- only data-part
\subitem Relations -- only data-part
\subitem Functors -- only as a precategory
\subitem Free category
\end{itemize}
%
Since it is useful to distinguish between types with more or less (homotopical)
structure I have followed the following design-principle: I have split concepts
up into things that represent ``data'' and ``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: `raw` which is a collection of the data
and `isCategory` which asserts some laws about that data.

This allows me to reason about things in a more mathematical way, where one can
reason about two categories by simply focusing on the data. This is acheived by
creating a function embodying the ``equality principle'' for a given type.

\section{Categories}
The data for a category consist of objects, morphisms (or arrows as I will refer
to them henceforth), the identity arrow and composition of arrows.

Another record encapsulates some laws about this data: associativity of
composition, identity law for the identity morphism. These are standard
requirements for being a category as can be found in standard mathematical
expositions on the topic. We, however, impose one further requirement on what it
means to be a category, namely that the type of arrows form a set. We could
relax this requirement, this would give us the notion of higher categorier
(\cite[p. 307]{hott-2013}). For the purpose of this project, however, this
report will restrict itself to 1-categories.

Raw categories satisfying these properties are called a pre-categories.

As a further requirement to be a proper category we require it to be univalent.
This requirement is quite similiar to univalence for types, but we let
isomorphism on objects play the role of equivalence on types. The univalence
criterion is:
%
$$
\isEquiv\ (A \equiv B)\ (A \approxeq B)\ \idToIso
$$
%
Here $\approxeq$ denotes isomorphism on objects (whereas $\cong$ denotes
isomorphism of types).

Note that this is not the same as:
%
$$
(A \equiv B) \simeq (A \approxeq B)
$$
%
The two types are logically equivalent, however. 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.

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. Lets have a look at one of them: The
identity law states that:
%
$$
\prod_{A\ B \tp \Object} \prod_{f \tp A \to B} \id \comp f \equiv f \x f \comp \id \equiv f
$$
%
There are multiple ways to prove this. Perhaps one of the more intuitive proofs
is by way of the following `combinators':
%
$$
\mathit{propPi} \tp \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\prod_{a \tp A} P\ a\right)
$$
%
I.e.; pi-types preserve propositionality when the co-domain is always a
proposition.
%
$$
\mathit{propSig} \tp \isProp\ A \to \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\sum_{a \tp A} P\ a\right)
$$
%
I.e.; sigma-types preserve propositionality whenever it's first component is a
proposition, and it's second component is a proposition for all points of in the
left type.

So the proof goes like this: We `eliminate' the 3 function abstractions by
applying $\propPi$ three times. So our proof obligation becomes:
%
$$
\isProp \left( \id \comp f \equiv f \x f \comp \id \equiv f \right)
$$
%
then we eliminate the (non-dependent) sigma-type by applying $\propSig$ giving
us the two obligations: $\isProp\ (\id \comp f \equiv f)$ and $\isProp\ (f \comp
\id \equiv 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 $\sum$ and $\prod$. Similiar 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've defined
ourselves. For instance, after we've proven that all the projections of
pre-categories are propositions, then we would like to bundle this up to show
that the type of pre-categories is also a proposition. Since pre-categories are
not formulated with a chain of sigma-types we wont have any combinators
available to help us here. In stead we'll have to use the path-type directly.

What we want to prove is:
%
$$
\isProp\ \IsPreCategory
$$
%
Which is judgmentally the same as
%
$$
\prod_{a\ b \tp \IsPreCategory} a \equiv b
$$
%
So let $a\ b \tp \IsPreCategory$ be given. To prove the equality $a \equiv b$ is
to give a continuous path from the index-type into path-space - in this case
$\IsPreCategory$. This path must satisfy being being judgmentally the same as
$a$ at the left endpoint and $b$ at the right endpoint. I.e. a function $I \to
\IsPreCategory$. 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 $\isIdentity_a$ and $\isIdentity_b$
is simply formed by:
%
$$
\propIsIdentity\ \isIdentity_a\ \isIdentity_b \tp \isIdentity_a \equiv \isIdentity_b
$$
%
So to give the continuous function $I \to \IsPreCategory$ that is our goal we
introduce $i \tp I$ and proceed by constructing an element of $\IsPreCategory$
by using that all the projections are propositions to generate paths between all
projections. Once we have such a path e.g. $p : \isIdentity_a \equiv
\isIdentity_b$ we can elimiate it with $i$ and thus obtaining $p\ i \tp
\isIdentity_{p\ i}$ and this element satisfies exactly that it corresponds to
the corresponding projections at either endpoint. Thus the element we construct
at $i$ becomes:
%
\begin{align*}
  & \{\ \mathit{propIsAssociative}\   \mathit{isAssociative}_x\
       \mathit{isAssociative}_y\ i  \\
  & ,\  \mathit{propIsIdentity}\      \mathit{isIdentity}_x\
       \mathit{isIdentity}_y\ i  \\
  & ,\  \mathit{propArrowsAreSets}\ \mathit{arrowsAreSets}_x\
       \mathit{arrowsAreSets}_y\ i  \\
  & \}
\end{align*}
%
I've found that 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
extensionality (the projections are all $\prod$-types). Assuming we had
functional extensionality available to us as an axiom, we would use functional
extensionality (in reverse?) to retreive the equalities in $a$ and $b$,
pattern-match on them to see that they are both $\mathit{refl}$ and then close
the proof with $\mathit{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.
$\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 if we follow the same recipe as above, let $a\ b \tp
\IsCategory$, to show them equal, we now need to give two paths. One homogenous:
%
$$
p_{\isPreCategory} \tp \isPreCategory_a \equiv \isPreCategory_b
$$
%
and one heterogeneous:
%
$$
\Path\ (\lambda\; i \mto Univalent_{p\ i})\ \isPreCategory_a\ \isPreCategory_b
$$
%
Which depends on the choice of $p_{\isPreCategory}$. 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 becasue $\isProp$ talks about non-dependent paths. To
`promote' this to a dependent path we can use another useful combinator;
$\lemPropF$. Given a type $A \tp \MCU$ and a type family on $A$; $B : A \to
\MCU$. Let $P$ be a proposition indexed by an element of $A$ and say we have a
path between some two elements in $A$; $p : a_0 \equiv a_1$ then we can built a
heterogeneous path between any two $b$'s at the endpoints:
%
$$
\Path\ (\lambda\; i \mto B\ (p\ i))\ b0\ b1
$$
%
where $b_0 \tp B a_0$ and $b_1 \tp B\ a_1$. This is quite a mouthful, but the
example at present should serve as an illustration. In this case $A =
\mathit{IsIdentity}\ \mathit{identity}$ and $B = \mathit{Univalent}$ we've 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_{\isPreCategory}$ by
applying using congruence of paths: $\congruence\ \mathit{isIdentity}\
p_{\isPreCategory}$

When we have a proper category we can make precise the notion of ``identifying
isomorphic types'' \TODO{cite awodey here}. That is, we can construct the
function:
%
$$
\isoToId \tp (A \approxeq B) \to (A \equiv B)
$$
%
One application of this, and a perhaps somewhat surprising result, is that
terminal objects are propositional. Intuitively; they do not have any
interesting structure. The proof of this follows from the usual observation that
any two terminal objects are isomorphic. The proof is omitted here, but the
curious reader can check the implementation for the details. \TODO{The proof is
a bit fun, should I include it?}

\section{Equivalences}
\label{sec:equiv}
The usual notion of a function $f : A \to B$ having an inverses is:
%
$$
\sum_{g : B \to A} f \comp g \equiv \identity_{B} \x g \comp f \equiv \identity_{A}
$$
%
This is defined in \cite[p. 129]{hott-2013} and is referred to as the a
quasi-inverse. At the same place \cite{hott-2013} gives an ``interface'' for
what an equivalence $\isEquiv : (A \to B) \to \MCU$ must supply:
%
\begin{itemize}
\item
  $\qinv\ f \to \isEquiv\ f$
\item
  $\isEquiv\ f \to \qinv\ f$
\item
  $\isEquiv\ f$ is a proposition
\end{itemize}
%
Having such an interface gives us both 1) a way to think rather abstractly about
how to work with equivalences and 2) to use ad-hoc definitions of equivalences.
The specific instantiation of $\isEquiv$ as defined in \cite{cubical-agda} is:
%
$$
isEquiv\ f \defeq \prod_{b : B} \isContr\ (\fiber\ f\ b)
$$
where
$$
\fiber\ f\ b \defeq \sum_{a \tp A} b \equiv f\ a
$$
%
I give it's 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 first function from the list of requirements we will call
$\mathit{fromIsomorphism}$, this is known as $\mathit{gradLemma}$ in
\cite{cubical-agda} the second one we will refer to as $\mathit{toIsmorphism}$. It's
implementation can be found in the sources. Likewise the proof that this
equivalence is propositional 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:
%
$$
A \simeq B \defeq \sum_{f \tp A \to B} \isEquiv\ f
$$
%
Note that the term equivalence here is overloaded referring both to the map $f
\tp A \to B$ and the type $A \simeq B$. I will use these conflated terms when it
it is clear from the context what is being referred to.

Just like we could promote a quasi-inverse to an equivalence we can promote an
isomorphism to an equivalence:
%
$$
\mathit{fromIsomorphism} \tp A \cong B \to A \simeq B
$$
%
and vice-versa:
%
$$
\mathit{toIsomorphism} \tp A \simeq B \to A \cong 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 \to B$ that witness this.

Both $\cong$ and $\simeq$ form equivalence relations.

\section{Univalence}
\label{univalence}
As noted in the introduction the univalence for types $A\; B \tp \Type$ states
that:
%
$$
\mathit{Univalence} \defeq (A \equiv B) \simeq (A \simeq B)
$$
%
As mentioned the univalence criterion for some category $\bC$ says that for all
\emph{objects} $A\;B$ we must have:
$$
\isEquiv\ (A \equiv B)\ (A \approxeq B)\ \idToIso
$$
And I mentioned that this was logically equivalent to
%
$$
(A \equiv B) \simeq (A \approxeq B)
$$
%
Given that we saw in the previous section that we can construct an equivalence
from an isomorphism it suffices to demonstrate:
%
$$
(A \equiv B) \cong (A \approxeq B)
$$
%
That is, we must demonstrate that there is an isomorphism (on types) between
equalities and isomorphisms (on arrows). It's 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 in any category since morphisms in a category are not regular maps --
in stead they can be thought of as a generalization hereof; i.e. arrows. The
univalence criterion therefore is simply a way of restricting arrows to behave
similarly to maps.

I will now mention a few helpful thoerems that follow from univalence that will
become useful later.

Obviously univalence gives us an isomorphism $A \equiv B \to A \approxeq B$. I
will name these for convenience:
%
$$
\idToIso \tp A \equiv B \to A \approxeq B
$$
%
$$
\isoToId \tp A \approxeq B \to A \equiv B
$$
%
The next few theorems are variations on theorem 9.1.9 from \cite{hott-2013}. Let
an isomorphism $A \approxeq B$ in some category $\bC$ be given. Name the
isomorphism $\iota \tp A \to B$ and its inverse $\widetilde{\iota} \tp B \to A$.
Since $\bC$ is a category (and therefore univalent) the isomorphism induces a
path $p \tp A \equiv B$. From this equality we can get two further paths:
$p_{\mathit{dom}} \tp \mathit{Arrow}\ A\ X \equiv \mathit{Arrow}\ A'\ X$ and
$p_{\mathit{cod}} \tp \mathit{Arrow}\ X\ A \equiv \mathit{Arrow}\ X\ A'$. We
then have the following two theorems:
%
$$
\mathit{coeDom} \tp \prod_{f \tp A \to X} \mathit{coe}\ p_{\mathit{dom}}\ f \equiv f \lll \widetilde{\iota}
$$
%
%
\begin{align}
\label{eq:coeCod}
\mathit{coeCod} \tp \prod_{f \tp A \to X} \mathit{coe}\ p_{\mathit{cod}}\ f \equiv \iota \lll f
\end{align}
%
I will give the proof of the first theorem here, the second one is analagous.
\begin{align*}
\mathit{coe}\ p_{\mathit{dom}}\ f
  & \equiv f \lll \mathit{obverse}_{\mathit{idToIso}\ p} && \text{lemma} \\
  & \equiv f \lll \widetilde{\iota}
    && \text{$\mathit{idToIso}$ and $\mathit{isoToId}$ are inverses}\\
\end{align*}
%
In the second step we use the fact that $p$ is constructed from the isomorphism
$\iota$ -- $\mathit{obverse}$ denotes the map $B \to A$ induced by the
isomorphism $\mathit{idToIso}\ p \tp A \cong B$. The helper-lemma is similar to
what we're trying to prove but talks about paths rather than isomorphisms:
%
$$
\prod_{f \tp \mathit{Arrow}\ A\ B} \prod_{p \tp A \equiv A'} \mathit{coe}\ p^*\ f \equiv f \lll \mathit{obverse}_{\mathit{idToIso}\ p}
$$
%
Note that the asterisk in $p^*$ denotes the path $\mathit{Arrow}\ A\ B \equiv
\mathit{Arrow}\ A'\ B$ 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 \mathit{Object}$, so let $\widetilde{A} \tp \Object$ and $\widetilde{p} \tp
A \equiv \widetilde{A}$ be given. The family that we perform induction over will
be:
%
$$
\mathit{coe}\ {\widetilde{p}}^*\ f \equiv f \lll \mathit{obverse}_{\mathit{idToIso}\ \widetilde{p}}
$$
The base-case therefore becomes:
\begin{align*}
\mathit{coe}\ {\widetilde{\refl}}^*\ f
& \equiv f \\
& \equiv f \lll \mathit{identity} \\
& \equiv f \lll \mathit{obverse}_{\mathit{idToIso}\ \widetilde{\refl}}
\end{align*}
%
The first step follows because reflixivity is a neutral element for coercions.
The second step is the identity law in the category. The last step has to do
with the fact that $\mathit{idToIso}$ is constructed by substituting according
to the supplied path and since reflexivity is also the neutral element for
substuitutions we arrive at the desired expression. To close the
based-path-induction we must supply the value at the other end and the
connecting path, but in this case this is simply $A' \tp \Object$ and $p \tp A
\equiv A'$ which we have.
%
\section{Categories}
\subsection{Opposite category}
\label{op-cat}
The first category I'll present is a pure construction on categories. Given some
category we can construct it's 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^{\mathit{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.

Showing that this forms a pre-category is rather straightforward. I'll state the
laws in terms of the underlying category $\bC$:
%
$$
h \rrr (g \rrr f) \equiv h \rrr g \rrr f
$$
%
Since $\rrr$ is reverse function composition this is just the symmetric version
of associativity.
%
$$
\mathit{identity} \rrr f \equiv f \x f \rrr identity \equiv 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 $\Hom_{A\ B}$ is a set for all $A\ B \tp
\Object$ then so is $\Hom_{B\ A}$.

Now, to show that this category is univalent is not as straight-forward. Lucliy
section \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
$\idToIso_{\mathit{Op}} \tp (A \equiv B) \to (A \approxeq_{\mathit{Op}} B)$.
From the original category we have that $\idToIso \tp (A \equiv B) \to (A \cong
B)$ is an isomorphism. Let us denote it's inverse with $\eta \tp (A \approxeq B)
\to (A \equiv B)$. If we squint we can see what we need is a way to go between
$\approxeq_{\mathit{Op}}$ and $\approxeq$, well, an inhabitant of $A \approxeq
B$ is simply an arrow $f \tp \mathit{Arrow}\ A\ B$ and it's inverse $g \tp
\mathit{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 $\mathit{shuffle} \tp (A \approxeq B) \to (A
\approxeq_{\bC} B)$ and $\mathit{shuffle}^{-1} : (A \approxeq_{\bC} B) \to (A
\approxeq B)$ respectively.

As the inverse of $\idToIso_{\mathit{Op}}$ I will pick $\zeta \defeq \eta \comp
\mathit{shuffle}$. The proof that they are inverses go as follows:
%
\begin{align*}
\zeta \comp \idToIso & \equiv
\eta \comp \shuffle \comp \idToIso
&& \text{by definition} \\
%% ≡⟨ cong (λ φ → φ x) (cong (λ φ → η ⊙ shuffle ⊙ φ) (funExt lem)) ⟩ \\
%
& \equiv
\eta \comp \shuffle \comp \inv{\shuffle} \comp \idToIso
&& \text{lemma} \\
%%   ≡⟨⟩ \\
& \equiv
\eta \comp \idToIso_{\bC}
&& \text{$\shuffle$ is an isomorphism} \\
%%   ≡⟨ (λ i → verso-recto i x) ⟩ \\
& \equiv
\identity
&& \text{$\eta$ is an ismorphism}
\end{align*}
%
The other direction is analogous.

The lemma used in this proof states that $\idToIso \equiv \inv{\shuffle} \comp
\idToIso_{\bC}$ it's a rather straight-forward proof since being-an-inverse-of
is a proposition.

So, in conclusion, we've shown that the opposite category is indeed a category.

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:
%
$$
\prod_{\bC \tp \mathit{Category}} \left(\bC^{\mathit{Op}}\right)^{\mathit{Op}} \equiv \bC
$$
%
As we've seen the laws in $\left(\bC^{\mathit{Op}}\right)^{\mathit{Op}}$ get
quite involved.\footnote{We haven't even seen the full story because we've 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 lets 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:
%
$$
\mathit{raw}\ \left(\bC^{\mathit{Op}}\right)^{\mathit{Op}} \equiv \mathit{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_\ell \defeq \sum_{A \tp \MCU_\ell} \isSet\ A$$
%
The more straight-forward notion of a category where the objects are types is
not a valid (1-)category. Since in cubical Agda types can have higher homotopic
structure.

Univalence does not follow immediately from univalence for types:
%
$$(A \equiv B) \simeq (A \simeq B)$$
%
Because here $A\ B \tp \Type$ whereas the objects in this category have the type
$\Set$ so we cannot form the type $\mathit{hA} \simeq \mathit{hB}$ for objects
$\mathit{hA}\;\mathit{hB} \tp \Set$. In stead I show that this category
satisfies:
%
$$
(\mathit{hA} \equiv \mathit{hB}) \simeq (\mathit{hA} \approxeq \mathit{hB})
$$
%
Which, as we saw in section \ref{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) \equiv (B, s_B))
 & \simeq (A \equiv B) && \ref{eq:equivPropSig} \\
 & \simeq (A \simeq B) && \text{Univalence} \\
 & \simeq ((A, s_A) \approxeq (B, s_B)) && \text{\ref{eq:equivSig} and \ref{eq:equivIso}}
\end{align*}

And since $\simeq$ 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(\prod_{a \tp A} \isProp (P\ a)\right) \to \prod_{x\;y \tp \sum_{a \tp A} P\ a} (x \equiv y) \simeq (\fst\ x \equiv \fst\ y)
\end{align}
%
The lemma states that for pairs whose second component are mere propositions
equiality 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}
\prod_{a \tp A} \left( P\ a \simeq Q\ a \right) \to \sum_{a \tp A} P\ a \simeq \sum_{a \tp A} Q\ a
\end{align}
%
Which says that if two type-families are equivalent at all points, then pairs
with identitical first components and these families as second components will
also be equivalent. For our purposes $P \defeq \isEquiv\ A\ B$ and $Q \defeq
\mathit{Isomorphism}$. So we must finally prove:
%
\begin{align}
  \label{eq:equivIso}
\prod_{f \tp A \to B} \left( \isEquiv\ A\ B\ f \simeq \mathit{Isomorphism}\ f \right)
\end{align}

First, lets proove \ref{eq:equivPropSig}: Let $propP \tp \prod_{a \tp A} \isProp (P\ a)$ and $x\;y \tp \sum_{a \tp A} P\ a$ be given. Because
of $\mathit{fromIsomorphism}$ it suffices to give an isomorphism between
$x \equiv y$ and $\fst\ x \equiv \fst\ y$:
%
\begin{align*}
  f & \defeq \congruence\ \fst \tp x \equiv y \to \fst\ x \equiv \fst\ y \\
  g & \defeq \mathit{lemSig}\ \mathit{propP}\ x\ y \tp \fst\ x \equiv \fst\ y \to x \equiv y
\end{align*}
%
\TODO{Is it confusing that I use point-free style here?}
Here $\mathit{lemSig}$ is a lemma that says that if the second component of a
pair is a proposition, it suffices to give a path between it's first components
to construct an equality of the two pairs:
%
\begin{align*}
\mathit{lemSig} \tp \left( \prod_{x \tp A} \isProp\ (B\ x) \right) \to
\prod_{u\; v \tp \sum_{a \tp A} B\ a}
  \left( \fst\ u \equiv \fst\ v \right) \to u \equiv v
\end{align*}
%
The proof that these are indeed inverses has been omitted. \TODO{Do I really
  want to ommit it?}\QED

Now to prove \ref{eq:equivSig}: Let $e \tp \prod_{a \tp A} \left( P\ a \simeq
Q\ a \right)$ be given. To prove the equivalence, it suffices to give an
isomorphism between $\sum_{a \tp A} P\ a$ and $\sum_{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 \to B$ be given. For the maps we
choose:
%
\begin{align*}
\mathit{toIso}
  & \tp \isEquiv\ f             \to \mathit{Isomorphism}\ f \\
\mathit{fromIso}
  & \tp \mathit{Isomorphism}\ f \to \isEquiv\ f
\end{align*}
%
As mentioned in section \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*}
  \mathit{fromIso} \comp \mathit{toIso} \equiv \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*}
  \mathit{toIso} \comp \mathit{fromIso} \equiv \identity_{\mathit{Isomorphism}\ f}
\end{align*}
%
We will show that $\mathit{Isomorphism}\ f$ is also a mere proposition. To this
end, let $X\;Y \tp \mathit{Isomorphism}\ f$ be given. Name the maps $x\;y \tp B
\to A$ respectively. Now, the proof that $X$ and $Y$ are the same is a pair of
paths: $p \tp x \equiv y$ and $\Path\ (\lambda\; i \mto
\mathit{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$. $p$ is inhabited by:
%
\begin{align*}
  x
  & \equiv x \comp \identity \\
  & \equiv x \comp (f \comp y)
  && \text{$y$ is an inverse to $f$} \\
  & \equiv (x \comp f) \comp y \\
  & \equiv \identity \comp y
  && \text{$x$ is an inverse to $f$} \\
  & \equiv 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*}
\prod_{g : B \to A} \isProp\ (\mathit{AreInverses}\ f\ g)
\end{align*}
%
But $\mathit{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{Product}
In the following I'll demonstrate a technique for using categories to prove
properties. The goal in this section is to show that products are propositions:
%
$$
\prod_{\bC \tp \Category} \prod_{A\;B \tp \Object} \isProp\ (\mathit{Product}\ \bC\ A\ B)
$$
%
Where $\mathit{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 preservehomotopy level,
then we know that products also are propositions. But before we get to that,
let's recall the definition of products.

\subsection{Products}
Given a category $\bC$ and two objects $A$ and $B$ in $\bC$ we define the
product of $A$ and $B$ to be an object $A \x B$ in $\bC$ and two arrows $\pi_1
\tp A \x B \to A$ and $\pi_2 \tp A \x B \to 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}
%% \prod_{X \tp Object} \prod_{f \tp \Arrow\ X\ A} \prod_{g \tp \Arrow\ X\ B}\\
%% \uexists_{f \x g \tp \Arrow\ X\ (A \x B)}
\pi_1 \lll \pi \equiv f \x \pi_2 \lll \pi \equiv g
%% ump : ∀ {X : Object} (f : ℂ [ X , A ]) (g : ℂ [ X , B ])
%%           → ∃![ f×g ] (ℂ [ fst ∘ f×g ] ≡ f P.× ℂ [ snd ∘ f×g ] ≡ g)
\end{align}
%
$\pi$ is called the product (arrow) of $f$ and $g$.

\subsection{Pair category}

\newcommand\pairA{\mathcal{A}}
\newcommand\pairB{\mathcal{B}}
Given a base category $\bC$ and two objects in this category $\pairA$ and
$\pairB$ we can construct the ``pair category'': \TODO{This is a working title,
  it's nice to have a name for this thing to refer back to}

The type 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 \equiv a_0 \x
b_1 \lll f \equiv 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)
  & \equiv
  (c_0 \lll f) \lll g
  && \text{Associativity} \\
  & \equiv
  b_0 \lll g
  && \text{$f$ satisfies \ref{eq:pairArrowLaw}} \\
  & \equiv
  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})
\equiv
(\overline{h} \lll \overline{g}) \lll \overline{f}
\end{align}
%
Herer $\lll$ refers to the `embellished' composition abd $\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:
%
\begin{align}
\label{eq:productAssocUnderlying}
h \lll (g \lll f)
\equiv
(h \lll g) \lll f
\end{align}
%
Which is provable by and that the witness to \ref{eq:pairArrowLaw} for the
left-hand-side and the right-hand-side are the same. The type of this goal is
quite involved, and I will not write it out in full, 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 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}
%
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}
\prod_{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.
%% %
%% $$
%% \prod_{(f, f_0, f_1)\; (g,g_0,g_1) \tp \Arrow\ X\ Y} f \equiv g \to (f, f_0, f_1) \equiv (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
%
$$
\prod_{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_\mathca{B})$
and $\mathcal{Y} = Y, y_\mathcal{A}, y_\mathcal{B}$ I will show:
%
\begin{align}
(\mathcal{X} \equiv \mathcal{Y}) \cong (\mathcal{X} \approxeq \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 \equiv 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 \cong 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} \defeq \var{isoToId}\ \var{iso} \tp X \equiv 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}:
\TODO{Super complicated}

\emph{Proposition} \ref{eq:univ-2} is isomorphic to \ref{eq:univ-3}:
For this I will two corrolaries of \ref{eq:coeCod}:
%
\begin{align}
\label{domain-twist}
\end{align}

\section{Monads}

%% \subsubsection{Functors}
%% Defines the notion of a functor - also split up into data and laws.

%% Propositionality for being a functor.

%% Composition of functors and the identity functor.

%% \subsubsection{Products}
%% Definition of what it means for an object to be a product in a given category.

%% Definition of what it means for a category to have all products.

%% \WIP{} Prove propositionality for being a product and having products.

%% \subsubsection{Exponentials}
%% Definition of what it means to be an exponential object.

%% Definition of what it means for a category to have all exponential objects.

%% \subsubsection{Cartesian closed categories}
%% Definition of what it means for a category to be cartesian closed; namely that
%% it has all products and all exponentials.

%% \subsubsection{Natural transformations}
%% Definition of transformations\footnote{Maybe this is a name I made up for a
%%   family of morphisms} and the naturality condition for these.

%% Proof that naturality is a mere proposition and the accompanying equality
%% principle. Proof that natural transformations are homotopic sets.

%% The identity natural transformation.

%% \subsubsection{Yoneda embedding}

%% The yoneda embedding is typically presented in terms of the category of
%% categories (cf. Awodey) \emph however this is not stricly needed - all we need
%% is what would be the exponential object in that category - this happens to be
%% functors and so this is how we define the yoneda embedding.

%% \subsubsection{Monads}

%% Defines an equivalence between these two formulations of a monad:

%% \subsubsubsection{Monoidal monads}

%% Defines the standard monoidal representation of a monad:

%% An endofunctor with two natural transformations (called ``pure'' and ``join'')
%% and some laws about these natural transformations.

%% Propositionality proofs and equality principle is provided.

%% \subsubsubsection{Kleisli monads}

%% A presentation of monads perhaps more familiar to a functional programer:

%% A map on objects and two maps on morphisms (called ``pure'' and ``bind'') and
%% some laws about these maps.

%% Propositionality proofs and equality principle is provided.

%% \subsubsubsection{Voevodsky's construction}

%% Provides construction 2.3 as presented in an unpublished paper by Vladimir
%% Voevodsky. This construction is similiar to the equivalence provided for the two
%% preceding formulations
%% \footnote{ TODO: I would like to include in the thesis some motivation for why
%%   this construction is particularly interesting.}

%% \subsubsection{Functors}
%% The category of functors and natural transformations. An immediate corrolary is
%% the set of presheaf categories.

%% \WIP{} I have not shown that the category of functors is univalent.

%% \subsubsection{Relations}
%% The category of relations. \WIP{} I have not shown that this category is
%% univalent. Not sure I intend to do so either.

%% \subsubsection{Free category}
%% The free category of a category. \WIP{} I have not shown that this category is
%% univalent.

%% \subsection{Current Challenges}
%% Besides the items marked \WIP{} above I still feel a bit unsure about what to
%% include in my report. Most of my work so far has been specifically about
%% developing this library. Some ideas:
%% %
%% \begin{itemize}
%% \item
%%   Modularity properties
%% \item
%%   Compare with setoid-approach to solve similiar problems.
%% \item
%%   How to structure an implementation to best deal with types that have no
%%   structure (propositions) and those that do (sets and everything above)
%% \end{itemize}
%% %
%% \subsection{Ideas for future developments}
%% \subsubsection{Higher categories}
%% I only have a notion of (1-)categories. Perhaps it would be nice to also
%% formalize higher categories.

%% \subsubsection{Hierarchy of concepts related to monads}
%% In Haskell the type-class Monad sits in a hierarchy atop the notion of a functor
%% and applicative functors. There's probably a similiar notion in the
%% category-theoretic approach to developing this.

%% As I have already defined monads from these two perspectives, it would be
%% interesting to take this idea even further and actually show how monads are
%% related to applicative functors and functors. I'm not entirely sure how this
%% would look in Agda though.

%% \subsubsection{Use formulation on the standard library}
%% I also thought it would be interesting to use this library to show certain
%% properties about functors, applicative functors and monads used in the Agda
%% Standard library. So I went ahead and tried to show that agda's standard
%% library's notion of a functor (along with suitable laws) is equivalent to my
%% formulation (in the category of homotopic sets). I ran into two problems here,
%% however; the first one is that the standard library's notion of a functor is
%% indexed by the object map:
%% %
%% $$
%% \Functor \tp (\Type \to \Type) \to \Type
%% $$
%% %
%% Where $\Functor\ F$ has the member:
%% %
%% $$
%% \fmap \tp (A \to B) \to F A \to F B
%% $$
%% %
%% Whereas the object map in my definition is existentially quantified:
%% %
%% $$
%% \Functor \tp \Type
%% $$
%% %
%% And $\Functor$ has these members:
%% \begin{align*}
%% F     & \tp \Type \to \Type \\
%% \fmap & \tp (A \to B) \to F A \to F B\}
%% \end{align*}
%% %