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

Fix its it's mistakes

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-05-09 18:34:05 +02:00
parent bc8309c0cd
commit 34798632f2
3 changed files with 15 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
doc/cubical.tex
View file

@ -1,6 +1,6 @@
\chapter{Cubical Agda} \chapter{Cubical Agda}
\section{Propositional equality} \section{Propositional equality}
Judgmental equality in Agda is a feature of the type-system. It's something that Judgmental equality in Agda is a feature of the type-system. Its something that
can be checked automatically by the type-checker: In the example from the can be checked automatically by the type-checker: In the example from the
introduction $n + 0$ can be judged to be equal to $n$ simply by expanding the introduction $n + 0$ can be judged to be equal to $n$ simply by expanding the
definition of $+$. definition of $+$.
@ -81,7 +81,7 @@ endpoints. I.e.:
\end{align*} \end{align*}
% %
The notion of ``homogeneous equalities'' is recovered when $P$ does not depend The notion of ``homogeneous equalities'' is recovered when $P$ does not depend
on it's argument: on its argument:
% %
$$ $$
a_0 \equiv a_1 \defeq \Path\ (\lambda i \to A)\ a_0\ a_1 a_0 \equiv a_1 \defeq \Path\ (\lambda i \to A)\ a_0\ a_1
@ -107,7 +107,7 @@ definitionally. So to inhabit it, is to give a path $I \to A$ which is
judgmentally $a$ at either endpoint. This is satisfied by the constant path; judgmentally $a$ at either endpoint. This is satisfied by the constant path;
i.e. the path that stays at $a$ at any index $i$. i.e. the path that stays at $a$ at any index $i$.
It's also surpisingly easy to show functional extensionality with which we can It is also surpisingly easy to show functional extensionality with which we can
construct a path between $f$ and $g$ -- the function defined in the introduction construct a path between $f$ and $g$ -- the function defined in the introduction
(section \S\ref{sec:functional-extensionality}). (section \S\ref{sec:functional-extensionality}).
%% module _ {ℓa ℓb} {A : Set ℓa} {B : A → Set ℓb} where %% module _ {ℓa ℓb} {A : Set ℓa} {B : A → Set ℓb} where
@ -335,8 +335,8 @@ $$
\subsection{Pairs over propositions} \subsection{Pairs over propositions}
\label{sec:propSig} \label{sec:propSig}
% %
$\sum$-types preserve propositionality whenever it's first component is a $\sum$-types preserve propositionality whenever its first component is a
proposition, and it's second component is a proposition for all points of in the proposition, and its second component is a proposition for all points of in the
left type. left type.
% %
$$ $$

16
doc/implementation.tex
View file

@ -70,7 +70,7 @@ constituents of a category and can be found in typical mathematical expositions
on the topic. We, however, impose one further requirement on what it means to be 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 is possible to relax this
requirement. This would lead to the notion of higher categories (\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
@ -367,7 +367,7 @@ $$
\fiber\ f\ b \defeq \sum_{a \tp A} \left( b \equiv f\ a \right) \fiber\ f\ b \defeq \sum_{a \tp A} \left( b \equiv f\ a \right)
$$ $$
% %
I give it's definition here mainly for completeness, because as I stated we can I give its definition here mainly for completeness, because as I stated we can
move away from this specific instantiation and think about it more abstractly move away from this specific instantiation and think about it more abstractly
once we have shown that this definition actually works as an equivalence. once we have shown that this definition actually works as an equivalence.
@ -420,7 +420,7 @@ $$
$$ $$
% %
That is, we must demonstrate that there is an isomorphism (on types) between That is, we must demonstrate that there is an isomorphism (on types) between
equalities and isomorphisms (on arrows). It's worthwhile to dwell on this for a equalities and isomorphisms (on arrows). It is worthwhile to dwell on this for a
few seconds. This type looks very similar to univalence for types and is 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 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 for types (which is a proposition -- i.e. provable) does not imply
@ -525,7 +525,7 @@ And this finishes the proof of \ref{eq:coeDomIso} and thus \ref{eq:coeDom}.
\subsection{Opposite category} \subsection{Opposite category}
\label{op-cat} \label{op-cat}
The first category I'll present is a pure construction on categories. Given some The first category I'll present is a pure construction on categories. Given some
category we can construct it's dual, called the opposite category. Starting with 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 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 univalence in a very simple category where the structure of the category is
rather simple. rather simple.
@ -566,12 +566,12 @@ section \S\ref{sec:equiv} gave us some tools to work with equivalences. We saw
that we can prove this category univalent by giving an inverse to that we can prove this category univalent by giving an inverse to
$\wideoverbar{\idToIso} \tp (A \equiv B) \to (A \wideoverbar{\approxeq} B)$. $\wideoverbar{\idToIso} \tp (A \equiv B) \to (A \wideoverbar{\approxeq} B)$.
From the original category we have that $\idToIso \tp (A \equiv B) \to (A \cong From the original category we have that $\idToIso \tp (A \equiv B) \to (A \cong
B)$ is an isomorphism. Let us denote it's inverse with $\isoToId \tp (A B)$ is an isomorphism. Let us denote its inverse with $\isoToId \tp (A
\approxeq B) \to (A \equiv B)$. If we squint we can see what we need is a way to \approxeq B) \to (A \equiv B)$. If we squint we can see what we need is a way to
go between $\wideoverbar{\approxeq}$ and $\approxeq$. go between $\wideoverbar{\approxeq}$ and $\approxeq$.
An inhabitant of $A \approxeq B$ is simply an arrow $f \tp \Arrow\ A\ B$ An inhabitant of $A \approxeq B$ is simply an arrow $f \tp \Arrow\ A\ B$
and it's inverse $g \tp \Arrow\ B\ A$. In the opposite category $g$ will and its inverse $g \tp \Arrow\ B\ A$. In the opposite category $g$ will
play the role of the isomorphism and $f$ will be the inverse. Similarly we can play the role of the isomorphism and $f$ will be the inverse. Similarly we can
go in the opposite direction. I name these maps $\shuffle \tp (A \approxeq go in the opposite direction. I name these maps $\shuffle \tp (A \approxeq
B) \to (A \wideoverbar{\approxeq} B)$ and $\shuffle^{-1} \tp (A B) \to (A \wideoverbar{\approxeq} B)$ and $\shuffle^{-1} \tp (A
@ -832,7 +832,7 @@ $\pi$ is called the product (arrow) of $f$ and $g$.
\newcommand\pairB{\mathcal{B}} \newcommand\pairB{\mathcal{B}}
Given a base category $\bC$ and two objects in this category $\pairA$ and Given a base category $\bC$ and two objects in this category $\pairA$ and
$\pairB$ we can construct the ``pair category'': \TODO{This is a working title, $\pairB$ we can construct the ``pair category'': \TODO{This is a working title,
it's nice to have a name for this thing to refer back to} it is nice to have a name for this thing to refer back to}
The type of objects in this category will be an object in the underlying The type of objects in this category will 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)
@ -1291,7 +1291,7 @@ The Kleisli-formulation consists of the following data:
% %
The objects $X$ and $Y$ are implicitly universally quantified. The objects $X$ and $Y$ are implicitly universally quantified.
It's interesting to note here that this formulation does not talk about natural It is interesting to note here that this formulation does not talk about natural
transformations or other such constructs from category theory. All we have here transformations or other such constructs from category theory. All we have here
is a regular maps on objects and a pair of arrows. is a regular maps on objects and a pair of arrows.
% %

4
doc/sources.tex
View file

@ -1,4 +1,4 @@
\chapter{Source code} \chapter{Source code excerpts}
\label{ch:app-sources} \label{ch:app-sources}
In the following a few of the definitions mentioned in the report are included. In the following a few of the definitions mentioned in the report are included.
The following is \emph{not} a verbatim copy of individual modules from the The following is \emph{not} a verbatim copy of individual modules from the
@ -6,7 +6,6 @@ implementation. Rather, this is a redacted and pre-formatted designed for
presentation purposes. It's provided here as a convenience. The actual sources presentation purposes. It's provided here as a convenience. The actual sources
are the only authoritative source. Is something is not clear, please refer to are the only authoritative source. Is something is not clear, please refer to
those. those.
\clearpage
\section{Cubical} \section{Cubical}
\label{sec:app-cubical} \label{sec:app-cubical}
\begin{figure}[h] \begin{figure}[h]
@ -24,6 +23,7 @@ module _ {ℓ} {A : Set ℓ} where
\end{Verbatim} \end{Verbatim}
\caption{Excerpt from the cubical library. Definition of the path-type.} \caption{Excerpt from the cubical library. Definition of the path-type.}
\end{figure} \end{figure}
\clearpage
% %
\begin{figure}[h] \begin{figure}[h]
\begin{Verbatim} \begin{Verbatim}