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

Corrections

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-05-03 14:18:51 +02:00
parent 2b4ee12ef2
commit 545fb0ade6
5 changed files with 105 additions and 126 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
doc/BACKLOG.md
View file

@ -1,22 +1,7 @@
Remove stuff about models of type theory
Add references to specific (noteable) implementaitons of category theory:
* Unimath
* cubicaltt
* https://github.com/pcapriotti/agda-categories
* https://github.com/copumpkin/categories
* ...
Talk about structure of library:
===
Propositional- and non-propositional stuff split up
Providing "equiality principles"
Provide overview of what has been proven.
What can I say about reusability?
Misc
====
Propositional content

4
doc/cubical.tex
View file

@ -192,6 +192,7 @@ of these theorems here, as they will be used later in chapter
\ref{ch:implementation} throughout.
\subsection{Path induction}
\label{sec:pathJ}
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
``base-case''). For \emph{based path induction}, that equaility is \emph{based}
@ -216,6 +217,7 @@ $$
$$
%
\subsection{Paths over propositions}
\label{sec:lemPropF}
Another very useful combinator is $\lemPropF$:
To `promote' this to a dependent path we can use another useful combinator;
@ -258,6 +260,7 @@ $$
$$
%
\subsection{Functions over propositions}
\label{sec:propPi}
$\prod$-types preserve propositionality when the co-domain is always a
proposition.
%
@ -265,6 +268,7 @@ $$
\mathit{propPi} \tp \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\prod_{a \tp A} P\ a\right)
$$
\subsection{Pairs over propositions}
\label{sec:propSig}
%
$\sum$-types preserve propositionality whenever it's first component is a
proposition, and it's second component is a proposition for all points of in the

145
doc/implementation.tex
View file

@ -42,10 +42,11 @@ Another record encapsulates some laws about this data: associativity of
composition, identity law for the identity morphism. These are standard
requirements for being a category as can be found in standard mathematical
expositions on the topic. We, however, impose one further requirement on what it
means to be a category, namely that the type of arrows form a set. We could
relax this requirement, this would give us the notion of higher categorier
(\cite[p. 307]{hott-2013}). For the purpose of this project, however, this
report will restrict itself to 1-categories.
means to be a category, namely that the type of arrows form a set. Such
categories are called \nomen{1-categories}. We could relax this requirement,
this would give us the notion of higher categorier (\cite[p. 307]{hott-2013}).
For the purpose of this project, however, this report will restrict itself to
1-categories.
Raw categories satisfying these properties are called a pre-categories.
@ -68,8 +69,9 @@ $$
$$
%
The two types are logically equivalent, however. One can construct the latter
from the former simply by ``forgetting'' that $\idToIso$ plays the role
of the equivalence. The other direction is more involved.
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 \ref{sec:univalence}.
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
@ -79,28 +81,21 @@ exactly because the type of arrows form a set, two witnesses must be the same.
All the proofs are really quite mechanical. Lets have a look at one of them: The
identity law states that:
%
$$
\begin{equation}
\var{IsIdentity} \defeq
\prod_{A\ B \tp \Object} \prod_{f \tp A \to B} \id \comp f \equiv f \x f \comp \id \equiv f
$$
\end{equation}
%
There are multiple ways to prove this. Perhaps one of the more intuitive proofs
is by way of the following `combinators':
is by way of the `combinators' $\propPi$ and $\propSig$ presented in sections
\ref{sec:propPi} and \ref{sec:propSig}:
%
$$
\mathit{propPi} \tp \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\prod_{a \tp A} P\ a\right)
$$
\begin{align*}
\mathit{propPi} & \tp \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\prod_{a \tp A} P\ a\right)
\\
\mathit{propSig} & \tp \isProp\ A \to \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\sum_{a \tp A} P\ a\right)
\end{align*}
%
I.e.; pi-types preserve propositionality when the co-domain is always a
proposition.
%
$$
\mathit{propSig} \tp \isProp\ A \to \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\sum_{a \tp A} P\ a\right)
$$
%
I.e.; sigma-types preserve propositionality whenever it's first component is a
proposition, and it's second component is a proposition for all points of in the
left type.
So the proof goes like this: We `eliminate' the 3 function abstractions by
applying $\propPi$ three times. So our proof obligation becomes:
%
@ -135,13 +130,12 @@ $$
$$
%
So let $a\ b \tp \IsPreCategory$ be given. To prove the equality $a \equiv b$ is
to give a continuous path from the index-type into path-space - in this case
$\IsPreCategory$. This path must satisfy being being judgmentally the same as
$a$ at the left endpoint and $b$ at the right endpoint. I.e. a function $I \to
\IsPreCategory$. We know we can form a continuous path between all projections
of $a$ and $b$, this follows from the type of all the projections being mere
propositions. For instance, the path between $\isIdentity_a$ and $\isIdentity_b$
is simply formed by:
to give a continuous path from the index-type into the path-space. I.e. a
function $I \to \IsPreCategory$. This path must satisfy being being judgmentally
the same as $a$ at the left endpoint and $b$ at the right endpoint. We know we
can form a continuous path between all projections of $a$ and $b$, this follows
from the type of all the projections being mere propositions. For instance, the
path between $\isIdentity_a$ and $\isIdentity_b$ is simply formed by:
%
$$
\propIsIdentity\ \isIdentity_a\ \isIdentity_b \tp \isIdentity_a \equiv \isIdentity_b
@ -154,17 +148,18 @@ projections. Once we have such a path e.g. $p \tp \isIdentity_a \equiv
\isIdentity_b$ we can elimiate it with $i$ and thus obtaining $p\ i \tp
\isIdentity_{p\ i}$ and this element satisfies exactly that it corresponds to
the corresponding projections at either endpoint. Thus the element we construct
at $i$ becomes:
at $i$ becomes the triple:
%
\begin{align*}
& \{\ \mathit{propIsAssociative}\ \mathit{isAssociative}_x\
\mathit{isAssociative}_y\ i \\
& ,\ \mathit{propIsIdentity}\ \mathit{isIdentity}_x\
\mathit{isIdentity}_y\ i \\
& ,\ \mathit{propArrowsAreSets}\ \mathit{arrowsAreSets}_x\
\mathit{arrowsAreSets}_y\ i \\
& \}
\end{align*}
\begin{equation}
\begin{alignat}{4}
& \mathit{propIsAssociative} && x.\mathit{isAssociative}\
&& y.\mathit{isAssociative} && i \\
& \mathit{propIsIdentity} && x.\mathit{isIdentity}\
&& y.\mathit{isIdentity} && i \\
& \mathit{propArrowsAreSets} && x.\mathit{arrowsAreSets}\
&& y.\mathit{arrowsAreSets} && i
\end{alignat}
\end{equation}
%
I've found that this to be a general pattern when proving things in homotopy
type theory, namely that you have to wrap and unwrap equalities at different
@ -181,11 +176,11 @@ The situation is a bit more complicated when we have a dependent type. For
instance, when we want to show that $\IsCategory$ is a mere proposition.
$\IsCategory$ is a record with two fields, a witness to being a pre-category and
the univalence condition. Recall that the univalence condition is indexed by the
identity-proof. So if we follow the same recipe as above, let $a\ b \tp
\IsCategory$, to show them equal, we now need to give two paths. One homogenous:
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:
%
$$
p_{\isPreCategory} \tp \isPreCategory_a \equiv \isPreCategory_b
p \tp \isPreCategory_a \equiv \isPreCategory_b
$$
%
and one heterogeneous:
@ -194,29 +189,23 @@ $$
\Path\ (\lambda\; i \mto Univalent_{p\ i})\ \isPreCategory_a\ \isPreCategory_b
$$
%
Which depends on the choice of $p_{\isPreCategory}$. The first of these we can
provide since, as we have shown, $\IsPreCategory$ is a proposition. However,
even though $\Univalent$ is also a proposition, we cannot use this directly to
show the latter. This is becasue $\isProp$ talks about non-dependent paths. To
`promote' this to a dependent path we can use another useful combinator;
$\lemPropF$. Given a type $A \tp \MCU$ and a type family on $A$; $B \tp A \to
\MCU$. Let $P$ be a proposition indexed by an element of $A$ and say we have a
path between some two elements in $A$; $p \tp a_0 \equiv a_1$ then we can built a
heterogeneous path between any two $b$'s at the endpoints:
%
$$
\Path\ (\lambda\; i \mto B\ (p\ i))\ b0\ b1
$$
%
where $b_0 \tp B a_0$ and $b_1 \tp B\ a_1$. This is quite a mouthful, but the
example at present should serve as an illustration. In this case $A =
\mathit{IsIdentity}\ \mathit{identity}$ and $B = \mathit{Univalent}$ we've shown
that being a category is a proposition, a result that holds for any choice of
identity proof. Finally we must provide a proof that the identity proofs at $a$
and $b$ are indeed the same, this we can extract from $p_{\isPreCategory}$ by
applying using congruence of paths: $\congruence\ \mathit{isIdentity}\
p_{\isPreCategory}$
Which depends on the choice of $p$. The first of these we can provide since, as
we have shown, $\IsPreCategory$ is constantly a proposition. However, even
though $\Univalent$ is also a proposition, we cannot use this directly to show
the latter. This is becasue $\isProp$ talks about non-dependent paths. To
`promote' this to a dependent path we can use the combinator; $\lemPropF$
introduced in \ref{sec:lemPropF}.
In this case $A = \mathit{IsIdentity}\ \mathit{identity}$ and $B =
\mathit{Univalent}$ we've shown that being a category is a proposition, a result
that holds for any choice of identity proof. Finally we must provide a proof
that the identity proofs at $a$ and $b$ are indeed the same, this we can extract
from $p$ by applying using congruence of paths:
%
$$
\congruence\ \mathit{isIdentity}\ p
$$
%
When we have a proper category we can make precise the notion of ``identifying
isomorphic types'' \TODO{cite awodey here}. That is, we can construct the
function:
@ -311,7 +300,7 @@ the type $A \cong B$ as well as the the map $A \to B$ that witness this.
Both $\cong$ and $\simeq$ form equivalence relations.
\section{Univalence}
\label{univalence}
\label{sec:univalence}
As noted in the introduction the univalence for types $A\; B \tp \Type$ states
that:
%
@ -342,16 +331,16 @@ equalities and isomorphisms (on arrows). It's worthwhile to dwell on this for a
few seconds. This type looks very similar to univalence for types and is
therefore perhaps a bit more intuitive to grasp the implications of. Of course
univalence for types (which is a proposition -- i.e. provable) does not imply
univalence in any category since morphisms in a category are not regular maps --
in stead they can be thought of as a generalization hereof; i.e. arrows. The
univalence criterion therefore is simply a way of restricting arrows to behave
similarly to maps.
univalence of all pre-category since morphisms in a category are not regular
maps -- in stead they can be thought of as a generalization hereof; i.e. arrows.
The univalence criterion therefore is simply a way of restricting arrows to
behave similarly to maps.
I will now mention a few helpful thoerems that follow from univalence that will
become useful later.
Obviously univalence gives us an isomorphism $A \equiv B \to A \approxeq B$. I
will name these for convenience:
Obviously univalence gives us an isomorphism between $A \equiv B$ and $A
\approxeq B$. I will name these for convenience:
%
$$
\idToIso \tp A \equiv B \to A \approxeq B
@ -366,8 +355,8 @@ an isomorphism $A \approxeq B$ in some category $\bC$ be given. Name the
isomorphism $\iota \tp A \to B$ and its inverse $\widetilde{\iota} \tp B \to A$.
Since $\bC$ is a category (and therefore univalent) the isomorphism induces a
path $p \tp A \equiv B$. From this equality we can get two further paths:
$p_{\mathit{dom}} \tp \mathit{Arrow}\ A\ X \equiv \mathit{Arrow}\ A'\ X$ and
$p_{\mathit{cod}} \tp \mathit{Arrow}\ X\ A \equiv \mathit{Arrow}\ X\ A'$. We
$p_{\mathit{dom}} \tp \mathit{Arrow}\ A\ X \equiv \mathit{Arrow}\ B\ X$ and
$p_{\mathit{cod}} \tp \mathit{Arrow}\ X\ A \equiv \mathit{Arrow}\ X\ B$. We
then have the following two theorems:
%
$$
@ -394,11 +383,11 @@ isomorphism $\mathit{idToIso}\ p \tp A \cong B$. The helper-lemma is similar to
what we're trying to prove but talks about paths rather than isomorphisms:
%
$$
\prod_{f \tp \mathit{Arrow}\ A\ B} \prod_{p \tp A \equiv A'} \mathit{coe}\ p^*\ f \equiv f \lll \mathit{obverse}_{\mathit{idToIso}\ p}
\prod_{f \tp \mathit{Arrow}\ A\ B} \prod_{p \tp A \equiv B} \mathit{coe}\ p_\var{dom}\ f \equiv f \lll \mathit{obverse}_{\mathit{idToIso}\ p}
$$
%
Note that the asterisk in $p^*$ denotes the path $\mathit{Arrow}\ A\ B \equiv
\mathit{Arrow}\ A'\ B$ induced by $p$. To prove this statement I let $f$ and $p$
Again $p_\var{dom}$ denotes the path $\mathit{Arrow}\ A\ X \equiv
\mathit{Arrow}\ B\ X$ induced by $p$. To prove this statement I let $f$ and $p$
be given and then invoke based-path-induction. The induction will be based at $A
\tp \mathit{Object}$, so let $\widetilde{A} \tp \Object$ and $\widetilde{p} \tp
A \equiv \widetilde{A}$ be given. The family that we perform induction over will
@ -551,7 +540,7 @@ $$
(\mathit{hA} \equiv \mathit{hB}) \simeq (\mathit{hA} \approxeq \mathit{hB})
$$
%
Which, as we saw in section \ref{univalence}, is sufficient to show that the
Which, as we saw in section \ref{sec:univalence}, is sufficient to show that the
category is univalent. The way that I have shown this is with a three-step
process. For objects $(A, s_A)\; (B, s_B) \tp \Set$ I show the following chain
of equivalences:

60
doc/introduction.tex
View file

@ -70,27 +70,27 @@ The proof obligation that this satisfies the identity law of functors
%
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
\equiv g$ and thus closing the goal.
\equiv g$ and thus close the goal.
%
\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 : A$. So in a sense they are the same. 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.
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 :
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
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
\nomen{equivalent} types. I will return to the definition of equivalence later,
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. The principle of univalence says that:
\nomen{equivalent} types. I will return to the definition of equivalence later
in section \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. The principle of univalence says that:
%
$$\mathit{univalence} \tp (A \simeq B) \simeq (A \equiv B)$$
%
@ -99,14 +99,14 @@ In particular this allows us to construct an equality from an equivalence
\section{Formalizing Category Theory}
%
The above examples serve to illustrate the limitation of Agda. One case where
these limitations are particularly prohibitive is in the study of Category
Theory. At a glance category theory can be described as ``the mathematical study
of (abstract) algebras of functions'' (\cite{awodey-2006}). So by that token
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 ``the mathematical study of
(abstract) algebras of functions'' (\cite{awodey-2006}). So by that token
functional extensionality is particularly useful for formulating Category
Theory. In Category theory it is also common to identify isomorphic structures
and this is exactly what we get from univalence. In fact we can formulate this
requirement within our formulation of categories by requiring the
and 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.
\section{Context}
@ -117,7 +117,7 @@ Inspiration:
* HoTT - sketch of homotopy proofs
\end{verbatim}
The idea of formalizing Category Theory in proof assistants is not new. There
are a multitude of these available online. Just as first reference see this
are a multitude of these available online. Just as a first reference see this
question on Math Overflow: \cite{mo-formalizations}. Notably these
implementations of category theory in Agda:
\begin{itemize}
@ -137,17 +137,17 @@ will make it possible to prove more things and to reuse proofs.
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
\nomen{canonicity} (\cite{huber-2016}). Canonicity means that any well-typed
term evaluates to a \emph{canonical} form. For example for a closed term $e :
\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.
\nomen{canonicity} (\TODO{Pageno!} \cite{huber-2016}). Canonicity means that any
well-typed term evaluates to a \emph{canonical} form. For example for a closed
term $e : \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.
Another approach is to use the \emph{setoid interpretation} of type theory
(\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
equivalence relation $\sim$.
equivalence relation $\sim \tp X \to X \to \MCU$.
Types should additionally `carry around' an equivalence relation that serve as
propositional equality. This approach has other drawbacks; it does not satisfy

5
doc/main.tex
View file

@ -43,14 +43,15 @@
\researchgroup{Programming Logic Group}
\bibliographystyle{plain}
\addtocontents{toc}{\protect\thispagestyle{empty}}
\begin{document}
\pagenumbering{roman}
\maketitle
\tableofcontents
%
\pagenumbering{arabic}
%
\input{introduction.tex}
\input{cubical.tex}
\input{implementation.tex}