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

Remove all my beloved contractions :(

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-05-09 18:47:12 +02:00
parent 34798632f2
commit 616d85351a
5 changed files with 41 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
doc/cubical.tex
View file

@ -149,7 +149,7 @@ this thesis. \TODO{Refer the reader somewhere for more info.}
\section{Homotopy levels} \section{Homotopy levels}
In ITT all equality proofs are identical (in a closed context). This means that, 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 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 do not have any interesting structure. This is referred to as Uniqueness of
Identity Proofs (UIP). Unfortunately it is not possible to have a type-theory Identity Proofs (UIP). Unfortunately it is not possible to have a type-theory
with both univalence and UIP. In stead we have a hierarchy of types with an with both univalence and UIP. In stead we have a hierarchy of types with an
increasing amount of homotopic structure. At the bottom of this hierarchy we increasing amount of homotopic structure. At the bottom of this hierarchy we
@ -192,9 +192,9 @@ indeed both $\top$ and $\bot$ are propositions:
λ\varnothing\ \varnothing & \tp \isProp\ ⊥ λ\varnothing\ \varnothing & \tp \isProp\ ⊥
\end{align*} \end{align*}
% %
I've used $\varnothing$ here to denote an impossible pattern. It is a theorem $\varnothing$ is used here to denote an impossible pattern. It is a theorem that
that if a mere proposition $A$ is inhabited, then so is it contractible. If it if a mere proposition $A$ is inhabited, then so is it contractible. If it is not
is not inhabited it is equivalent to the empty-type (or false inhabited it is equivalent to the empty-type (or false
proposition).\TODO{Cite!!} proposition).\TODO{Cite!!}
I will refer to a type $A \tp \MCU$ as a \emph{mere} proposition if I want to I will refer to a type $A \tp \MCU$ as a \emph{mere} proposition if I want to
@ -209,15 +209,15 @@ Then comes the set of homotopical sets:
\end{aligned} \end{aligned}
\end{equation} \end{equation}
% %
I won't give an example of a set at this point. It turns out that proving e.g. I will not give an example of a set at this point. It turns out that proving
$\isProp\ \bN$ is not so straight-forward (see \cite[\S3.1.4]{hott-2013}). e.g. $\isProp\ \bN$ is not so straight-forward (see \cite[\S3.1.4]{hott-2013}).
There will be examples of sets later in this report. At this point it should be There will be examples of sets later in this report. At this point it should be
noted that the term ``set'' is somewhat conflated; there is the notion of sets 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 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 consistently to refer to a type $A$ as a set exactly if $\isSet\ A$ is a
a proposition. proposition.
The next step in the hierarchy is, as the reader might've guessed, the type: As the reader may have guessed the next step in the hierarchy is the type:
% %
\begin{equation} \begin{equation}
\begin{aligned} \begin{aligned}
@ -278,8 +278,8 @@ We have the function:
\pathJ\ P\ p \tp \prod_{a' \tp A} \prod_{p \tp a ≡ a'} P\ a\ p \pathJ\ P\ p \tp \prod_{a' \tp A} \prod_{p \tp a ≡ a'} P\ a\ p
\end{equation} \end{equation}
% %
I will not give an example of using $\pathJ$ here. But we'll see an application I will not give an example of using $\pathJ$ here. An application can be found
of it in \ref{eq:pathJ-example}. later in \ref{eq:pathJ-example}.
\subsection{Paths over propositions} \subsection{Paths over propositions}
\label{sec:lemPropF} \label{sec:lemPropF}

6
doc/discussion.tex
View file

@ -7,9 +7,9 @@ to very complicated goals. One technique for alleviating this was to prove that
certain types are mere propositions. certain types are mere propositions.
\subsection{Computational properties} \subsection{Computational properties}
Another aspect (\TODO{That I actually didn't highlight very well in the previous Another aspect (\TODO{That I actually did not highlight very well in the
chapter}) is the computational nature of paths. Say we have formalized this previous chapter}) is the computational nature of paths. Say we have
common result about monads: formalized this common result about monads:
\TODO{Some equation\ldots} \TODO{Some equation\ldots}

48
doc/implementation.tex
View file

@ -186,11 +186,11 @@ 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$. Similar combinators can be defined `canonical' types like $\sum$ and $\prod$. Similar combinators can be defined at
at the other homotopic levels. These combinators are however not applicable in 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 have
ourselves. For instance, after we've proven that all the projections of defined ourselves. For instance, after we have proven that all the projections
pre-categories are propositions, then we would like to bundle this up to show of pre-categories are propositions, then we would like to bundle this up to show
that the type of pre-categories is also a proposition. Formally: that the type of pre-categories is also a proposition. Formally:
% %
\begin{equation} \begin{equation}
@ -208,8 +208,7 @@ Where The definition of $\IsPreCategory$ is the triple:
% %
Each corresponding to the first three laws for categories. Note that since 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 $\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 combinators available to help us here. In stead the paths must be used directly.
directly.
\ref{eq:propIsPreCategory} is judgmentally the same as \ref{eq:propIsPreCategory} is judgmentally the same as
% %
@ -252,7 +251,7 @@ $i$ becomes the triple:
\end{aligned} \end{aligned}
\end{equation} \end{equation}
% %
I've found this to be a general pattern when proving things in homotopy type I have found this to be a general pattern when proving things in homotopy type
theory, namely that you have to wrap and unwrap equalities at different levels. theory, namely that you have to wrap and unwrap equalities at different levels.
It is worth noting that proving this theorem with the regular inductive equality 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
@ -287,7 +286,7 @@ 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 was introduced in \S\ref{sec:lemPropF}. To this end we can use $\lemPropF$, which was introduced in \S\ref{sec:lemPropF}.
In this case $A = \var{IsIdentity}\ \identity$ and $B = \Univalent$. We've In this case $A = \var{IsIdentity}\ \identity$ and $B = \Univalent$. We have
shown that being a category is a proposition, a result that holds for any choice 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 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 $a$ and $b$ are indeed the same, this we can extract from $p$ by applying
@ -473,7 +472,7 @@ I will give the proof of the first theorem here, the second one is analogous.
In the second step we use the fact that $p$ is constructed from the isomorphism In the second step we use the fact that $p$ is constructed from the isomorphism
$\iota$ -- $\inv{(\idToIso\ p)}$ denotes the map $B \to A$ induced by the $\iota$ -- $\inv{(\idToIso\ p)}$ denotes the map $B \to A$ induced by the
isomorphism $\idToIso\ p \tp A \cong B$. The helper-lemma is similar to isomorphism $\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: what we are trying to prove but talks about paths rather than isomorphisms:
% %
\begin{equation} \begin{equation}
\label{eq:coeDomIso} \label{eq:coeDomIso}
@ -524,9 +523,9 @@ And this finishes the proof of \ref{eq:coeDomIso} and thus \ref{eq:coeDom}.
\section{Categories} \section{Categories}
\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 will present is a pure construction on categories. Given
category we can construct its dual, called the opposite category. Starting with some category we can construct its dual, called the opposite category. Starting
a simple example allows us to focus on how we work with equivalences and with a simple example allows us to focus on how we work with equivalences and
univalence in a very simple category where the structure of the category is univalence in a very simple category where the structure of the category is
rather simple. rather simple.
@ -537,7 +536,7 @@ an arrow from $B$ to $A$ in the underlying category. The identity arrow is the
same as the one in the underlying category (they have the same type). Function same as the one in the underlying category (they have the same type). Function
composition will be reverse function composition from the underlying category. composition will be reverse function composition from the underlying category.
I'll refer to things in terms of the underlying category, unless they have an I will refer to things in terms of the underlying category, unless they have an
over-bar. So e.g. $\idToIso$ is a function in the underlying category and the over-bar. So e.g. $\idToIso$ is a function in the underlying category and the
corresponding thing is denoted $\wideoverbar{\idToIso}$ in the opposite corresponding thing is denoted $\wideoverbar{\idToIso}$ in the opposite
category. category.
@ -613,9 +612,9 @@ $$
\prod_{\bC \tp \Category} \left(\bC^{\var{Op}}\right)^{\var{Op}} \equiv \bC \prod_{\bC \tp \Category} \left(\bC^{\var{Op}}\right)^{\var{Op}} \equiv \bC
$$ $$
% %
As we've seen the laws in $\left(\bC^{\var{Op}}\right)^{\var{Op}}$ get quite As we have seen the laws in $\left(\bC^{\var{Op}}\right)^{\var{Op}}$ get quite
involved.\footnote{We haven't even seen the full story because we've used this involved.\footnote{We have not even seen the full story because we have used
`interface' for equivalences.} Luckily since being-a-category is a mere this `interface' for equivalences.} Luckily since being-a-category is a mere
proposition, we need not concern ourselves with this bit when proving the above. proposition, we need not concern ourselves with this bit when proving the above.
We can use the equality principle for categories that let us prove an equality We can use the equality principle for categories that let us prove an equality
just by giving an equality on the data-part. So, given a category $\bC$ all we just by giving an equality on the data-part. So, given a category $\bC$ all we
@ -794,8 +793,9 @@ is later extended to talk about higher categories.
\section{Products} \section{Products}
\label{sec:products} \label{sec:products}
In the following I'll demonstrate a technique for using categories to prove In the following a technique for using categories to prove properties will be
properties. The goal in this section is to show that products are propositions: demonstrated. The goal in this section is to show that products are
propositions:
% %
$$ $$
\prod_{\bC \tp \Category} \prod_{A\;B \tp \Object} \isProp\ (\var{Product}\ \bC\ A\ B) \prod_{\bC \tp \Category} \prod_{A\;B \tp \Object} \isProp\ (\var{Product}\ \bC\ A\ B)
@ -806,7 +806,7 @@ and $B$ in the category $\bC$. I do this by constructing a category whose
terminal objects are equivalent to products in $\bC$, and since terminal objects terminal objects are equivalent to products in $\bC$, and since terminal objects
are propositional in a proper category and equivalences preserve homotopy level, are propositional in a proper category and equivalences preserve homotopy level,
then we know that products also are propositions. But before we get to that, then we know that products also are propositions. But before we get to that,
let's recall the definition of products. we recall the definition of products.
\subsection{Definition of products} \subsection{Definition of products}
Given a category $\bC$ and two objects $A$ and $B$ in $\bC$ we define the Given a category $\bC$ and two objects $A$ and $B$ in $\bC$ we define the
@ -1080,8 +1080,8 @@ equality principle for arrows in this category (\ref{eq:productEqPrinc}) gives
us that it suffices to show that $f$ and $\inv{f}$, this is exactly us that it suffices to show that $f$ and $\inv{f}$, this is exactly
$\var{inv}_f$. $\var{inv}_f$.
This concludes the first direction of the isomorphism that we're constructing. This concludes the first direction of the isomorphism that we are constructing.
For the other direction we're given just given the isomorphism For the other direction we are given the isomorphism:
% %
$$ $$
(f, \inv{f}, \var{inv}_f) (f, \inv{f}, \var{inv}_f)
@ -1151,7 +1151,7 @@ gory details.
% %
\subsection{Propositionality of products} \subsection{Propositionality of products}
% %
Now that we've constructed the ``pair category'' I'll demonstrate how to use Now that we have constructed the ``pair category'' I will demonstrate how to use
this to prove that products are propositional. I will do this by showing that this to prove that products are propositional. I will do this by showing that
terminal objects in this category are equivalent to products: terminal objects in this category are equivalent to products:
% %
@ -1162,7 +1162,7 @@ terminal objects in this category are equivalent to products:
And as always we do this by constructing an isomorphism: And as always we do this by constructing an isomorphism:
% %
In the direction $\var{Terminal} → \var{Product}\ ℂ\ \mathcal{A}\ \mathcal{B}$ In the direction $\var{Terminal} → \var{Product}\ ℂ\ \mathcal{A}\ \mathcal{B}$
we're given a terminal object $X, x_𝒜, x_ℬ$. $X$ Will be the product-object and we are given a terminal object $X, x_𝒜, x_ℬ$. $X$ Will be the product-object and
$x_𝒜, x_ℬ$ will be the product arrows, so it just remains to verify that this is $x_𝒜, x_ℬ$ will be the product arrows, so it just remains to verify that this is
indeed a product. That is, for an object $Y$ and two arrows $y_𝒜 \tp indeed a product. That is, for an object $Y$ and two arrows $y_𝒜 \tp
\Arrow\ Y\ 𝒜$, $y_ℬ\ \Arrow\ Y\ ℬ$ we must find a unique arrow $f \tp \Arrow\ Y\ 𝒜$, $y_ℬ\ \Arrow\ Y\ ℬ$ we must find a unique arrow $f \tp

4
doc/introduction.tex
View file

@ -30,7 +30,7 @@ Consider the functions:
\end{multicols} \end{multicols}
% %
$n + 0$ is \nomen{definitionally} equal to $n$, which we write as $n + 0 = n$. $n + 0$ is \nomen{definitionally} equal to $n$, which we write as $n + 0 = n$.
This is also called \nomen{judgmental} equality. We call it definitional This is also \called \nomen{judgmental} equality. We call it definitional
equality because the \emph{equality} arises from the \emph{definition} of $+$ equality because the \emph{equality} arises from the \emph{definition} of $+$
which is: which is:
% %
@ -56,7 +56,7 @@ 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{point-wise 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 its 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
show that representable functors are indeed functors. The representable functor show that representable functors are indeed functors. The representable functor

2
doc/sources.tex
View file

@ -3,7 +3,7 @@
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
implementation. Rather, this is a redacted and pre-formatted designed for 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. Its 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.
\section{Cubical} \section{Cubical}