fredefox
/
cat
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Old unstaged changes 

I hope these are mostly non dangerous.  Looks like it's mainly some reformatting.
This commit is contained in:
Frederik Hanghøj Iversen 2018-07-17 16:51:16 +02:00
parent 6f275247dd
commit 188bba6c8d
6 changed files with 390 additions and 377 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
doc/abstract.tex
View File

@ -3,22 +3,21 @@ The usual notion of propositional equality in intensional type-theory
is restrictive. For instance it does not admit functional
extensionality nor univalence. This poses a severe limitation on both
what is \emph{provable} and the \emph{re-usability} of proofs. Recent
developments have however resulted in cubical type theory which
permits a constructive proof of these two important notions. The
programming language Agda has been extended with capabilities for
working in such a cubical setting. This thesis will explore the
usefulness of this extension in the context of category theory.
developments have, however, resulted in cubical type theory, which
permits a constructive proof of univalence. The programming language
Agda has been extended with capabilities for working in such a cubical
setting. This thesis will explore the usefulness of this extension in
the context of category theory.
The thesis will motivate the need for univalence and explain why
propositional equality in cubical Agda is more expressive than in
standard Agda. Alternative approaches to Cubical Agda will be
presented and their pros and cons will be explained. As an example of
the application of univalence two formulations of monads will be
the application of univalence, two formulations of monads will be
presented: Namely monads in the monoidal form and monads in the
Kleisli form and under the univalent interpretation it will be shown
how these are equal.
Kleisli form. Using univalence, it will be shown how these are equal.
Finally the thesis will explain the challenges that a developer will
face when working with cubical Agda and give some techniques to
overcome these difficulties. It will also try to suggest how further
work can help alleviate some of these challenges.
overcome these difficulties. It will suggest how further work can
help alleviate some of these challenges.

20
doc/conclusion.tex
View File

@ -12,27 +12,27 @@ thing Agda enjoys Uniqueness of Identity Proofs (UIP) though a flag
exists to turn this off. This feature is not present in Cubical Agda.
Rather than having unique identity proofs cubical Agda gives rise to a
hierarchy of types with increasing \nomen{homotopical
structure}{homotopy levels}. It turns out to be useful to built the
structure}{homotopy levels}. It turns out to be useful to build the
formalization with this hierarchy in mind as it can simplify proofs
considerably. Another issue one must overcome in Cubical Agda is when
a type has a field whose type depends on a previous field. In this
case paths between such types will be heterogeneous paths. In
practice it turns out to be considerably more difficult to work with
heterogeneous paths than with homogeneous paths. The thesis
heterogeneous paths than with homogeneous paths. This thesis
demonstrated the application of some techniques to overcome these
difficulties, such as based path induction.
This thesis formalizes some of the core concepts from category theory
including; categories, functors, products, exponentials, Cartesian
including: categories, functors, products, exponentials, Cartesian
closed categories, natural transformations, the yoneda embedding,
monads and more. Category theory is an interesting case study for the
application of cubical Agda for two reasons in particular: Because
category theory is the study of abstract algebra of functions, meaning
that functional extensionality is particularly relevant. Another
reason is that in category theory it is commonplace to identify
isomorphic structures. Univalence allows for making this notion
precise. This thesis also demonstrated another technique that is
common in category theory; namely to define categories to prove
application of cubical Agda for two reasons in particular. One reason
is because category theory is the study of abstract algebra of
functions, meaning that functional extensionality is particularly
relevant. Another reason is that in category theory it is commonplace
to identify isomorphic structures. Univalence allows for making this
notion precise. This thesis also demonstrated another technique that
is common in category theory; namely to define categories to prove
properties of other structures. Specifically a category was defined
to demonstrate that any two product objects in a category are
isomorphic. Furthermore the thesis showed two formulations of monads

65
doc/cubical.tex
View File

@ -7,7 +7,7 @@ $n$ simply by expanding the definition of $+$.
On the other hand, propositional equality is something defined within
the language itself. Propositional equality cannot be derived
automatically. The normal definition of judgmental equality is an
automatically. The normal definition of propositional equality is an
inductive data type. Cubical Agda discards this type in favor of some
new primitives.
@ -73,7 +73,7 @@ $$
p \tp \prod_{i \tp \I} P\ i
$$
%
Which must satisfy being judgmentally equal to $a_0$ at the
This function must satisfy being judgmentally equal to $a_0$ at the
left endpoint and equal to $a_1$ at the other end. I.e.:
%
\begin{align*}
@ -93,8 +93,8 @@ I will generally prefer to use the notation $a \equiv b$ when talking
about non-dependent paths and use the notation $\Path\ (\lambda\; i
\to P\ i)\ a\ b$ when the path space is of particular interest.
With this definition we can also recover reflexivity. That is, for any $A \tp
\MCU$ and $a \tp A$:
With this definition we can recover reflexivity. That is, for any $A
\tp \MCU$ and $a \tp A$:
%
\begin{equation}
\begin{aligned}
@ -105,7 +105,7 @@ With this definition we can also recover reflexivity. That is, for any $A \tp
%
Here the path space is $P \defeq \lambda\; i \to A$ and it satsifies
$P\ i = A$ definitionally. So to inhabit it, is to give a path $\I \to
A$ which is judgmentally $a$ at either endpoint. This is satisfied by
A$ that is judgmentally $a$ at either endpoint. This is satisfied by
the constant path; i.e.\ the path that is constantly $a$ at any index
$i \tp \I$.
@ -120,14 +120,15 @@ Functional extensionality is the proposition that given a type $A \tp
\end{equation}
%
%% p = λ\; i a → p a i
So given $η \tp \prod_{a \tp A} f\ a \equiv g\ a$ we must give a path $f \equiv
g$. That is a function $\I \to \prod_{a \tp A} B\ a$. So let $i \tp \I$ be given.
We must now give an expression $\phi \tp \prod_{a \tp A} B\ a$ satisfying
$\phi\ 0 \equiv f\ a$ and $\phi\ 1 \equiv g\ a$. This neccesitates that the
expression must be a lambda-abstraction, so let $a \tp A$ be given. Now we can
apply $a$ to $η$ and get the path $η\ a \tp f\ a \equiv g\ a$. And this exactly
satisfies the conditions for $\phi$. In conclustion \ref{eq:funExt} is inhabited
by the term:
So given $η \tp \prod_{a \tp A} f\ a \equiv g\ a$ we must give a path
$f \equiv g$. That is a function $\I \to \prod_{a \tp A} B\ a$. So let
$i \tp \I$ be given. We must now give an expression $\phi \tp
\prod_{a \tp A} B\ a$ satisfying $\phi\ 0 \equiv f\ a$ and $\phi\ 1
\equiv g\ a$. This neccesitates that the expression must be a lambda
abstraction, so let $a \tp A$ be given. We can now apply $a$ to $η$
and get the path $η\ a \tp f\ a \equiv g\ a$. This exactly
satisfies the conditions for $\phi$. In conclusion \ref{eq:funExt} is
inhabited by the term:
%
\begin{equation*}
\funExt\ η \defeq λ\; i\ a → η\ a\ i
@ -149,10 +150,10 @@ In ITT all equality proofs are identical (in a closed context). This
means that, in some sense, any two inhabitants of $a \equiv b$ are
``equally good''. They do not have any interesting structure. This is
referred to as Uniqueness of Identity Proofs (UIP). Unfortunately it
is not possible to have a type theory with both univalence and UIP. In
stead in cubical Agda we have a hierarchy of types with an increasing
amount of homotopic structure. At the bottom of this hierarchy is the
set of contractible types:
is not possible to have a type theory with both univalence and UIP.
Instead in cubical Agda we have a hierarchy of types with an
increasing amount of homotopic structure. At the bottom of this
hierarchy is the set of contractible types:
%
\begin{equation}
\begin{aligned}
@ -214,8 +215,8 @@ proving e.g.\ $\isProp\ \bN$ directly is not so straightforward (see
\cite[\S3.1.4]{hott-2013}). Hedberg's theorem states that any type
with decidable equality is a set. There will be examples of sets later
in this report. At this point it should be noted that the term ``set''
is somewhat conflated; there is the notion of sets from set-theory, in
Agda types are denoted \texttt{Set}. I will use it consistently to
is somewhat conflated; there is the notion of sets from set theory.
In Agda types are denoted \texttt{Set}. I will use it consistently to
refer to a type $A$ as a set exactly if $\isSet\ A$ is a proposition.
As the reader may have guessed the next step in the hierarchy is the type:
@ -227,11 +228,12 @@ As the reader may have guessed the next step in the hierarchy is the type:
\end{aligned}
\end{equation}
%
And so it continues. In fact we can generalize this family of types by indexing
them with a natural number. For historical reasons, though, the bottom of the
hierarchy, the contractible types, is said to be a \nomen{-2-type}{homotopy
levels}, propositions are \nomen{-1-types}{homotopy levels}, (homotopical)
sets are \nomen{0-types}{homotopy levels} and so on\ldots
So it continues. In fact we can generalize this family of types by
indexing them with a natural number. For historical reasons, though,
the bottom of the hierarchy, the contractible types, is said to be a
\nomen{-2-type}{homotopy levels}, propositions are
\nomen{-1-types}{homotopy levels}, (homotopical) sets are
\nomen{0-types}{homotopy levels} and so on\ldots
Just as with paths, homotopical sets are not at the center of focus for this
thesis. But I mention here some properties that will be relevant for this
@ -250,7 +252,7 @@ Specifically the results come from the Agda library \texttt{cubical}
(\cite{cubical-demo}). I have used a handful of results from this
library as well as contributed a few lemmas myself%
\footnote{The module \texttt{Cat.Prelude} lists the upstream
dependencies. As well my contribution to \texttt{cubical} can be
dependencies. My contribution to \texttt{cubical} can as well be
found in the git logs which are available at
\hrefsymb{https://github.com/Saizan/cubical-demo}{\texttt{https://github.com/Saizan/cubical-demo}}.
}.
@ -279,12 +281,11 @@ $$
D \tp \prod_{b \tp A} \prod_{p \tp a ≡ b} \MCU
$$
%
And an inhabitant of $D$ at $\refl$:
and an inhabitant of $D$ at $\refl$:
%
$$
d \tp D\ a\ \refl
$$
%
We have the function:
%
\begin{equation}
@ -343,7 +344,7 @@ over the family:
T\ d'\ r' & \defeq \trans\ p\ (\trans\ q\ r') ≡ \trans\ (\trans\ p\ q)\ r'
\end{align*}
%
So the base case is proven with $t$ which is defined as:
The base case is proven with $t$ which is defined as:
%
\begin{align*}
\trans\ p\ (\trans\ q\ \refl) & ≡
@ -376,7 +377,7 @@ $$
$$
%
Note that $d_0$ and $d_1$, though points of the same family, have
different types. This is quite a mouthful. So let me try to show how
different types. This is quite a mouthful, so let me try to show how
this is a very general and useful result.
Often when proving equalities between elements of some dependent types
@ -388,7 +389,7 @@ $$
T \defeq \sum_{a \tp A} D\ a
$$
%
For some proposition $D \tp A \to \MCU$. That is we have $\var{propD}
for some proposition $D \tp A \to \MCU$. That is we have $\var{propD}
\tp \prod_{a \tp A} \isProp\ (D\ a)$. If we want to prove $t_0 \equiv
t_1$ for two elements $t_0, t_1 \tp T$ then this will be a pair of
paths:
@ -408,7 +409,7 @@ $$
$$
%
\subsection{Functions over propositions}
\label{sec:propPi}
\label{sec:propPi}%
$\prod$-types preserve propositionality when the co-domain is always a
proposition.
%
@ -419,7 +420,7 @@ $$
\label{sec:propSig}
%
$\sum$-types preserve propositionality whenever its first component is
a proposition, and its second component is a proposition for all
a proposition and its second component is a proposition for all
points of the left type.
%
$$

24
doc/discussion.tex
View File

@ -10,8 +10,8 @@ mere propositions.
\subsection{Computational properties}
The new contribution of cubical Agda is that it has a constructive
proof of functional extensionality\index{functional extensionality}
and univalence\index{univalence}. This means that in particular that
the type checker can reduce terms defined with these theorems. So one
and univalence\index{univalence}. This means in particular that the
type checker can reduce terms defined with these theorems. One
interesting result of this development is how much this influenced the
development. In particular having a functional extensionality that
``computes'' should simplify some proofs.
@ -33,24 +33,24 @@ module:
%
I will not reproduce it in full here as the type is quite involved. In
stead I have put this in a source listing in \ref{app:abstract-funext}.
The method used to find in what places the computational behaviour of
these proofs are needed has the caveat of only working for places that
directly or transitively uses these two proofs. Fortunately though
the code is structured in such a way that this is the case. So in
conclusion the way I have structured these proofs means that the
computational behaviour of functional extensionality and univalence
has not been so relevant.
stead I have put this in a source listing in
\ref{app:abstract-funext}. The method used to find in what places the
computational behaviour of these proofs are needed has the caveat of
only working for places that directly or transitively uses these two
proofs. Fortunately though the code is structured in such a way that
this is the case. In conclusion the way I have structured these proofs
means that the computational behaviour of functional extensionality
and univalence has not been so relevant.
Barring this the computational behaviour of paths can still be useful.
E.g.\ if a programmer wants to reuse functions that operate on a
monoidal monads to work with a monad in the Kleisli form that the
programmer has specified. To make this idea concrete, say we are
given some function $f \tp \Kleisli \to T$ having a path between $p
given some function $f \tp \Kleisli \to T$, having a path between $p
\tp \Monoidal \equiv \Kleisli$ induces a map $\coe\ p \tp \Monoidal
\to \Kleisli$. We can compose $f$ with this map to get $f \comp
\coe\ p \tp \Monoidal \to T$. Of course, since that map was
constructed with an isomorphism these maps already exist and could be
constructed with an isomorphism, these maps already exist and could be
used directly. So this is arguably only interesting when one also
wants to prove properties of applying such functions.

429
doc/implementation.tex
View File

@ -57,11 +57,11 @@ The concepts formalized in this development are:
\end{center}
\end{samepage}%
%
As well as a range of various results about these. E.g.\ I have shown
that the category of sets has products. In the following I aim to
demonstrate some of the techniques employed in this formalization and
in the interest of brevity I will not detail all the things I have
formalized. In stead I have selected parts of this formalization that
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},
@ -82,15 +82,15 @@ 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
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
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
@ -98,17 +98,18 @@ found in typical mathematical expositions on the topic. We shall
impose one further requirement on what it means to be a category,
namely that the type of arrows form a set.
Such categories are called \nomen{1-categories}{1-category}. It is
possible to relax this requirement. This would lead to the notion of
higher categories (\cite[p. 307]{hott-2013}). For the purpose of this
thesis however, this report will restrict itself to
1-categories\index{1-category}. Generalizing this work to higher
Categories 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 it to be univalent. Before we can define this, I must introduce two more
definitions: If we let $p$ be a witness to the identity law, which formally is:
\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}
@ -118,20 +119,20 @@ definitions: If we let $p$ be a witness to the identity law, which formally is:
\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:
\identity, p) \tp A ≊ A$ for any object $A$. Here $≊$ denotes
isomorphism on objects (whereas $\cong$ denotes isomorphism on types).
This will be elaborated further on in sections \S\ref{sec:equiv} and
\S\ref{sec:univalence}. Moreover due to substitution for paths we can
construct an isomorphism from \emph{any} path:
%
\begin{equation}
\idToIso \tp A ≡ B → A ≊ B
\end{equation}
%
The univalence criterion for categories states that this map must be an
equivalence. The requirement is similar to univalence for types, but where
isomorphism on objects play the role of equivalence on types. Formally:
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}
@ -146,10 +147,10 @@ Note that \ref{eq:cat-univ} is \emph{not} the same as:
(A ≡ B) ≃ (A ≊ B)
\end{equation}
%
However the two are logically equivalent: One can construct the latter
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}.
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:
@ -161,7 +162,7 @@ data:
\lll & \tp \Arrow\ B\ C → \Arrow\ A\ B → \Arrow\ A\ C
\end{align}
%
And laws:
and laws:
%
\begin{align}
%% \tag{associativity}
@ -182,16 +183,16 @@ And laws:
\isEquiv\ (A ≡ B)\ (A ≊ B)\ \idToIso
\end{align}
%
The function $\lll$ denotes arrow composition (right-to-left), and
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 arrow ($f$, $g$,
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
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:
@ -217,10 +218,10 @@ $$
\isProp\ \left( \left( \id \comp f ≡ f \right) \x \left( f \comp \id ≡ f \right) \right)
$$
%
Then we eliminate the (non-dependent) sigma-type by applying $\propSig$ giving
us the two obligations $\isProp\ (\id \comp f ≡ f)$ and $\isProp\ (f \comp
\id ≡ f)$ which follows from the type of arrows being a
set.
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
@ -246,7 +247,7 @@ Where the definition of $\IsPreCategory$ is the triple:
%
Each corresponding to the first three laws for categories. Note that
since $\IsPreCategory$ is not formulated with a chain of sigma-types
we will not have any combinators available to help us here. In stead
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:
@ -255,13 +256,13 @@ $$
∏_{a, b \tp \IsPreCategory} a ≡ b
$$
%
So to prove the proposition let $a, b \tp \IsPreCategory$ be given. To
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 →
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
$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:
%
@ -271,14 +272,15 @@ $$
a.\isIdentity ≡ b.\isIdentity
$$
%
So to give the continuous function $\I → \IsPreCategory$, which is our goal, we
introduce $i \tp \I$ and proceed by constructing an element of $\IsPreCategory$
by using the fact that all the projections are propositions to generate paths
between all projections. Once we have such a path e.g.\ $p \tp a.\isIdentity
≡ b.\isIdentity$ we can eliminate it with $i$ and thus obtain $p\ i \tp
(p\ i).\isIdentity$. This element satisfies exactly that it corresponds to the
corresponding projections at either endpoint. Thus the element we construct at
$i$ becomes the triple:
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}
@ -296,7 +298,7 @@ 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
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
@ -307,9 +309,9 @@ 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
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. So to
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:
%
@ -332,13 +334,13 @@ result that univalence is a proposition to a heterogeneous path. To
this end we can use $\lemPropF$, which was introduced in
\S\ref{sec:lemPropF}.
In this case $A = \var{IsIdentity}\ \identity$ and $B =
\Univalent$. We have shown that being a category is a proposition, a
result that holds for any choice of identity proof 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:
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
@ -350,10 +352,10 @@ $$
\var{lemPropF}\ \var{propUnivalent}\ (\var{cong}\ p.\var{isIdentity})
$$
%
And this finishes the proof that being-a-category is a mere proposition
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
When we have a proper category, we can make precise the notion of
``identifying isomorphic types''. That is, we can construct the
function:
%
@ -395,8 +397,8 @@ $\Isomorphism\ f$. This also gives rise to the following type:
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:
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 \\
@ -465,7 +467,7 @@ As mentioned the univalence criterion for some category $\bC$ says that for all
$$
\isEquiv\ (A ≡ B)\ (A ≊ B)\ \idToIso
$$
And I mentioned that this was logically equivalent to
This is logically equivalent to
%
$$
(A ≡ B) ≃ (A ≊ B)
@ -484,10 +486,10 @@ 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
-- in stead they can be thought of as a generalization hereof. The
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 maps with respect to univalence.
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.
@ -554,7 +556,7 @@ are trying to prove but talks about paths rather than isomorphisms:
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 ≡
\Object$. Let $\widetilde{B} \tp \Object$ and $\widetilde{p} \tp A ≡
\widetilde{B}$ be given. The family that we perform induction over
will be:
%
@ -590,28 +592,30 @@ term:
\pathJ\ D\ d\ B\ p
\end{equation}
%
And this finishes the proof of \ref{eq:coeDomIso} and thus \ref{eq:coeDom}.
This finishes the proof of \ref{eq:coeDomIso} and thus
\ref{eq:coeDom}.
%
\section{Categories}
\subsection{Opposite category}
\label{op-cat}
The first category I will present is a pure construction on categories. Given
some category we can construct its dual, called the opposite category. Starting
with a simple example allows us to focus on how we work with equivalences and
univalence in a very simple category where the structure of the category is
rather simple.
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.
$\bC^{\var{Op}}$. It has the same objects, but the type of arrows are
flipped, that is to say an arrow from $A$ to $B$ in the opposite
category corresponds to an arrow from $B$ to $A$ in the underlying
category. The identity arrow is the same as the one in the underlying
category (they have the same type). Function composition will be
reverse function composition from the underlying category.
I will refer to things in terms of the underlying category, unless they have an
over-bar. So e.g.\ $\idToIso$ is a function in the underlying category and the
corresponding thing is denoted $\wideoverbar{\idToIso}$ in the opposite
category.
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.
%
@ -628,9 +632,9 @@ $$
%
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$.
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
@ -649,9 +653,9 @@ opposite direction. I name these maps $\shufflef \tp (A ≊ B) → (A
\wideoverbar{≊} B)$ and $\shufflef^{-1} \tp (A \wideoverbar{≊} B) → (A
≊ B)$ respectively.
As the inverse of $\wideoverbar{\idToIso}$ I will pick $\wideoverbar{\isoToId}
≜ \isoToId \comp \shufflef$. The proof that they are inverses go as
follows:
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} & =
@ -673,13 +677,15 @@ follows:
%
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.
The lemma used in step 2 of this proof states that
$\wideoverbar{idToIso} ≡ \inv{\shufflef} \comp \idToIso$. This is a
rather straightforward proof since being-an-inverse-of is a
proposition, so it suffices to show that their first components are
equal but this holds judgmentally.
This finished the proof that the opposite category is in fact a category. Now,
to prove that opposite-of is an involution we must show:
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
@ -713,10 +719,10 @@ Univalence does not follow immediately from univalence for types:
%
$$(A ≡ B) ≃ (A ≃ B)$$
%
Because here $A, B \tp \Type$ whereas the objects in this category have the type
$\Set$ so we cannot form the type $\var{hA} ≃ \var{hB}$ for objects
$\var{hA}\;\var{hB} \tp \Set$. In stead I show that this category
satisfies:
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})
@ -734,7 +740,7 @@ of equivalences:
& ≃ ((A, s_A) ≊ (B, s_B)) && \text{\ref{eq:equivSig} and \ref{eq:equivIso}}
\end{align*}
And since $≃$ is an equivalence relation we can chain these equivalences
Since $≃$ is an equivalence relation we can chain these equivalences
together. Step one will be proven with the lemma:
%
\begin{align}
@ -753,19 +759,20 @@ for types. Step three will be proven with the following lemma:
∏_{a \tp A} \left( P\ a ≃ Q\ a \right) → ∑_{a \tp A} P\ a ≃ ∑_{a \tp A} Q\ a
\end{align}
%
Which says that if two type-families are equivalent at all points, then pairs
with identical first components and these families as second components will
also be equivalent. For our purposes $P ≜ \isEquiv\ A\ B$ and $Q ≜
\Isomorphism$. So we must finally prove:
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}
First, lets prove \ref{eq:equivPropSig}: Let $propP \tp ∏_{a \tp A} \isProp\ (P\ a)$ and $x\;y \tp ∑_{a \tp A} P\ a$ be given. Because
of $\var{fromIsomorphism}$ it suffices to give an isomorphism between
$x ≡ y$ and $\fst\ x ≡ \fst\ y$:
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*}
@ -778,7 +785,7 @@ $x ≡ y$ and $\fst\ x ≡ \fst\ y$:
\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
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*}
@ -811,7 +818,7 @@ choose:
\end{align*}
%
As mentioned in section \S\ref{sec:equiv}. These maps are not in general inverses
of each other. In stead, we will use the fact that $A$ and $B$ are sets. The first thing we must prove is:
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}
@ -843,20 +850,22 @@ $\mathcal{X}$ and $\mathcal{Y}$ denotes the witnesses that $x$
& = 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:
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.
but $\var{AreInverses}\ f\ g$ is a pair of equations on arrows, so we
use $\propSig$ and the fact that both $A$ and $B$ are sets to close
this proof.
%% \subsection{Category of categories}
%% Note that this category does in fact not exist. In stead I provide
%% 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.
@ -878,13 +887,13 @@ $$
∏_{\bC \tp \Category} ∏_{A\;B \tp \Object} \isProp\ (\var{Product}\ \bC\ A\ B)
$$
%
Where $\var{Product}\ \bC\ A\ B$ denotes the type of products of
objects $A$ and $B$ in the category $\bC$. I do this by constructing a
category whose terminal objects are equivalent to products in $\bC$,
and since terminal objects are propositional in a proper category and
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.
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
@ -908,9 +917,9 @@ 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
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)
category, $X$ and two arrows (also from the underlying category)
$\Arrow\ X\ \pairA$ and $\Arrow\ X\ \pairB$.
\newcommand\pairf{\ensuremath{f}}
@ -974,30 +983,32 @@ The proof obligations consists of two things. The first one is:
(h \lll g) \lll f
\end{align}
%
And the other proof obligation is that the witness to \ref{eq:pairArrowLaw} for
the left-hand-side and the right-hand-side are the same.
The 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 the present
exposition it will suffices 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:
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}
%
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:
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}
@ -1005,33 +1016,33 @@ stead we generalize \ref{eq:productPath} to:
\end{align}
%
For all objects $X , x_{\pairA} , x_{\pairB}$ and $Y , y_{\pairA} ,
y_{\pairB}$, but this follows from the fact that $∏$ and $∑$ preserve
homotopical structure. 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.
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} simply with
And thus we have proven \ref{eq:productAssoc} using
\ref{eq:productAssocUnderlying}.
Now we must prove that arrows form a set:
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 two
obligations:
Since pairs preserve homotopical structure this reduces to the
following two obligations: The first one is:
%
$$
\isSet\ (\bC.\Arrow\ X\ Y)
$$
%
Which holds. And
which holds. The other one is:
%
$$
∏_{f \tp \Arrow\ X\ Y}
@ -1040,15 +1051,16 @@ $$
\right)
$$
%
This we get from \ref{eq:productEqPrinc} and the fact that homotopical structure
is cumulative.
We get this from \ref{eq:productEqPrinc} and the fact that homotopical
structure is cumulative.
This finishes the proof that this is a valid pre-category.
That concludes the proof that this is a valid pre-category.
\subsubsection{Univalence}
To prove that this is a proper category it must be shown that it is univalent.
That is, for any two objects $\mathcal{X} = (X, x_{\mathcal{A}} , x_{\mathcal{B}})$
and $\mathcal{Y} = Y, y_{\mathcal{A}}, y_{\mathcal{B}}$ I will show:
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})
@ -1075,8 +1087,8 @@ The next types will be the triple:
%% \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:
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}
@ -1087,7 +1099,7 @@ isomorphism, and create a path from this:
\end{split}
\end{align}
%
Where $\widetilde{p} ≜ \isoToId\ \var{iso} \tp X ≡ Y$.
where $\widetilde{p} ≜ \isoToId\ \var{iso} \tp X ≡ Y$.
Finally we have the type:
%
@ -1096,10 +1108,10 @@ Finally we have the type:
(X , x_{\mathcal{A}} , x_{\mathcal{B}}) ≊ (Y , y_{\mathcal{A}} , y_{\mathcal{B}})
\end{align}
%
So 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 module:
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}
@ -1116,13 +1128,13 @@ This proof of this has been omitted but can be found in the module:
\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
\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}
@ -1157,16 +1169,17 @@ shall be:
f \tp \Arrow\ X\ Y
\end{align}
%
To show that this choice fits the bill I must now verify that it satisfies
\ref{eq:pairArrowLaw}, which in this case becomes:
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.
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}.
@ -1222,7 +1235,7 @@ This is achieved with the following lemma:
\Path\ (λ \; i → q\ i)\ a\ b
\end{align}
%
Which is used without proof. See the implementation for the details.
which is used without proof. See the implementation for the details.
\ref{eq:product-paths} is then proven with the propositions:
%
@ -1249,7 +1262,7 @@ 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{Products are propositions}
\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
@ -1264,14 +1277,19 @@ that terminal objects in the span category are equivalent to products:
\var{Terminal} ≃ \var{Product}\ ℂ\ \mathcal{A}\ \mathcal{B}
\end{align}
%
And as always we do this by constructing an isomorphism:
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:
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}
@ -1282,23 +1300,23 @@ indeed a product. That is, for an object $Y$ and two arrows $y_𝒜 \tp
%% \end{split}
\end{align}
%
Since $X, x_𝒜, x_ℬ$ is a terminal object there is a \emph{unique}
arrow from this object to any other object, so in particular also $Y,
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. So now it remains that for
any other object there is a unique arrow from that object into $X,
x_𝒜, x_ℬ$. Let $Y, y_𝒜, y_ℬ$ be another object. As the arrow
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_ℬ}$. So we have picked as our center
of contraction $y_𝒜 \x y_ℬ , \phi_{y_𝒜 \x y_ℬ}$ we must now show that
it is contractible. So let $f \tp \Arrow\ X\ Y$ and $\phi_f$ be given
(here $\phi_f$ is the proof that $f$ satisfies \ref{eq:pairCondRev}).
The proof will be a pair of proofs:
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
@ -1330,11 +1348,10 @@ $$
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:
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)
@ -1354,7 +1371,7 @@ following data:
\fmap & \tp ℂ.\Arrow\ A\ B → 𝔻.\Arrow\ (\omapF\ A)\ (\omapF\ B)
\end{align*}
%
And the following laws:
and the following laws:
\begin{align*}
\fmap\ ℂ.\identity & ≡ 𝔻.identity \\
\fmap\ (g \clll f) & ≡ \fmap\ g \dlll \fmap\ f
@ -1462,7 +1479,7 @@ The objects $X$ and $Y$ are implicitly universally quantified. With this data w
f \fish g & ≜ f \rrr (\bind\ g)
\end{align*}
%
It is interesting to note here that this formulation does mention
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.
%
@ -1502,7 +1519,7 @@ In the monoidal formulation we can define $\bind$:
\bind\ f ≜ \join \lll \fmap\ f
\end{align}
%
And likewise in the Kleisli formulation we can define $\join$:
and likewise in the Kleisli formulation we can define $\join$:
%
\begin{align}
\join ≜ \bind\ \identity
@ -1596,7 +1613,7 @@ the monoidal formulation we pick:
We must now not only show the monad laws given for the monoidal
formulation (\monoidallaws), we must also verify that $\EndoR$ is a
functor and that $\pure$ and $\join$ are natural transformations. I
will ommit this here. In stead we shall see how these two mappings
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}
@ -1614,7 +1631,7 @@ other. To recap, these maps are:
→ (\EndoR, \pure, \bind\ \identity)
\end{align*}
%
Where $\EndoR ≜ (\omapR, \bind\ (\pure \lll f))$. The proof that
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:
@ -1639,9 +1656,9 @@ 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. So it suffices
to equate the data-parts of the \ref{eq:monad-forwards}. Such a proof
is a triple equating the three projections of
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:

210
doc/introduction.tex
View File

@ -1,17 +1,17 @@
\chapter{Introduction}
This thesis is a case-study in the application of cubical Agda in the
context of category theory. At the center of this is the notion of
\nomenindex{equality}. In type-theory there are two pervasive notions
of equality: \nomenindex{judgmental equality} and
This thesis is a case study in the application of cubical Agda to the
formalization of category theory. At the center of this is the notion
of \nomenindex{equality}. There are two pervasive notions of equality
in type theory: \nomenindex{judgmental equality} and
\nomenindex{propositional equality}. Judgmental equality is a property
of the type system. Judgmental equality on the other hand is usually
defined \emph{within} the system. When introducing definitions this
report will use the symbol $\defeq$. Judgmental equalities will be
denoted with $=$ and for propositional equalities the notation
$\equiv$ is used.
of the type system. Propositional equality on the other hand is
usually defined \emph{within} the system. When introducing
definitions this report will use the symbol $\defeq$. Judgmental
equalities will be denoted with $=$ and for propositional equalities
the notation $\equiv$ is used.
The rules of judgmental equality are related with $β$- and
$η$-reduction which gives a notion of computation in a given type
$η$-reduction, which gives a notion of computation in a given type
theory.
%
There are some properties that one usually want judgmental equality to
@ -19,20 +19,21 @@ satisfy. It must be \nomenindex{sound}, enjoy \nomenindex{canonicity}
and be a \nomenindex{congruence relation}. Soundness means that things
judged to be equal are equal with respects to the \nomenindex{model}
of the theory or the \emph{meta theory}. It must be a congruence
relation because otherwise the relation certainly does not adhere to
our notion of equality. One would be able to conclude things like: $x
\equiv y \rightarrow f\ x \nequiv f\ y$. Canonicity means that any
well typed term evaluates to a \emph{canonical} form. For example for
a closed term $e \tp \bN$ it will be the case that $e$ reduces to $n$
applications of $\mathit{suc}$ to $0$ for some $n$; $e =
\mathit{suc}^n\ 0$. Without canonicity terms in the language can get
``stuck'' meaning that they do not reduce to a canonical form.
relation, because otherwise the relation certainly does not adhere to
our notion of equality. E.g.\ One would be able to conclude things
like: $x \equiv y \rightarrow f\ x \nequiv f\ y$. Canonicity means
that any well typed term evaluates to a \emph{canonical} form. For
example, for a closed term $e \tp \bN$, it will be the case that $e$
reduces to $n$ applications of $\mathit{suc}$ to $0$ for some $n$;
i.e.\ $e = \mathit{suc}^n\ 0$. Without canonicity terms in the
language can get ``stuck'', meaning that they do not reduce to a
canonical form.
To work as a programming languages it is necessary for judgmental
equality to be \nomenindex{decidable}. Being decidable simply means
that that an algorithm exists to decide whether two terms are equal.
For any practical implementation the decidability must also be
effectively computable.
For a system to work as a programming languages it is necessary for
judgmental equality to be \nomenindex{decidable}. Being decidable
simply means that that an algorithm exists to decide whether two terms
are equal. For any practical implementation, the decidability must
also be effectively computable.
For propositional equality the decidability requirement is relaxed. It
is not in general possible to decide the correctness of logical
@ -47,28 +48,27 @@ inhabitant. In extensional type theory the principle of reflection
$$a ≡ b → a = b$$
%
is enough to make type checking undecidable. This report focuses on
Agda which at a glance can be thought of as a version of intensional
Agda, which at a glance can be thought of as a version of intensional
type theory. Pattern-matching in regular Agda lets one prove
\nomenindex{Uniqueness of Identity Proofs} (UIP). UIP states that any
two identity proofs are propositionally identical.
The usual notion of propositional equality in ITT is quite
restrictive. In the next section a few motivating examples will
highlight this. There exist techniques to circumvent these problems,
as we shall see. This thesis will explore an extension to Agda that
redefines the notion of propositional equality and as such is an
alternative to these other techniques. The extension is called cubical
Agda. Cubical Agda drops UIP as this does not permit
\nomenindex{functional extensionality} and
\nomenindex{univalence}. What makes this extension particularly
interesting is that it gives a \emph{constructive} interpretation of
univalence. What all this means will be elaborated in the following
sections.
restrictive. In the next section a few motivating examples will be
presented that highlight. There exist techniques to circumvent these
problems, as we shall see. This thesis will explore an extension to
Agda that redefines the notion of propositional equality and as such
is an alternative to these other techniques. The extension is called
cubical Agda. Cubical Agda drops UIP, as it does not permit
\nomenindex{functional extensionality} nor \nomenindex{univalence}.
What makes cubical Agda particularly interesting is that it gives a
\emph{constructive} interpretation of univalence. What all this means
will be elaborated in the following sections.
%
\section{Motivating examples}
%
In the following two sections I present two examples that illustrate
some limitations inherent in ITT and -- by extension -- Agda.
some limitations inherent in ITT and, by extension, Agda.
%
\subsection{Functional extensionality}
\label{sec:functional-extensionality}%
@ -80,9 +80,9 @@ Consider the functions:
\end{align*}%
%
The term $n + 0$ is \nomenindex{definitionally} equal to $n$, which we
write as $n + 0 = n$. This is also called \nomenindex{judgmental
equality}. We call it definitional equality because the
\emph{equality} arises from the \emph{definition} of $+$ which is:
write as $n + 0 = n$. This is also called \nomenindex{judgmental
equality}. We call it definitional equality because the
\emph{equality} arises from the \emph{definition} of $+$, which is:
%
\begin{align*}
+ & \tp \bN \to \bN \to \bN \\
@ -90,12 +90,12 @@ write as $n + 0 = n$. This is also called \nomenindex{judgmental
n + (\suc{m}) & \defeq \suc{(n + m)}
\end{align*}
%
Note that $0 + n$ is \emph{not} definitionally equal to $n$. This is
because $0 + n$ is in normal form. I.e.\ there is no rule for $+$
whose left hand side matches this expression. We do however have that
Note that $0 + n$ is \emph{not} definitionally equal to $n$. This is
because $0 + n$ is in normal form. I.e.\ there is no rule for $+$
whose left hand side matches this expression. We do, however, have that
they are \nomen{propositionally}{propositional equality} equal, which
we write as $n \equiv n + 0$. Propositional equality means that there
is a proof that exhibits this relation. We can do induction over $n$
we write as $n \equiv n + 0$. Propositional equality means that there
is a proof that exhibits this relation. We can do induction over $n$
to prove this:
%
\begin{align}
@ -107,39 +107,38 @@ to prove this:
\end{split}
\end{align}
%
This show that zero is a right neutral element hence the name $\var{zrn}$.
Since equality is a transitive relation we have that $\forall n \to
\var{zeroLeft}\ n \equiv \var{zeroRight}\ n$. Unfortunately we don't
have $\var{zeroLeft} \equiv \var{zeroRight}$. There is no way to
construct a proof asserting the obvious equivalence of
$\var{zeroLeft}$ and $\var{zeroRight}$. Actually showing this is
outside the scope of this text. Essentially it would involve giving a
This show that zero is a right neutral element (hence the name
$\var{zrn}$). Since equality is a transitive relation we have that
$\forall n \to \var{zeroLeft}\ n \equiv \var{zeroRight}\ n$.
Unfortunately we don't have $\var{zeroLeft} \equiv \var{zeroRight}$.
There is no way to construct a proof asserting the obvious equivalence
of $\var{zeroLeft}$ and $\var{zeroRight}$. Actually showing this is
outside the scope of this text. It would essentially involve giving a
model for our type theory that validates all our axioms but where
$\var{zeroLeft} \equiv \var{zeroRight}$ is not true. We cannot show
$\var{zeroLeft} \equiv \var{zeroRight}$ is not true. We cannot show
that they are equal even though we can prove them equal for all
points. For functions this is exactly the notion of equality that we
are interested in: Functions are considered equal when they are equal
for all inputs. This is called \nomenindex{pointwise equality}, where
the \emph{points} of a function refer to its arguments.
points. This is exactly the notion of equality that we are interested
in for functions: Functions are considered equal when they are equal
for all inputs. This is called \nomenindex{pointwise equality} where
\emph{points} of a function refer to its arguments.
%
\subsection{Equality of isomorphic types}
%
Let $\top$ denote the unit type -- a type with a single constructor.
In the propositions as types interpretation of type theory $\top$ is
the proposition that is always true. The type $A \x \top$ and $A$ has
an element for each $a \tp A$. So in a sense they have the same shape
(Greek;
\nomenindex{isomorphic}). The second element of the pair does not
add any ``interesting information''. It can be useful to identify such
types. In fact, it is quite commonplace in mathematics. Say we look at
a set $\{x \mid \phi\ x \land \psi\ x\}$ and somehow conclude that
$\psi\ x \equiv \top$ for all $x$. A mathematician would immediately
conclude $\{x \mid \phi\ x \land \psi\ x\} \equiv \{x \mid \phi\ x\}$
without thinking twice. Unfortunately such an identification can not
be performed in ITT.
the proposition that is always true. The type $A \x \top$ and $A$ has
an element for each $a \tp A$. So in a sense they have the same shape
(Greek; \nomenindex{isomorphic}). The second element of the pair does
not add any ``interesting information''. It can be useful to identify
such types. In fact it is quite commonplace in mathematics. Say we
look at a set $\{x \mid \phi\ x \land \psi\ x\}$ and somehow conclude
that $\psi\ x \equiv \top$ for all $x$. A mathematician would
immediately conclude $\{x \mid \phi\ x \land \psi\ x\} \equiv \{x \mid
\phi\ x\}$ without thinking twice. Unfortunately such an
identification can not be performed in ITT.
More specifically what we are interested in is a way of identifying
\nomenindex{equivalent} types. I will return to the definition of
\nomenindex{equivalent} types. I will return to the definition of
equivalence later in section \S\ref{sec:equiv}, but for now it is
sufficient to think of an equivalence as a one-to-one correspondence.
We write $A \simeq B$ to assert that $A$ and $B$ are equivalent types.
@ -155,23 +154,23 @@ and vice versa.
\section{Formalizing Category Theory}
%
The above examples serve to illustrate a limitation of ITT. One case
The above examples serve to illustrate a limitation of ITT. One case
where these limitations are particularly prohibitive is in the study
of Category Theory. At a glance category theory can be described as
of Category Theory. At a glance category theory can be described as
``the mathematical study of (abstract) algebras of functions''
(\cite{awodey-2006}). By that token functional extensionality is
particularly useful for formulating Category Theory. In Category
theory it is also commonplace to identify isomorphic structures and
univalence gives us a way to make this notion precise. In fact we can
(\cite{awodey-2006}). By that token functional extensionality is
particularly useful for formulating Category Theory. In Category
theory it is also commonplace to identify isomorphic structures.
Univalence gives us a way to make this notion precise. In fact we can
formulate this requirement within our formulation of categories by
requiring the \emph{categories} themselves to be univalent as we shall
see in \S\ref{sec:univalence}.
see in section \S\ref{sec:univalence}.
\section{Context}
\label{sec:context}
%
The idea of formalizing Category Theory in proof assistants is not new. There
are a multitude of these available online. Notably:
The idea of formalizing Category Theory in proof assistants is not new. There
are a multitude of these available online. Notably:
%
\begin{itemize}
\item
@ -186,20 +185,21 @@ are a multitude of these available online. Notably:
\url{https://github.com/HoTT/HoTT/tree/master/theories/Categories}
\item
A formalization in \emph{CubicalTT} -- a language designed for
cubical type theory. Formalizes many different things, but only a
cubical type theory. Formalizes many different things, but only a
few concepts from category theory:
\url{https://github.com/mortberg/cubicaltt}
\end{itemize}
%
The contribution of this thesis is to explore how working in a cubical setting
will make it possible to prove more things and to reuse proofs and to try and
compare some aspects of this formalization with the existing ones.
The contribution of this thesis is to explore how working in a cubical
setting will make it possible to prove more things, to reuse proofs
and to compare some aspects of this formalization with the existing
ones.
There are alternative approaches to working in a cubical setting where
one can still have univalence and functional extensionality. One
option is to postulate these as axioms. This approach, however, has
other shortcomings, e.g. you lose \nomenindex{canonicity}
(\cite[p. 3]{huber-2016}).
one can still have univalence and functional extensionality. One
option is to postulate these as axioms. This approach, however, has
other shortcomings, e.g.\ you lose \nomenindex{canonicity}
(\cite[p.\ 3]{huber-2016}).
Another approach is to use the \emph{setoid interpretation} of type
theory (\cite{hofmann-1995,huber-2016}). With this approach one works
@ -207,13 +207,13 @@ with \nomenindex{extensional sets} $(X, \sim)$. That is a type $X \tp
\MCU$ and an equivalence relation $\sim\ \tp X \to X \to \MCU$ on that
type. Under the setoid interpretation the equivalence relation serve
as a sort of ``local'' propositional equality. Since the developer
gets to pick this relation it is not a~priori a congruence
relation. So this must be verified manually by the developer.
Furthermore, functions between different setoids must be shown to be
setoid homomorphism, that is; they preserve the relation.
gets to pick this relation, it is not a~priori a congruence
relation. It must be manually verified by the developer. Furthermore,
functions between different setoids must be shown to be setoid
homomorphism, that is; they preserve the relation.
This approach has other drawbacks; it does not satisfy all
propositional equalities of type theory a\~priori. That is, the
This approach has other drawbacks: It does not satisfy all
propositional equalities of type theory a~priori. That is, the
developer must manually show that e.g.\ the relation is a congruence.
Equational proofs $a \sim_{X} b$ are in some sense `local' to the
extensional set $(X , \sim)$. To e.g.\ prove that $x ∼ y → f\ x ∼
@ -223,23 +223,19 @@ makes it very cumbersome to work with in practice (\cite[p.
4]{huber-2016}).
\section{Conventions}
In the remainder of this paper I will use the term \nomenindex{Type}
to describe -- well -- types. Thereby departing from the notation in
Agda where the keyword \texttt{Set} refers to types. \nomenindex{Set}
on the other hand shall refer to the homotopical notion of a set. I
will also leave all universe levels implicit. This of course does not
mean that a statement such as $\MCU \tp \MCU$ means that we have
type-in-type but rather that the arguments to the universes are
implicit.
In the remainder of this thesis I will use the term \nomenindex{Type}
to describe -- well -- types; thereby departing from the notation in
Agda where the keyword \texttt{Set} refers to types.
\nomenindex{Set}, on the other hand, shall refer to the homotopical
notion of a set. I will also leave all universe levels implicit. This
of course does not mean that a statement such as $\MCU \tp \MCU$ means
that we have type-in-type but rather that the arguments to the
universes are implicit.
And I use the term
\nomenindex{arrow} to refer to morphisms in a category,
whereas the terms
\nomenindex{morphism},
\nomenindex{map} or
\nomenindex{function}
shall be reserved for talking about type theoretic functions; i.e.
functions in Agda.
I use the term \nomenindex{arrow} to refer to morphisms in a category,
whereas the terms \nomenindex{morphism}, \nomenindex{map} or
\nomenindex{function} shall be reserved for talking about type
theoretic functions; i.e.\ functions in Agda.
As already noted $\defeq$ will be used for introducing definitions $=$
will be used to for judgmental equality and $\equiv$ will be used for