Fix spelling mistakes

This commit is contained in:
Frederik Hanghøj Iversen 2018-05-08 00:25:34 +02:00
parent 0db4e97511
commit 7faf0961c5
9 changed files with 243 additions and 95 deletions

37
doc/appendix.tex Normal file
View file

@ -0,0 +1,37 @@
\lstset{basicstyle=\footnotesize\ttfamily,breaklines=true,breakpages=true}
\def\fileps
{ ../src/Cat.agda
, ../src/Cat/Categories/Cat.agda
, ../src/Cat/Categories/Cube.agda
, ../src/Cat/Categories/CwF.agda
, ../src/Cat/Categories/Fam.agda
, ../src/Cat/Categories/Free.agda
, ../src/Cat/Categories/Fun.agda
, ../src/Cat/Categories/Rel.agda
, ../src/Cat/Categories/Sets.agda
, ../src/Cat/Category.agda
, ../src/Cat/Category/CartesianClosed.agda
, ../src/Cat/Category/Exponential.agda
, ../src/Cat/Category/Functor.agda
, ../src/Cat/Category/Monad.agda
, ../src/Cat/Category/Monad/Kleisli.agda
, ../src/Cat/Category/Monad/Monoidal.agda
, ../src/Cat/Category/Monad/Voevodsky.agda
, ../src/Cat/Category/Monoid.agda
, ../src/Cat/Category/NaturalTransformation.agda
, ../src/Cat/Category/Product.agda
, ../src/Cat/Category/Yoneda.agda
, ../src/Cat/Equivalence.agda
, ../src/Cat/Prelude.agda
}
\foreach \filep in \fileps {
\chapter{\filep}
%% \begin{figure}[htpb]
\lstinputlisting{\filep}
%% \caption{Source code for \texttt{\filep}}
%% \label{fig:\filep}
%% \end{figure}
}
%% \lstset{framextopmargin=50pt}
%% \lstinputlisting{../../src/Cat.agda}

View file

@ -40,6 +40,7 @@
\newcommand*{\subtitle}[1]{\gdef\@subtitle{#1}} \newcommand*{\subtitle}[1]{\gdef\@subtitle{#1}}
\newgeometry{top=3cm, bottom=3cm,left=2.25 cm, right=2.25cm} \newgeometry{top=3cm, bottom=3cm,left=2.25 cm, right=2.25cm}
\begingroup \begingroup
\thispagestyle{empty}
\usepackage{noto} \usepackage{noto}
\fontseries{sb} \fontseries{sb}
%% \fontfamily{noto}\selectfont %% \fontfamily{noto}\selectfont

3
doc/conclusion.tex Normal file
View file

@ -0,0 +1,3 @@
\chapter{Conclusion}
\TODO{\ldots}

View file

@ -56,7 +56,7 @@ the real numbers from $0$ to $1$. $P$ is a family of types over the index set
$I$. I will sometimes refer to $P$ as the ``path-space'' of some path $p \tp $I$. I will sometimes refer to $P$ as the ``path-space'' of some path $p \tp
\Path\ P\ a\ b$. By this token $P\ 0$ then corresponds to the type at the \Path\ P\ a\ b$. By this token $P\ 0$ then corresponds to the type at the
left-endpoint and $P\ 1$ as the type at the right-endpoint. The type is called left-endpoint and $P\ 1$ as the type at the right-endpoint. The type is called
$\Path$ because it is connected with paths in homotopy thoery. The intuition $\Path$ because it is connected with paths in homotopy theory. The intuition
behind this is that $\Path$ describes paths in $\MCU$ -- i.e. between types. For behind this is that $\Path$ describes paths in $\MCU$ -- i.e. between types. For
a path $p$ for the point $p\ i$ the index $i$ describes how far along the path a path $p$ for the point $p\ i$ the index $i$ describes how far along the path
one has moved. An inhabitant of $\Path\ P\ a_0\ a_1$ is a (dependent-) one has moved. An inhabitant of $\Path\ P\ a_0\ a_1$ is a (dependent-)
@ -155,7 +155,7 @@ 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 \texttt{Set}. I will use it consistently to refer to a type $A$ as a set exactly
if $\isSet\ A$ is inhabited. if $\isSet\ A$ is inhabited.
The next step in the hierarchy is, as you might've guessed, the type: The next step in the hierarchy is, as the reader might've guessed, the type:
% %
\begin{equation} \begin{equation}
\begin{alignat}{2} \begin{alignat}{2}
@ -166,7 +166,7 @@ The next step in the hierarchy is, as you might've guessed, the type:
% %
And so it continues. In fact we can generalize this family of types by indexing 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 them with a natural number. For historical reasons, though, the bottom of the
hierarchy, the contractible tyes, is said to be a \nomen{-2-type}, propositions hierarchy, the contractible types, is said to be a \nomen{-2-type}, propositions
are \nomen{-1-types}, (homotopical) sets are \nomen{0-types} and so on\ldots are \nomen{-1-types}, (homotopical) sets are \nomen{0-types} and so on\ldots
Just as with paths, homotopical sets are not at the center of focus for this Just as with paths, homotopical sets are not at the center of focus for this
@ -181,12 +181,12 @@ Proposition: For any homotopic level $n$ this is a mere proposition.
% %
\section{A few lemmas} \section{A few lemmas}
Rather than getting into the nitty-gritty details of Agda I venture to take a Rather than getting into the nitty-gritty details of Agda I venture to take a
more ``combinators-based'' approach. That is, I will use theorems about paths more ``combinator-based'' approach. That is, I will use theorems about paths
already that have already been formalized. Specifically the results come from already that have already been formalized. Specifically the results come from
the Agda library \texttt{cubical} (\TODO{Cite}). I have used a handful of the Agda library \texttt{cubical} (\TODO{Cite}). 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 found in the git logs \TODO{Cite}.} 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 found in the git logs \TODO{Cite}.}
These theorems are all purely related to homotopy theory and cubical agda and as These theorems are all purely related to homotopy theory and cubical Agda and as
such not specific to the formalization of Category Theory. I will present a few such not specific to the formalization of Category Theory. I will present a few
of these theorems here, as they will be used later in chapter of these theorems here, as they will be used later in chapter
\ref{ch:implementation} throughout. \ref{ch:implementation} throughout.
@ -195,7 +195,7 @@ of these theorems here, as they will be used later in chapter
\label{sec:pathJ} \label{sec:pathJ}
The induction principle for paths intuitively gives us a way to reason about a The induction principle for paths intuitively gives us a way to reason about a
type-family indexed by a path by only considering if said path is $\refl$ (the type-family indexed by a path by only considering if said path is $\refl$ (the
``base-case''). For \emph{based path induction}, that equaility is \emph{based} ``base-case''). For \emph{based path induction}, that equality is \emph{based}
at some element $a \tp A$. at some element $a \tp A$.
Let a type $A \tp \MCU$ and an element of the type $a \tp A$ be given. $a$ is said to be the base of the induction. Given a family of types: Let a type $A \tp \MCU$ and an element of the type $a \tp A$ be given. $a$ is said to be the base of the induction. Given a family of types:

74
doc/discussion.tex Normal file
View file

@ -0,0 +1,74 @@
\chapter{Perspectives}
\section{Discussion}
In the previous chapter the practical aspects of proving things in Cubical Agda
were highlighted. I also demonstrated the usefulness of separating ``laws'' from
``data''. One of the reasons for this is that dependencies within types can lead
to very complicated goals. One technique for alleviating this was to prove that
certain types are mere propositions.
\subsection{Computational properties}
Another aspect (\TODO{That I actually didn't highlight very well in the previous
chapter}) is the computational nature of paths. Say we have formalized this
common result about monads:
\TODO{Some equation\ldots}
By transporting this to the Kleisli formulation we get a result that we can use
to compute with. This is particularly useful because the Kleisli formulation
will be more familiar to programmers e.g. those coming from a background in
Haskell. Whereas the theory usually talks about monoidal monads.
\TODO{Mention that with postulates we cannot do this}
\subsection{Reusability of proofs}
The previous example also illustrate how univalence unifies two otherwise
disparate areas: The category-theoretic study of monads; and monads as in
functional programming. Univalence thus allows one to reuse proofs. You could
say that univalence gives the developer two proofs for the price of one.
The introduction (section \ref{sec:context}) mentioned an often
employed-technique for enabling extensional equalities is to use the
setoid-interpretation. Nowhere in this formalization has this been necessary,
$\Path$ has been used globally in the project as propositional equality. One
interesting place where this becomes apparent is in interfacing with the Agda
standard library. Multiple definitions in the Agda standard library have been
designed with the setoid-interpretation in mind. E.g. the notion of ``unique
existential'' is indexed by a relation that should play the role of
propositional equality. Likewise for equivalence relations, they are indexed,
not only by the actual equivalence relation, but also by another relation that
serve as propositional equality.
%% Unfortunately we cannot use the definition of equivalences found in the
%% standard library to do equational reasoning directly. The reason for this is
%% that the equivalence relation defined there must be a homogenous relation,
%% but paths are heterogeneous relations.
In the formalization at present a significant amount of energy has been put
towards proving things that would not have been needed in classical Agda. The
proofs that some given type is a proposition were provided as a strategy to
simplify some otherwise very complicated proofs (e.g.
\ref{eq:proof-prop-IsPreCategory} and \label{eq:productPath}). Often these
proofs would not be this complicated. If the J-rule holds definitionally the
proof-assistant can help simplify these goals considerably. The lack of the
J-rule has a significant impact on the complexity of these kinds of proofs.
\TODO{Universe levels.}
\section{Future work}
\subsection{Agda \texttt{Prop}}
Jesper Cockx' work extending the universe-level-laws for Agda and the
\texttt{Prop}-type.
\subsection{Compiling Cubical Agda}
\label{sec:compiling-cubical-agda}
Compilation of program written in Cubical Agda is currently not supported. One
issue here is that the backends does not provide an implementation for the
cubical primitives (such as the path-type). This means that even though the
path-type gives us a computational interpretation of functional extensionality,
univalence, transport, etc., we do not have a way of actually using this to
compile our programs that use these primitives. It would be interesting to see
practical applications of this. The path between monads that this library
exposes could provide one particularly interesting case-study.
\subsection{Higher inductive types}
This library has not explored the usefulness of higher inductive types in the
context of Category Theory.

View file

@ -2,37 +2,52 @@
\label{ch:implementation} \label{ch:implementation}
This implementation formalizes the following concepts: This implementation formalizes the following concepts:
% %
\begin{itemize} \begin{enumerate}[i.]
\item Core categorical concepts \item Categories
\subitem Categories \item Functors
\subitem Functors \item Products
\subitem Products \item Exponentials
\subitem Exponentials \item Cartesian closed categories
\subitem Cartesian closed categories \item Natural transformations
\subitem Natural transformations \item Yoneda embedding
\subitem Yoneda embedding \item Monads
\subitem Monads \item Categories
\subsubitem Monoidal monads \begin{enumerate}[i.]
\subsubitem Kleisli monads \item Opposite category
\subsubitem Voevodsky's construction \item Category of sets
\item Category of \ldots \item ``Pair category''
\subitem Homotopy sets \end{enumerate}
\subitem Categories -- only data-part \end{enumerate}
\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) Furthermore the following items have been partly formalized:
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 \begin{enumerate}[i.]
that we can provide a proof that the laws are mere propositions. As an example a \item The (higher) category of categories.
category is defined to have two members: `raw` which is a collection of the data \item Category of relations
and `isCategory` which asserts some laws about that data. \item Category of functors and natural transformations -- only as a precategory
\item Free category
\item Monoidal objects
\item Monoidal categories
\end{enumerate}
%
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 a parts
of this formalization that highlight some interesting proof techniques relevant
to doing proofs in Cubical Agda.
One such technique that is pervasive to this formalization is the idea of
distinguishing types with more or less homotopical structure. To do this I have
followed the following design-principle: I have split concepts up into things
that represent ``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 ``standard mathematical way'', This allows me to reason about things in a more ``standard mathematical way'',
where one can reason about two categories by simply focusing on the data. This 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 is achieved by creating a function embodying the ``equality principle'' for a
given type. given type.
\section{Categories} \section{Categories}
@ -45,7 +60,7 @@ 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. a category, namely that the type of arrows form a set.
Such categories are called \nomen{1-categories}. It's possible to relax this Such categories are called \nomen{1-categories}. It's possible to relax this
requirement. This would lead to the notion of higher categorier (\cite[p. requirement. This would lead to the notion of higher categories (\cite[p.
307]{hott-2013}). For the purpose of this project, however, this report will 307]{hott-2013}). For the purpose of this project, however, this report will
restrict itself to 1-categories. Making based on higher categories would be a restrict itself to 1-categories. Making based on higher categories would be a
very natural possible extension of this work. very natural possible extension of this work.
@ -63,7 +78,7 @@ definitions: If we let $p$ be a witness to the identity law, which formally is:
\end{equation} \end{equation}
% %
Then we can construct the identity isomorphism $\var{idIso} \tp \identity, Then we can construct the identity isomorphism $\var{idIso} \tp \identity,
\identity, p \tp A \approxeq A$ for any obejct $A$. Here $\approxeq$ denotes \identity, p \tp A \approxeq A$ for any object $A$. Here $\approxeq$ denotes
isomorphism on objects (whereas $\cong$ denotes isomorphism of types). This will isomorphism on objects (whereas $\cong$ denotes isomorphism of types). This will
be elaborated further on in sections \ref{sec:equiv} and \ref{sec:univalence}. be elaborated further on in sections \ref{sec:equiv} and \ref{sec:univalence}.
Moreover, due to substitution for paths we can construct an isomorphism from Moreover, due to substitution for paths we can construct an isomorphism from
@ -121,7 +136,7 @@ f \lll \identity ≡ f
\end{align} \end{align}
% %
$\lll$ denotes arrow composition (right-to-left), and reverse function $\lll$ denotes arrow composition (right-to-left), and reverse function
composition (left-to-right, diagramatic order) is denoted $\rrr$. The objects composition (left-to-right, diagrammatic order) is denoted $\rrr$. The objects
($A$, $B$ and $C$) and arrow ($f$, $g$, $h$) are implicitly universally ($A$, $B$ and $C$) and arrow ($f$, $g$, $h$) are implicitly universally
quantified. quantified.
@ -160,25 +175,32 @@ us the two obligations: $\isProp\ (\id \comp f \equiv f)$ and $\isProp\ (f \comp
set. set.
This example illustrates nicely how we can use these combinators to reason about This example illustrates nicely how we can use these combinators to reason about
`canonical' types like $\sum$ and $\prod$. Similiar combinators can be defined `canonical' types like $\sum$ and $\prod$. Similar combinators can be defined
at the other homotopic levels. These combinators are however not applicable in 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 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 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 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 that the type of pre-categories is also a proposition. Formally:
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:
% %
\begin{equation} \begin{equation}
\label{eq:propIsPreCategory} \label{eq:propIsPreCategory}
\isProp\ \IsPreCategory \isProp\ \IsPreCategory
\end{equation} \end{equation}
% %
%% \begin{proof} Where The definition of $\IsPreCategory$ is the triple:
% %
This is judgmentally the same as \begin{align*}
\var{isAssociative} & \tp \var{IsAssociative}\\
\var{isIdentity} & \tp \var{IsIdentity}\\
\var{arrowsAreSets} & \tp \var{ArrowsAreSets}
\end{align*}
%
Each corresponding to the first three laws for categories. Note that since
$\IsPreCategory$ is not formulated with a chain of sigma-types we wont have any
combinators available to help us here. In stead we'll have to use the path-type
directly.
\ref{eq:propIsPreCategory} is judgmentally the same as
% %
$$ $$
\prod_{a\ b \tp \IsPreCategory} a \equiv b \prod_{a\ b \tp \IsPreCategory} a \equiv b
@ -202,12 +224,13 @@ So to give the continuous function $I \to \IsPreCategory$, which is our goal, we
introduce $i \tp I$ and proceed by constructing an element of $\IsPreCategory$ 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 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 between all projections. Once we have such a path e.g. $p \tp a.\isIdentity
\equiv b.\isIdentity$ we can elimiate it with $i$ and thus obtain $p\ i \tp \equiv 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 (p\ i).\isIdentity$. This element satisfies exactly that it corresponds to the
corresponding projections at either endpoint. Thus the element we construct at corresponding projections at either endpoint. Thus the element we construct at
$i$ becomes the triple: $i$ becomes the triple:
% %
\begin{equation} \begin{equation}
\label{eq:proof-prop-IsPreCategory}
\begin{aligned} \begin{aligned}
& \var{propIsAssociative} && a.\var{isAssociative}\ & \var{propIsAssociative} && a.\var{isAssociative}\
&& b.\var{isAssociative} && i \\ && b.\var{isAssociative} && i \\
@ -224,7 +247,7 @@ 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 type would already not be possible, since we at least need extensionality (the
projections are all $\prod$-types). Assuming we had functional extensionality projections are all $\prod$-types). Assuming we had functional extensionality
available to us as an axiom, we would use functional extensionality (in 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 reverse?) to retrieve the equalities in $a$ and $b$, pattern-match on them to
see that they are both $\var{refl}$ and then close the proof with $\var{refl}$. see that they are both $\var{refl}$ and then close the proof with $\var{refl}$.
Of course this theorem is not so interesting in the setting of ITT since we know Of course this theorem is not so interesting in the setting of ITT since we know
a priori that equality proofs are unique. a priori that equality proofs are unique.
@ -234,7 +257,7 @@ 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 $\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 the univalence condition. Recall that the univalence condition is indexed by the
identity-proof. So to follow the same recipe as above, let $a\ b \tp identity-proof. So to follow the same recipe as above, let $a\ b \tp
\IsCategory$ be given, to show them equal, we now need to give two paths. One homogenous: \IsCategory$ be given, to show them equal, we now need to give two paths. One homogeneous:
% %
$$ $$
p \tp a.\isPreCategory \equiv b.\isPreCategory p \tp a.\isPreCategory \equiv b.\isPreCategory
@ -249,9 +272,9 @@ $$
Which depends on the choice of $p$. The first of these we can provide since, as Which depends on the choice of $p$. The first of these we can provide since, as
we have shown, $\IsPreCategory$ is a proposition. However, even though we have shown, $\IsPreCategory$ is a proposition. However, even though
$\Univalent$ is also a proposition, we cannot use this directly to show the $\Univalent$ is also a proposition, we cannot use this directly to show the
latter. This is becasue $\isProp$ talks about non-dependent paths. So we need to latter. This is because $\isProp$ talks about non-dependent paths. So we need to
'promote' the result that univalence is a proposition to a heterogeneous path. 'promote' the result that univalence is a proposition to a heterogeneous path.
To this end we can use $\lemPropF$, which wasintroduced in \ref{sec:lemPropF}. To this end we can use $\lemPropF$, which was introduced in \ref{sec:lemPropF}.
In this case $A = \var{IsIdentity}\ \identity$ and $B = \var{Univalent}$. We've In this case $A = \var{IsIdentity}\ \identity$ and $B = \var{Univalent}$. We've
shown that being a category is a proposition, a result that holds for any choice shown that being a category is a proposition, a result that holds for any choice
@ -267,7 +290,7 @@ And this finishes the proof that being-a-category is a mere proposition
(\ref{eq:propIsPreCategory}). (\ref{eq:propIsPreCategory}).
When we have a proper category we can make precise the notion of ``identifying 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 isomorphic types'' \TODO{cite Awodey here}. That is, we can construct the
function: function:
% %
$$ $$
@ -322,7 +345,7 @@ The maps $\var{fromIso}$ and $\var{toIso}$ naturally extend to these maps:
\end{align} \end{align}
% %
Having this interface gives us both: a way to think rather abstractly about how Having this interface gives us both: a way to think rather abstractly about how
to work with equivalences and a way to use ad-hoc definitions of equivalences. to work with equivalences and a way to use ad hoc definitions of equivalences.
The specific instantiation of $\isEquiv$ as defined in \cite{cubical-agda} is: The specific instantiation of $\isEquiv$ as defined in \cite{cubical-agda} is:
% %
$$ $$
@ -394,7 +417,7 @@ univalence of all pre-category since morphisms in a category are not regular
functions -- in stead they can be thought of as a generalization hereof. The univalence criterion therefore is simply a way of restricting arrows functions -- in stead they can be thought of as a generalization hereof. The univalence criterion therefore is simply a way of restricting arrows
to behave similarly to maps. to behave similarly to maps.
I will now mention a few helpful thoerems that follow from univalence that will I will now mention a few helpful theorems that follow from univalence that will
become useful later. become useful later.
Obviously univalence gives us an isomorphism between $A \equiv B$ and $A Obviously univalence gives us an isomorphism between $A \equiv B$ and $A
@ -427,7 +450,7 @@ then have the following two theorems:
\var{coe}\ p_{\var{cod}}\ f \equiv \iota \lll f \var{coe}\ p_{\var{cod}}\ f \equiv \iota \lll f
\end{align} \end{align}
% %
I will give the proof of the first theorem here, the second one is analagous. I will give the proof of the first theorem here, the second one is analogous.
% %
\begin{align*} \begin{align*}
\var{coe}\ p_{\var{dom}}\ f \var{coe}\ p_{\var{dom}}\ f
@ -467,11 +490,11 @@ The base-case therefore becomes:
& \equiv f \lll \inv{(\var{idToIso}\ \widetilde{\refl})} & \equiv f \lll \inv{(\var{idToIso}\ \widetilde{\refl})}
\end{align*} \end{align*}
% %
The first step follows because reflixivity is a neutral element for coercions. The first step follows because reflexivity is a neutral element for coercion.
The second step is the identity law in the category. The last step has to do The second step is the identity law in the category. The last step has to do
with the fact that $\var{idToIso}$ is constructed by substituting according to with the fact that $\var{idToIso}$ is constructed by substituting according to
the supplied path and since reflexivity is also the neutral element for the supplied path and since reflexivity is also the neutral element for
substuitutions we arrive at the desired expression. To close the substitutions we arrive at the desired expression. To close the
based-path-induction we must supply the value ``at the other''. In this case based-path-induction we must supply the value ``at the other''. In this case
this is simply $B \tp \Object$ and $p \tp A \equiv B$ which we have. this is simply $B \tp \Object$ and $p \tp A \equiv B$ which we have.
@ -552,7 +575,7 @@ follows:
&& \text{$\var{shuffle}$ is an isomorphism} \\ && \text{$\var{shuffle}$ is an isomorphism} \\
& \equiv & \equiv
\identity \identity
&& \text{$\isoToId$ is an ismorphism} && \text{$\isoToId$ is an isomorphism}
\end{align*} \end{align*}
% %
The other direction is analogous. The other direction is analogous.
@ -639,7 +662,7 @@ lemma:
\end{align} \end{align}
% %
Which says that if two type-families are equivalent at all points, then pairs 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 with identical first components and these families as second components will
also be equivalent. For our purposes $P \defeq \isEquiv\ A\ B$ and $Q \defeq also be equivalent. For our purposes $P \defeq \isEquiv\ A\ B$ and $Q \defeq
\var{Isomorphism}$. So we must finally prove: \var{Isomorphism}$. So we must finally prove:
% %
@ -648,7 +671,7 @@ also be equivalent. For our purposes $P \defeq \isEquiv\ A\ B$ and $Q \defeq
\prod_{f \tp A \to B} \left( \isEquiv\ A\ B\ f \simeq \var{Isomorphism}\ f \right) \prod_{f \tp A \to B} \left( \isEquiv\ A\ B\ f \simeq \var{Isomorphism}\ f \right)
\end{align} \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 First, lets prove \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 $\var{fromIsomorphism}$ it suffices to give an isomorphism between of $\var{fromIsomorphism}$ it suffices to give an isomorphism between
$x \equiv y$ and $\fst\ x \equiv \fst\ y$: $x \equiv y$ and $\fst\ x \equiv \fst\ y$:
% %
@ -674,7 +697,7 @@ the two pairs:
\end{align*} \end{align*}
% %
The proof that these are indeed inverses has been omitted. \TODO{Do I really The proof that these are indeed inverses has been omitted. \TODO{Do I really
want to ommit it?}\QED want to omit it?}\QED
Now to prove \ref{eq:equivSig}: Let $e \tp \prod_{a \tp A} \left( P\ a \simeq 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 Q\ a \right)$ be given. To prove the equivalence, it suffices to give an
@ -839,14 +862,13 @@ arrows form a set. For instance, to prove associativity we must prove that
(\overline{h} \lll \overline{g}) \lll \overline{f} (\overline{h} \lll \overline{g}) \lll \overline{f}
\end{align} \end{align}
% %
Herer $\lll$ refers to the `embellished' composition and $\overline{f}$, Here $\lll$ refers to the `embellished' composition and $\overline{f}$,
$\overline{g}$ and $\overline{h}$ are triples consisting of arrows from the $\overline{g}$ and $\overline{h}$ are triples consisting of arrows from the
underlying category ($f$, $g$ and $h$) and a pair of witnesses to underlying category ($f$, $g$ and $h$) and a pair of witnesses to
\ref{eq:pairArrowLaw}. \ref{eq:pairArrowLaw}.
%% Luckily those winesses are paths in the hom-set of the %% Luckily those winesses are paths in the hom-set of the
%% underlying category which is a set, so these are mere propositions. %% underlying category which is a set, so these are mere propositions.
The proof The proof obligations is consists of two things. The first one is:
obligations is:
% %
\begin{align} \begin{align}
\label{eq:productAssocUnderlying} \label{eq:productAssocUnderlying}
@ -855,15 +877,18 @@ h \lll (g \lll f)
(h \lll g) \lll f (h \lll g) \lll f
\end{align} \end{align}
% %
Which is provable by \TODO{What?} and that the witness to \ref{eq:pairArrowLaw} And the other proof obligation is that the witness to \ref{eq:pairArrowLaw} for
for the left-hand-side and the right-hand-side are the same. The type of this the left-hand-side and the right-hand-side are the same.
goal is quite involved, and I will not write it out in full, but at present it
suffices to show the type of the path-space. Note that the arrows in The proof of the first goal comes directly from the underlying category. The
\ref{eq:productAssoc} are arrows from $\mathcal{A} = (A , a_{\pairA} , a_{\pairB})$ type of the second goal is very complicated. I will not write it out in full
to $\mathcal{D} = (D , d_{\pairA} , d_{\pairB})$ where $a_{\pairA}$, $a_{\pairB}$, here, but it suffices to show the type of the path-space. Note that the arrows
$d_{\pairA}$ and $d_{\pairB}$ are arrows in the underlying category. Given that $p$ in \ref{eq:productAssoc} are arrows from $\mathcal{A} = (A , a_{\pairA} ,
is the chosen proof of \ref{eq:productAssocUnderlying} we then have that the a_{\pairB})$ to $\mathcal{D} = (D , d_{\pairA} , d_{\pairB})$ where
witness to \ref{eq:pairArrowLaw} vary over the type: $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} \begin{align}
\label{eq:productPath} \label{eq:productPath}
@ -979,7 +1004,7 @@ the implementation for the details).
\TODO{Super complicated} \TODO{Super complicated}
\emph{Proposition} \ref{eq:univ-2} is isomorphic to \ref{eq:univ-3}: For this I \emph{Proposition} \ref{eq:univ-2} is isomorphic to \ref{eq:univ-3}: For this I
will swho two corrolaries of \ref{eq:coeCod}: For an isomorphism $(\iota, 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 \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 \Arrow\ B\ X$ and a heterogeneous path between them, $q \tp \Path\ (\lambda i
\to p_{\var{dom}}\ i)\ f\ g$, where $p_{\var{dom}} \tp \Arrow\ A\ X \equiv \to p_{\var{dom}}\ i)\ f\ g$, where $p_{\var{dom}} \tp \Arrow\ A\ X \equiv
@ -995,7 +1020,7 @@ g & \equiv f \lll \inv{\iota}
% %
Proof: \TODO{\ldots} Proof: \TODO{\ldots}
Now we can prove the equiavalence in the following way: Given $(f, \inv{f}, Now we can prove the equivalence in the following way: Given $(f, \inv{f},
\var{inv}_f) \tp X \cong Y$ and two heterogeneous paths \var{inv}_f) \tp X \cong Y$ and two heterogeneous paths
% %
\begin{align*} \begin{align*}
@ -1025,7 +1050,7 @@ 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 is a path varying according to a path constructed from this isomorphism, this is
exactly what \ref{eq:domain-twist-0} gives us. exactly what \ref{eq:domain-twist-0} gives us.
% %
The other direction is quite analagous. We choose $\inv{f}$ as the morphism and 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}. prove that it satisfies \ref{eq:pairArrowLaw} with \ref{eq:domain-twist-1}.
We must now show that this choice of arrows indeed form an isomorphism. Our We must now show that this choice of arrows indeed form an isomorphism. Our
@ -1099,7 +1124,7 @@ The proof of the first one is:
We have now constructed the maps between \ref{eq:univ-0} and \ref{eq:univ-1}. It We have now constructed the maps between \ref{eq:univ-0} and \ref{eq:univ-1}. It
remains to show that they are inverses of each other. To cut a long story short, remains to show that they are inverses of each other. To cut a long story short,
the proof uses the fact that isomorphism-of is propositional and that arrows (in the proof uses the fact that isomorphism-of is propositional and that arrows (in
both categories) are sets. The reader is refered to the implementation for the both categories) are sets. The reader is referred to the implementation for the
gory details. gory details.
% %
\subsection{Propositionality of products} \subsection{Propositionality of products}
@ -1137,7 +1162,7 @@ conditions will be equal since $f$ is unique.
For the other direction we are now given a product $X, x_𝒜, x_$. Again this 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 will be the terminal object. So now it remains that for any other object there
is aunique arrow from that object into $X, x_𝒜, x_$. Let $Y, y_𝒜, y_$ be 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 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 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 name the witness to this $\phi_{y_𝒜 \x y_}$. So we have picked as our center of
@ -1184,12 +1209,14 @@ That in any category:
\end{align} \end{align}
% %
\section{Monads} \section{Monads}
In this section I show two formulations of monads and then show that they are In this section I present two formulations of monads. The two representations
the same. The two representations are referred to as the monoidal- and kleisli- are referred to as the monoidal- and Kleisli- representation respectively or
representation respectively. simply monoidal monads and Kleisli monads for short. We then show that the two
formulations are equivalent, which due to univalence gives us a path between the
two types.
We shall let a category $\bC$ be given. In the remainder all objects and arrows Let a category $\bC$ be given. In the remainder of this sections all objects and
will implicitly refer to objects and arrows in this category. arrows will implicitly refer to objects and arrows in this category.
% %
\subsection{Monoidal formulation} \subsection{Monoidal formulation}
The monoidal formulation of monads consists of the following data: The monoidal formulation of monads consists of the following data:
@ -1226,7 +1253,7 @@ they range over are universally quantified.
\subsection{Kleisli formulation} \subsection{Kleisli formulation}
% %
The kleisli-formulation consists of the following data: The Kleisli-formulation consists of the following data:
% %
\begin{align} \begin{align}
\label{eq:monad-kleisli-data} \label{eq:monad-kleisli-data}
@ -1262,18 +1289,18 @@ This data must satisfy:
% %
Here likewise the arrows $f \tp \Arrow\ X\ (\EndoR\ Y)$ and $g \tp Here likewise the arrows $f \tp \Arrow\ X\ (\EndoR\ Y)$ and $g \tp
\Arrow\ Y\ (\EndoR\ Z)$ are universally quantified (as well as the objects they \Arrow\ Y\ (\EndoR\ Z)$ are universally quantified (as well as the objects they
range over). $\fish$ is the kleisli-arrow which is defined as $f \fish g \defeq range over). $\fish$ is the Kleisli-arrow which is defined as $f \fish g \defeq
f \rrr (\bind\ g)$ . (\TODO{Better way to typeset $\fish$?}) f \rrr (\bind\ g)$ . (\TODO{Better way to typeset $\fish$?})
\subsection{Equivalence of formulations} \subsection{Equivalence of formulations}
% %
In my implementation I proceede to show how the one formulation gives rise to In my implementation I proceed to show how the one formulation gives rise to
the other and vice-versa. For the present purpose I will briefly sketch some the other and vice-versa. For the present purpose I will briefly sketch some
parts of this construction: parts of this construction:
The notation I have chosen here in the report The notation I have chosen here in the report
overloads e.g. $\pure$ to both refer to a natural transformation and an arrow. overloads e.g. $\pure$ to both refer to a natural transformation and an arrow.
This is of course not a coincidence as the arrow in the kleisli formulation This is of course not a coincidence as the arrow in the Kleisli formulation
shall correspond exactly to the map on arrows from the natural transformation shall correspond exactly to the map on arrows from the natural transformation
called $\pure$. called $\pure$.
@ -1283,7 +1310,7 @@ In the monoidal formulation we can define $\bind$:
\bind \defeq \join \lll \fmap\ f \bind \defeq \join \lll \fmap\ f
\end{align} \end{align}
% %
And likewise in the kleisli formulation we can define $\join$: And likewise in the Kleisli formulation we can define $\join$:
% %
\begin{align} \begin{align}
\join \defeq \bind\ \identity \join \defeq \bind\ \identity

View file

@ -1,7 +1,7 @@
\chapter{Introduction} \chapter{Introduction}
Functional extensionality and univalence is not expressible in Functional extensionality and univalence is not expressible in
\nomen{Intensional Martin Löf Type Theory} (ITT). This poses a severe limitation \nomen{Intensional Martin Löf Type Theory} (ITT). This poses a severe limitation
on both i. what is \emph{provable} and ii. the \emph{reusability} of proofs. on both i. what is \emph{provable} and ii. the \emph{re-usability} of proofs.
Recent developments have, however, resulted in \nomen{Cubical Type Theory} (CTT) Recent developments have, however, resulted in \nomen{Cubical Type Theory} (CTT)
which permits a constructive proof of these two important notions. which permits a constructive proof of these two important notions.
@ -54,7 +54,7 @@ not true.} There is no way to construct a proof asserting the obvious
equivalence of $f$ and $g$ -- even though we can prove them equal for all equivalence of $f$ and $g$ -- even though we can prove them equal for all
points. This is exactly the notion of equality of functions that we are points. This is exactly the notion of equality of functions that we are
interested in; that they are equal for all inputs. We call this interested in; that they are equal for all inputs. We call this
\nomen{pointwise equality}, where the \emph{points} of a function refers \nomen{point-wise equality}, where the \emph{points} of a function refers
to it's arguments. to it's arguments.
In the context of category theory functional extensionality is e.g. needed to In the context of category theory functional extensionality is e.g. needed to
@ -73,7 +73,7 @@ The proof obligation that this satisfies the identity law of functors
\end{align*} \end{align*}
% %
One needs functional extensionality to ``go under'' the function arrow and apply One needs functional extensionality to ``go under'' the function arrow and apply
the (left) identity law of the underlying category to proove $\idFun \comp g the (left) identity law of the underlying category to prove $\idFun \comp g
\equiv g$ and thus close the goal. \equiv g$ and thus close the goal.
% %
\subsection{Equality of isomorphic types} \subsection{Equality of isomorphic types}
@ -81,7 +81,7 @@ the (left) identity law of the underlying category to proove $\idFun \comp g
Let $\top$ denote the unit type -- a type with a single constructor. In the 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 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 : that is always true. The type $A \x \top$ and $A$ has an element for each $a :
A$. So in a sense they have the same shape (greek; \nomen{isomorphic}). The A$. So in a sense they have the same shape (Greek; \nomen{isomorphic}). The
second element of the pair does not add any ``interesting information''. It can 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 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 mathematics. Say we look at a set $\{x \mid \phi\ x \land \psi\ x\}$ and somehow
@ -114,6 +114,7 @@ formulate this requirement within our formulation of categories by requiring the
\emph{categories} themselves to be univalent as we shall see. \emph{categories} themselves to be univalent as we shall see.
\section{Context} \section{Context}
\label{sec:context}
% %
The idea of formalizing Category Theory in proof assistants is not new. There The idea of formalizing Category Theory in proof assistants is not new. There
are a multitude of these available online. Just as a first reference see this are a multitude of these available online. Just as a first reference see this
@ -131,7 +132,7 @@ implementations of category theory in Agda:
A formalization in Agda with univalence and functional extensionality as A formalization in Agda with univalence and functional extensionality as
postulates. postulates.
\item \item
\url{https://github.com/pcapriotti/agda-categories} \url{https://github.com/HoTT/HoTT/tree/master/theories/Categories}
A formalization in Coq in the homotopic setting A formalization in Coq in the homotopic setting
\item \item
@ -160,11 +161,11 @@ canonical form.
Another approach is to use the \emph{setoid interpretation} of type theory Another approach is to use the \emph{setoid interpretation} of type theory
(\cite{hofmann-1995,huber-2016}). With this approach one works with (\cite{hofmann-1995,huber-2016}). With this approach one works with
\nomen{extensionals sets} $(X, \sim)$, that is a type $X \tp \MCU$ and an \nomen{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 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'' interpretation the equivalence relation serve as a sort of ``local''
propositional equality. This approach has other drawbacks; it does not satisfy propositional equality. This approach has other drawbacks; it does not satisfy
all propositional equalites of type theory (\TODO{Citation needed}), is all propositional equalities of type theory (\TODO{Citation needed}), is
cumbersome to work with in practice (\cite[p. 4]{huber-2016}) and makes cumbersome to work with in practice (\cite[p. 4]{huber-2016}) and makes
equational proofs less reusable since equational proofs $a \sim_{X} b$ are equational proofs less reusable since equational proofs $a \sim_{X} b$ are
inherently `local' to the extensional set $(X , \sim)$. inherently `local' to the extensional set $(X , \sim)$.

View file

@ -43,7 +43,6 @@
\researchgroup{Programming Logic Group} \researchgroup{Programming Logic Group}
\bibliographystyle{plain} \bibliographystyle{plain}
\addtocontents{toc}{\protect\thispagestyle{empty}}
%% \newtheorem{prop}{Proposition} %% \newtheorem{prop}{Proposition}
\makeatletter \makeatletter
\newcommand*{\rom}[1]{\expandafter\@slowroman\romannumeral #1@} \newcommand*{\rom}[1]{\expandafter\@slowroman\romannumeral #1@}
@ -52,13 +51,15 @@
\pagenumbering{roman} \pagenumbering{roman}
\maketitle \maketitle
\addtocontents{toc}{\protect\thispagestyle{empty}}
\tableofcontents \tableofcontents
\pagenumbering{arabic} \pagenumbering{arabic}
% %
\input{introduction.tex} \input{introduction.tex}
\input{cubical.tex} \input{cubical.tex}
\input{implementation.tex} \input{implementation.tex}
\input{discussion.tex}
\input{conclusion.tex}
\nocite{cubical-demo} \nocite{cubical-demo}
\nocite{coquand-2013} \nocite{coquand-2013}

View file

@ -36,6 +36,8 @@
\usepackage{lmodern} \usepackage{lmodern}
\usepackage{enumerate}
\usepackage{fontspec} \usepackage{fontspec}
\usepackage[light]{sourcecodepro} \usepackage[light]{sourcecodepro}
%% \setmonofont{Latin Modern Mono} %% \setmonofont{Latin Modern Mono}
@ -52,3 +54,5 @@
\usepackage{unicode-math} \usepackage{unicode-math}
%% \RequirePackage{kvoptions} %% \RequirePackage{kvoptions}
\usepackage{pgffor}