Add chapter on cubical
This commit is contained in:
parent
852eb0757f
commit
2b4ee12ef2
|
|
@ -41,6 +41,7 @@
|
|||
\newgeometry{top=3cm, bottom=3cm,left=2.25 cm, right=2.25cm}
|
||||
\begingroup
|
||||
\usepackage{noto}
|
||||
\fontseries{sb}
|
||||
%% \fontfamily{noto}\selectfont
|
||||
{\Huge\@title}\\[.5cm]
|
||||
{\Large A formalization of category theory in Cubical Agda}\\[.5cm]
|
||||
|
|
|
|||
275
doc/cubical.tex
Normal file
275
doc/cubical.tex
Normal file
|
|
@ -0,0 +1,275 @@
|
|||
\chapter{Cubical Agda}
|
||||
\section{Propositional equality}
|
||||
In Agda judgmental equality is a feature of the type-system. It's a property of
|
||||
types that can be checked by computational means. In the example from the
|
||||
introduction $n + 0$ can be judged to be equal to $n$ simply by expanding the
|
||||
definition of $+$.
|
||||
|
||||
Propositional equality on the other hand is defined within the language itself.
|
||||
Cubical Agda extends the underlying type system (\TODO{Cite someone smarter than
|
||||
me with a good resource on this}) but introduces a data-type within the
|
||||
languages.
|
||||
|
||||
\subsection{The equality type}
|
||||
The usual notion of judgmental equality says that given a type $A \tp \MCU$ and
|
||||
two points of $A$; $a_0, a_1 \tp A$ we can form the type:
|
||||
%
|
||||
\begin{align}
|
||||
a_0 \equiv a_1 \tp \MCU
|
||||
\end{align}
|
||||
%
|
||||
In Agda this is defined as an inductive data-type with the single constructor:
|
||||
%
|
||||
\begin{align}
|
||||
\refl \tp a \equiv a
|
||||
\end{align}
|
||||
%
|
||||
For any $a \tp A$.
|
||||
|
||||
There also exist a related notion of \emph{heterogeneous} equality where allows
|
||||
for equating points of different types. In this case given two types $A, B \tp
|
||||
\MCU$ and two points $a \tp A$, $b \tp B$ we can construct the type:
|
||||
%
|
||||
\begin{align}
|
||||
a \cong b \tp \MCU
|
||||
\end{align}
|
||||
%
|
||||
This is likewise defined as an inductive data-type with a single constructors:
|
||||
%
|
||||
\begin{align}
|
||||
\refl \tp a \cong a
|
||||
\end{align}
|
||||
%
|
||||
In Cubical Agda these two notions are paralleled with homogeneous- and
|
||||
heterogeneous paths respectively.
|
||||
%
|
||||
\subsection{The path type}
|
||||
In Cubical Agda judgmental equality is encapsulated with the type:
|
||||
%
|
||||
$$
|
||||
\Path \tp (P : I → \MCU) → P\ 0 → P\ 1 → \MCU
|
||||
$$
|
||||
%
|
||||
$I$ is a special data-type (\TODO{that also has special computational properties
|
||||
AFAIK}) called the index set. $I$ can be thought of simply as the interval on
|
||||
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
|
||||
\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
|
||||
$\Path$ because it is connected with paths in homotopy thoery. The intuition
|
||||
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
|
||||
one has moved. An inhabitant of $\Path\ P\ a_0\ a_1$ is a (dependent-)
|
||||
function, $p$, from the index-space to the path-space:
|
||||
%
|
||||
$$
|
||||
p \tp I \to P\ i
|
||||
$$
|
||||
%
|
||||
Which must satisfy being judgmentally equal to $a_0$ (respectively $a_1$) at the
|
||||
endpoints. I.e.:
|
||||
%
|
||||
\begin{align*}
|
||||
p\ 0 & = a_0 \\
|
||||
p\ 1 & = a_1
|
||||
\end{align}
|
||||
%
|
||||
The notion of ``homogeneous equalities'' can be recovered by not letting the
|
||||
path-space $P$ depend on it's argument:
|
||||
%
|
||||
$$
|
||||
a_0 \equiv a_1 \defeq \Path\ (\lambda i \to A)\ a_0\ a_1
|
||||
$$
|
||||
%
|
||||
For $A \tp \MCU$, $a_0, a_1 \tp A$. I will generally prefer to use the notation
|
||||
$a_0 \equiv a_1$ when talking about non-dependent paths and use the notation
|
||||
$\Path\ (\lambda i \to A)\ a_0\ a_1$ 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$:
|
||||
%
|
||||
\begin{align}
|
||||
\refl & \tp \Path (\lambda i \to A)\ a\ a \\
|
||||
\refl & \defeq \lambda i \to a
|
||||
\end{align}
|
||||
%
|
||||
Or, in other terms; reflexivity is the path in $A$ that is $a$ at the left
|
||||
endpoint as well as at the right endpoint. It is inhabited by the path which
|
||||
stays constantly at $a$ at any index $i$.
|
||||
|
||||
Paths have some other important properties, but they are not the focus of this
|
||||
thesis. \TODO{Refer the reader somewhere for more info.}
|
||||
%
|
||||
\section{Homotopy levels}
|
||||
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
|
||||
don't have any interesting structure. This is referred to as uniqueness of
|
||||
identity proofs. Unfortunately this is orthogonal to univalence that only makes
|
||||
sense in the absence of UIP.
|
||||
|
||||
In homotopy type theory we have a hierarchy of types based on their ``internal
|
||||
structure''. At the bottom of this hierarchy we have the set of contractible
|
||||
types:
|
||||
%
|
||||
\begin{equation}
|
||||
\begin{alignat}{2}
|
||||
& \isContr && \tp \MCU \to \MCU \\
|
||||
& \isContr\ A && \defeq \sum_{c \tp A} \prod_{a \tp A} a \equiv c
|
||||
\end{alignedat}
|
||||
\end{equation}
|
||||
%
|
||||
The first component of $\isContr\ A$ is called ``the center of contraction''.
|
||||
Under the propositions-as-types interpretation of type-theory $\isContr\ A$ can
|
||||
be thought of as ``the true proposition $A$''. It is a theorem that if a type is
|
||||
contractible, then it is isomorphic to the unit-type $\top$.
|
||||
|
||||
The next step in the hierarchy is the set of mere propositions:
|
||||
%
|
||||
\begin{equation}
|
||||
\begin{alignat}{2}
|
||||
& \isProp && \tp \MCU \to \MCU \\
|
||||
& \isProp\ A && \defeq \prod_{a_0, a_1 \tp A} a_0 \equiv a_1
|
||||
\end{alignedat}
|
||||
\end{equation}
|
||||
%
|
||||
$\isProp\ A$ can be thought of as the set of true and false propositions. It is
|
||||
a result that if a mere proposition $A$ is inhabited, then so is it
|
||||
contractible. If it is not inhabited it is equivalent to the empty-type (or
|
||||
false proposition).\TODO{Cite!!}
|
||||
|
||||
I will refer to a type $A \tp \MCU$ as a \emph{mere} proposition if I want to
|
||||
stress that we have $\isProp\ A$.
|
||||
|
||||
Then comes the set of homotopical sets:
|
||||
%
|
||||
\begin{equation}
|
||||
\begin{alignat}{2}
|
||||
& \isSet && \tp \MCU \to \MCU \\
|
||||
& \isSet\ A && \defeq \prod_{a_0, a_1 \tp A} \isProp\ (a_0 \equiv a_1)
|
||||
\end{alignedat}
|
||||
\end{equation}
|
||||
%
|
||||
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 refer to a type $A$ as a set exactly
|
||||
if $\isSet\ A$ is inhabited.
|
||||
|
||||
The next step in the hierarchy is, as you might've guessed, the type:
|
||||
%
|
||||
\begin{equation}
|
||||
\begin{alignat}{2}
|
||||
& \isGroupoid && \tp \MCU \to \MCU \\
|
||||
& \isGroupoid\ A && \defeq \prod_{a_0, a_1 \tp A} \isSet\ (a_0 \equiv a_1)
|
||||
\end{alignedat}
|
||||
\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 tyes, is said to be a \nomen{-2-type}, propositions
|
||||
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
|
||||
thesis. But I mention here some properties that will be relevant for this
|
||||
exposition:
|
||||
|
||||
Proposition: Homotopy levels are cumulative. That is, if $A \tp \MCU$ has
|
||||
homotopy level $n$ then so does it have $n + 1$.
|
||||
|
||||
Let $\left\Vert A \right\Vert = n$ denote that the level of $A$ is $n$.
|
||||
Proposition: For any homotopic level $n$ this is a mere proposition.
|
||||
%
|
||||
\section{A few lemmas}
|
||||
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
|
||||
already that have already been formalized. Specifically the results come from
|
||||
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}.}
|
||||
|
||||
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
|
||||
of these theorems here, as they will be used later in chapter
|
||||
\ref{ch:implementation} throughout.
|
||||
|
||||
\subsection{Path induction}
|
||||
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}
|
||||
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:
|
||||
%
|
||||
$$
|
||||
P \tp \prod_{a' \tp A} \prod_{p \tp a ≡ a'} \MCU
|
||||
$$
|
||||
%
|
||||
And an inhabitant of $P$ at $\refl$:
|
||||
%
|
||||
$$
|
||||
p \tp P\ a\ \refl
|
||||
$$
|
||||
%
|
||||
We have the function:
|
||||
%
|
||||
$$
|
||||
\pathJ\ P\ p \tp \prod_{a' \tp A} \prod_{p \tp a ≡ a'} P\ a\ p
|
||||
$$
|
||||
%
|
||||
\subsection{Paths over propositions}
|
||||
Another very useful combinator is $\lemPropF$:
|
||||
|
||||
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$; $P \tp A \to
|
||||
\MCU$. Let $\var{propP} \tp \prod_{x \tp A} \isProp\ (P\ x)$ be the proof that
|
||||
$P$ is a mere proposition for all elements of $A$. Furthermore 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 elements of $p_0 \tp P\ a_0$ and $p_1 \tp
|
||||
P\ a_1$:
|
||||
%
|
||||
$$
|
||||
\lemPropF\ \var{propP}\ p \defeq \Path\ (\lambda\; i \mto P\ (p\ i))\ p_0\ p_1
|
||||
$$
|
||||
%
|
||||
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
|
||||
$\lemPropF$ can be used to boil this complexity down to showing that the
|
||||
dependent parts of the type are mere propositions. For instance, saw we have a type:
|
||||
%
|
||||
$$
|
||||
T \defeq \sum_{a : A} P\ a
|
||||
$$
|
||||
%
|
||||
For some proposition $P \tp A \to \MCU$. 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:
|
||||
%
|
||||
%
|
||||
\begin{align*}
|
||||
p \tp & \fst\ t_0 \equiv \fst\ t_1 \\
|
||||
& \Path\ (\lambda i \to P\ (p\ i))\ \snd\ t_0 \equiv \snd\ t_1
|
||||
\end{align*}
|
||||
%
|
||||
Here $\lemPropF$ directly allow us to prove the latter of these:
|
||||
%
|
||||
$$
|
||||
\lemPropF\ \var{propP}\ p
|
||||
\tp \Path\ (\lambda i \to P\ (p\ i))\ \snd\ t_0 \equiv \snd\ t_1
|
||||
$$
|
||||
%
|
||||
\subsection{Functions over propositions}
|
||||
$\prod$-types preserve propositionality when the co-domain is always a
|
||||
proposition.
|
||||
%
|
||||
$$
|
||||
\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}
|
||||
%
|
||||
$\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
|
||||
left type.
|
||||
%
|
||||
$$
|
||||
\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)
|
||||
$$
|
||||
|
|
@ -1,5 +1,6 @@
|
|||
\chapter{Implementation}
|
||||
This implementation formalizes the following concepts $>\!\!>\!\!=$:
|
||||
\chapter{Category Theory}
|
||||
\label{ch:implementation}
|
||||
This implementation formalizes the following concepts:
|
||||
%
|
||||
\begin{itemize}
|
||||
\item Core categorical concepts
|
||||
|
|
@ -224,19 +225,18 @@ $$
|
|||
\isoToId \tp (A \approxeq B) \to (A \equiv B)
|
||||
$$
|
||||
%
|
||||
One application of this, and a perhaps somewhat surprising result, is that
|
||||
terminal objects are propositional. Intuitively; they do not
|
||||
have any interesting structure:
|
||||
A perhaps somewhat surprising application of this is that we can show that
|
||||
terminal objects are propositional:
|
||||
%
|
||||
\begin{align}
|
||||
\label{eq:termProp}
|
||||
\isProp\ \var{Terminal}
|
||||
\end{align}
|
||||
%
|
||||
The proof of this follows from the usual
|
||||
observation that any two terminal objects are isomorphic. The proof is omitted
|
||||
here, but the curious reader can check the implementation for the details.
|
||||
\TODO{The proof is a bit fun, should I include it?}
|
||||
It follows from the usual observation that any two terminal objects are
|
||||
isomorphic - and since categories are univalent, so are they equal. The proof is
|
||||
omitted here, but the curious reader can check the implementation for the
|
||||
details. \TODO{The proof is a bit fun, should I include it?}
|
||||
|
||||
\section{Equivalences}
|
||||
\label{sec:equiv}
|
||||
|
|
@ -477,21 +477,21 @@ direction. I name these maps $\mathit{shuffle} \tp (A \approxeq B) \to (A
|
|||
\approxeq B)$ respectively.
|
||||
|
||||
As the inverse of $\idToIso_{\mathit{Op}}$ I will pick $\zeta \defeq \eta \comp
|
||||
\mathit{shuffle}$. The proof that they are inverses go as follows:
|
||||
\var{shuffle}$. The proof that they are inverses go as follows:
|
||||
%
|
||||
\begin{align*}
|
||||
\zeta \comp \idToIso & \equiv
|
||||
\eta \comp \shuffle \comp \idToIso
|
||||
\eta \comp \var{shuffle} \comp \idToIso
|
||||
&& \text{by definition} \\
|
||||
%% ≡⟨ cong (λ φ → φ x) (cong (λ φ → η ⊙ shuffle ⊙ φ) (funExt lem)) ⟩ \\
|
||||
%
|
||||
& \equiv
|
||||
\eta \comp \shuffle \comp \inv{\shuffle} \comp \idToIso
|
||||
\eta \comp \var{shuffle} \comp \inv{\var{shuffle}} \comp \idToIso
|
||||
&& \text{lemma} \\
|
||||
%% ≡⟨⟩ \\
|
||||
& \equiv
|
||||
\eta \comp \idToIso_{\bC}
|
||||
&& \text{$\shuffle$ is an isomorphism} \\
|
||||
&& \text{$\var{shuffle}$ is an isomorphism} \\
|
||||
%% ≡⟨ (λ i → verso-recto i x) ⟩ \\
|
||||
& \equiv
|
||||
\identity
|
||||
|
|
@ -500,7 +500,7 @@ As the inverse of $\idToIso_{\mathit{Op}}$ I will pick $\zeta \defeq \eta \comp
|
|||
%
|
||||
The other direction is analogous.
|
||||
|
||||
The lemma used in this proof states that $\idToIso \equiv \inv{\shuffle} \comp
|
||||
The lemma used in this proof states that $\idToIso \equiv \inv{\var{shuffle}} \comp
|
||||
\idToIso_{\bC}$ it's a rather straight-forward proof since being-an-inverse-of
|
||||
is a proposition.
|
||||
|
||||
|
|
|
|||
|
|
@ -155,16 +155,3 @@ all judgemental equalites of type theory, is 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 inherently `local' to the extensional set
|
||||
$(X , \sim)$.
|
||||
%
|
||||
\section{The equality type}
|
||||
The usual definition of equality in Agda is an inductive data-type with a single
|
||||
constructor:
|
||||
%
|
||||
%% \VerbatimInput{../libs/main.tex}
|
||||
% \def\verbatim@font{xits}
|
||||
\begin{verbatim}
|
||||
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
|
||||
instance refl : x ≡ x
|
||||
\end{verbatim}
|
||||
%
|
||||
I shall refer to this as the (usual) inductive equality type.
|
||||
|
|
|
|||
|
|
@ -47,6 +47,8 @@
|
|||
\newcommand{\idToIso}{\var{idToIso}}
|
||||
\newcommand{\isSet}{\var{isSet}}
|
||||
\newcommand{\isContr}{\var{isContr}}
|
||||
\newcommand{\isGroupoid}{\var{isGroupoid}}
|
||||
\newcommand{\pathJ}{\var{pathJ}}
|
||||
\newcommand\Object{\var{Object}}
|
||||
\newcommand\Functor{\var{Functor}}
|
||||
\newcommand\isProp{\var{isProp}}
|
||||
|
|
|
|||
|
|
@ -43,6 +43,7 @@
|
|||
\researchgroup{Programming Logic Group}
|
||||
\bibliographystyle{plain}
|
||||
|
||||
|
||||
\begin{document}
|
||||
|
||||
\pagenumbering{roman}
|
||||
|
|
@ -51,6 +52,7 @@
|
|||
%
|
||||
\pagenumbering{arabic}
|
||||
\input{introduction.tex}
|
||||
\input{cubical.tex}
|
||||
\input{implementation.tex}
|
||||
|
||||
\nocite{cubical-demo}
|
||||
|
|
|
|||
Loading…
Reference in a new issue