Changes based on Pierre's suggestions
This commit is contained in:
parent
2b0dfe4984
commit
179570edf0
148
doc/cubical.tex
148
doc/cubical.tex
|
|
@ -1,17 +1,18 @@
|
|||
\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
|
||||
Judgmental equality in Agda is a feature of the type-system. It's something that
|
||||
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
|
||||
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.
|
||||
On the other hand, propositional equality is something defined within the
|
||||
language itself. Propositional equality cannot be derived automatically. The
|
||||
normal definition of judgmental equality is an inductive data-type. Cubical Agda
|
||||
discards this type in favor of a new primitives that has certain computational
|
||||
properties exclusive to it.
|
||||
|
||||
Exceprts of the source code relevant to this section can be found in appendix
|
||||
\ref{sec:app-cubical}.
|
||||
\S\ref{sec:app-cubical}.
|
||||
|
||||
\subsection{The equality type}
|
||||
The usual notion of judgmental equality says that given a type $A \tp \MCU$ and
|
||||
|
|
@ -21,7 +22,8 @@ two points of $A$; $a_0, a_1 \tp A$ we can form the type:
|
|||
a_0 \equiv a_1 \tp \MCU
|
||||
\end{align}
|
||||
%
|
||||
In Agda this is defined as an inductive data-type with the single constructor:
|
||||
In Agda this is defined as an inductive data-type with the single constructor
|
||||
for any $a \tp A$:
|
||||
%
|
||||
\begin{align}
|
||||
\refl \tp a \equiv a
|
||||
|
|
@ -29,7 +31,7 @@ In Agda this is defined as an inductive data-type with the single constructor:
|
|||
%
|
||||
For any $a \tp A$.
|
||||
|
||||
There also exist a related notion of \emph{heterogeneous} equality where allows
|
||||
There also exist a related notion of \emph{heterogeneous} equality which 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:
|
||||
%
|
||||
|
|
@ -37,7 +39,8 @@ for equating points of different types. In this case given two types $A, B \tp
|
|||
a \cong b \tp \MCU
|
||||
\end{align}
|
||||
%
|
||||
This is likewise defined as an inductive data-type with a single constructors:
|
||||
This is likewise defined as an inductive data-type with a single constructors
|
||||
for any $a \tp A$:
|
||||
%
|
||||
\begin{align}
|
||||
\refl \tp a \cong a
|
||||
|
|
@ -47,11 +50,11 @@ 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:
|
||||
Judgmental equality in Cubical Agda is encapsulated with the type:
|
||||
%
|
||||
$$
|
||||
\begin{equation}
|
||||
\Path \tp (P \tp I → \MCU) → P\ 0 → P\ 1 → \MCU
|
||||
$$
|
||||
\end{equation}
|
||||
%
|
||||
$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
|
||||
|
|
@ -62,11 +65,11 @@ 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 theory. 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:
|
||||
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
|
||||
p \tp \prod_{i \tp I} P\ i
|
||||
$$
|
||||
%
|
||||
Which must satisfy being judgmentally equal to $a_0$ (respectively $a_1$) at the
|
||||
|
|
@ -77,16 +80,16 @@ endpoints. I.e.:
|
|||
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:
|
||||
The notion of ``homogeneous equalities'' is recovered when $P$ does not 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
|
||||
$a \equiv b$ when talking about non-dependent paths and use the notation
|
||||
$\Path\ (\lambda i \to P\ i)\ a\ b$ when the path-space is of particular
|
||||
interest.
|
||||
|
||||
With this definition we can also recover reflexivity. That is, for any $A \tp
|
||||
|
|
@ -99,28 +102,63 @@ With this definition we can also recover reflexivity. That is, for any $A \tp
|
|||
\end{aligned}
|
||||
\end{equation}
|
||||
%
|
||||
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$.
|
||||
Here the path-space is $P \defeq \lambda i \to A$ and it satsifies $P\ i = A$
|
||||
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;
|
||||
i.e. the path that stays 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.}
|
||||
It's also surpisingly easy to show functional extensionality with which we can
|
||||
construct a path between $f$ and $g$ -- the function defined in the introduction
|
||||
(section \S\ref{sec:functional-extensionality}).
|
||||
%% module _ {ℓa ℓb} {A : Set ℓa} {B : A → Set ℓb} where
|
||||
%% funExt : {f g : (x : A) → B x} → ((x : A) → f x ≡ g x) → f ≡ g
|
||||
Functional extensionality is the proposition, given a type $A \tp \MCU$, a
|
||||
family of types $B \tp A \to \MCU$ and functions $f, g \tp \prod_{a \tp A}
|
||||
B\ a$:
|
||||
%
|
||||
\begin{equation}
|
||||
\label{eq:funExt}
|
||||
\var{funExt} \tp \prod_{a \tp A} f\ a \equiv g\ a \to f \equiv g
|
||||
\end{equation}
|
||||
%
|
||||
%% p = λ i a → p a i
|
||||
So given $p \tp \prod_{a \tp A} f\ a \equiv g\ a$ we must give a path $f \equiv
|
||||
g$. That is a function $I \to \prod_{a \tp A} B\ a$. So let $i \tp I$ be given.
|
||||
We must now give an expression $\phi \tp \prod_{a \tp A} B\ a$ satisfying
|
||||
$\phi\ 0 \equiv f\ a$ and $\phi\ 1 \equiv g\ a$. This neccesitates that the
|
||||
expression must be a lambda-abstraction, so let $a \tp A$ be given. Now we can
|
||||
apply $a$ to $p$ and get the path $p\ a \tp f\ a \equiv g\ a$. And this exactly
|
||||
satisfied the conditions for $\phi$. In conclustion \ref{eq:funExt} is inhabited
|
||||
by the term:
|
||||
%
|
||||
\begin{equation}
|
||||
\label{eq:funExt}
|
||||
\var{funExt}\ p \defeq λ i\ a → p\ a\ i
|
||||
\end{equation}
|
||||
%
|
||||
With this we can now prove the desired equality $f \equiv g$ from section
|
||||
\S\ref{sec:functional-extensionality}:
|
||||
%
|
||||
\begin{align*}
|
||||
p & \tp f \equiv g \\
|
||||
p & \defeq \var{funExt}\ \lambda n \to \refl
|
||||
\end{align*}
|
||||
%
|
||||
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:
|
||||
don't have any interesting structure. This is referred to as Uniqueness of
|
||||
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
|
||||
increasing amount of homotopic structure. At the bottom of this hierarchy we
|
||||
have the set of contractible types:
|
||||
%
|
||||
\begin{equation}
|
||||
\begin{aligned}
|
||||
%% \begin{split}
|
||||
& \isContr && \tp \MCU \to \MCU \\
|
||||
& \isContr && \tp \MCU \to \MCU \\
|
||||
& \isContr\ A && \defeq \sum_{c \tp A} \prod_{a \tp A} a \equiv c
|
||||
%% \end{split}
|
||||
\end{aligned}
|
||||
|
|
@ -128,8 +166,14 @@ types:
|
|||
%
|
||||
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$.
|
||||
be thought of as ``the true proposition $A$''. And indeed $\top$ is
|
||||
contractible:
|
||||
\begin{equation*}
|
||||
\var{tt} , \lambda x \to \refl \tp \isContr\ \top
|
||||
\end{equation*}
|
||||
%
|
||||
It is a theorem that if a type is contractible, then it is isomorphic to the
|
||||
unit-type.
|
||||
|
||||
The next step in the hierarchy is the set of mere propositions:
|
||||
%
|
||||
|
|
@ -140,10 +184,18 @@ The next step in the hierarchy is the set of mere propositions:
|
|||
\end{aligned}
|
||||
\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!!}
|
||||
$\isProp\ A$ can be thought of as the set of true and false propositions. And
|
||||
indeed both $\top$ and $\bot$ are propositions:
|
||||
%
|
||||
\begin{align*}
|
||||
λ \var{tt}\ \var{tt} → refl & \tp \isProp\ ⊤ \\
|
||||
λ\varnothing\ \varnothing & \tp \isProp\ ⊥
|
||||
\end{align*}
|
||||
%
|
||||
I've used $\varnothing$ here to denote an impossible pattern. It is a theorem
|
||||
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$.
|
||||
|
|
@ -157,10 +209,13 @@ Then comes the set of homotopical sets:
|
|||
\end{aligned}
|
||||
\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.
|
||||
I won't give an example of a set at this point. It turns out that proving e.g.
|
||||
$\isProp\ \bN$ is not so straight-forward (see \S3.1.4 in \ref{hott-2013}).
|
||||
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
|
||||
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
|
||||
a proposition.
|
||||
|
||||
The next step in the hierarchy is, as the reader might've guessed, the type:
|
||||
%
|
||||
|
|
@ -219,10 +274,13 @@ $$
|
|||
%
|
||||
We have the function:
|
||||
%
|
||||
$$
|
||||
\begin{equation}
|
||||
\pathJ\ P\ p \tp \prod_{a' \tp A} \prod_{p \tp a ≡ a'} P\ a\ p
|
||||
$$
|
||||
\end{equation}
|
||||
%
|
||||
I will not give an example of using $\pathJ$ here. But we'll see an application
|
||||
of it in \ref{eq:pathJ-example}.
|
||||
|
||||
\subsection{Paths over propositions}
|
||||
\label{sec:lemPropF}
|
||||
Another very useful combinator is $\lemPropF$:
|
||||
|
|
|
|||
|
|
@ -26,7 +26,7 @@ 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
|
||||
The introduction (section \S\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
|
||||
|
|
|
|||
|
|
@ -53,9 +53,15 @@ given type.
|
|||
For the rest of this chapter I will present some of these results. For didactic
|
||||
reasons no source-code has been included in this chapter. To see the formal
|
||||
definitions excerpts of the implementation have been included in appendix
|
||||
\ref{ch:app-sources}.
|
||||
\S\ref{ch:app-sources}:
|
||||
Appendix
|
||||
\S\ref{sec:app-categories} corresponds to section \S\ref{sec:categories},
|
||||
appendix \S\ref{sec:app-products} to section \S\ref{sec:products}
|
||||
and appendix \S\ref{sec:app-monads} to section \S\ref{sec:monads}.
|
||||
|
||||
|
||||
\section{Categories}
|
||||
\label{sec:categories}
|
||||
The data for a category consist of a type for the sort of objects; a type for
|
||||
the sort of arrows; an identity arrow and a composition operation for arrows.
|
||||
Another record encapsulates some laws about this data: associativity of
|
||||
|
|
@ -85,9 +91,9 @@ definitions: If we let $p$ be a witness to the identity law, which formally is:
|
|||
Then we can construct the identity isomorphism $\var{idIso} \tp \identity,
|
||||
\identity, p \tp A \approxeq A$ for any object $A$. Here $\approxeq$ denotes
|
||||
isomorphism on objects (whereas $\cong$ denotes isomorphism of types). This will
|
||||
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
|
||||
\emph{any} path:
|
||||
be elaborated further on in sections \S\ref{sec:equiv} and
|
||||
\S\ref{sec:univalence}. Moreover, due to substitution for paths we can construct
|
||||
an isomorphism from \emph{any} path:
|
||||
%
|
||||
\begin{equation}
|
||||
\var{idToIso} \tp A ≡ B → A ≊ B
|
||||
|
|
@ -106,14 +112,14 @@ Note that \ref{eq:cat-univ} is \emph{not} the same as:
|
|||
%
|
||||
\begin{equation}
|
||||
\label{eq:cat-univalence}
|
||||
\tag{Univalence, category}
|
||||
%% \tag{Univalence, category}
|
||||
(A \equiv B) \simeq (A \approxeq B)
|
||||
\end{equation}
|
||||
%
|
||||
However the two are logically equivalent: 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 and will be discussed in
|
||||
section \ref{sec:univalence}.
|
||||
section \S\ref{sec:univalence}.
|
||||
|
||||
In summary, the definition of a category is the following collection of data:
|
||||
%
|
||||
|
|
@ -127,14 +133,14 @@ In summary, the definition of a category is the following collection of data:
|
|||
And laws:
|
||||
%
|
||||
\begin{align}
|
||||
\tag{associativity}
|
||||
%% \tag{associativity}
|
||||
h \lll (g \lll f) ≡ (h \lll g) \lll f \\
|
||||
\tag{identity}
|
||||
%% \tag{identity}
|
||||
\identity \lll f ≡ f \x
|
||||
f \lll \identity ≡ f
|
||||
\\
|
||||
\label{eq:arrows-are-sets}
|
||||
\tag{arrows are sets}
|
||||
%% \tag{arrows are sets}
|
||||
\isSet\ (\Arrow\ A\ B)\\
|
||||
\tag{\ref{eq:cat-univ}}
|
||||
\isEquiv\ (A \equiv B)\ (A \approxeq B)\ \idToIso
|
||||
|
|
@ -159,7 +165,7 @@ Proving that \ref{eq:identity} is a mere proposition:
|
|||
%
|
||||
There are multiple ways to prove this. Perhaps one of the more intuitive proofs
|
||||
is by way of the `combinators' $\propPi$ and $\propSig$ presented in sections
|
||||
\ref{sec:propPi} and \ref{sec:propSig}:
|
||||
\S\ref{sec:propPi} and \S\ref{sec:propSig}:
|
||||
%
|
||||
\begin{align*}
|
||||
\var{propPi} & \tp \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\prod_{a \tp A} P\ a\right)
|
||||
|
|
@ -279,7 +285,7 @@ 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 because $\isProp$ talks about non-dependent paths. So we need to
|
||||
'promote' the result that univalence is a proposition to a heterogeneous path.
|
||||
To this end we can use $\lemPropF$, which was introduced in \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 = \var{Univalent}$. We've
|
||||
shown that being a category is a proposition, a result that holds for any choice
|
||||
|
|
@ -476,33 +482,43 @@ what we're trying to prove but talks about paths rather than isomorphisms:
|
|||
\end{equation}
|
||||
%
|
||||
Again $p_{\var{dom}}$ denotes the path $\var{Arrow}\ A\ X \equiv
|
||||
\var{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 \var{Object}$, so let $\widetilde{B} \tp \Object$ and $\widetilde{p} \tp
|
||||
A \equiv \widetilde{B}$ be given. The family that we perform induction over will
|
||||
\var{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 \var{Object}$ Let $\widetilde{B} \tp \Object$ and $\widetilde{p} \tp A
|
||||
\equiv \widetilde{B}$ be given. The family that we perform induction over will
|
||||
be:
|
||||
%
|
||||
$$
|
||||
\var{coe}\ {\widetilde{p}}^*\ f
|
||||
\begin{align}
|
||||
D\ \widetilde{B}\ \widetilde{p} \defeq
|
||||
%% \prod_{\widetilde{B} \tp \Object}
|
||||
%% \prod_{\widetilde{p} \tp A \equiv \widetilde{B}}
|
||||
\var{coe}\ {\widetilde{p}}^*\ f
|
||||
\equiv
|
||||
f \lll \inv{(\var{idToIso}\ \widetilde{p})}
|
||||
$$
|
||||
The base-case therefore becomes:
|
||||
\end{align}
|
||||
The base-case therefore becomes
|
||||
$d \tp \var{coe}\ \refl^*\ f \equiv f \lll \inv{(\var{idToIso}\ \refl)}$
|
||||
and is inhabited by:
|
||||
\begin{align*}
|
||||
\var{coe}\ {\widetilde{\refl}}^*\ f
|
||||
& \equiv f \\
|
||||
\var{coe}\ \refl^*\ f
|
||||
& \equiv f
|
||||
&& \text{$\refl$ is a neutral element for $\var{coe}$}\\
|
||||
& \equiv f \lll \var{identity} \\
|
||||
& \equiv f \lll \inv{(\var{idToIso}\ \widetilde{\refl})}
|
||||
& \equiv f \lll \var{subst}\ \var{refl}\ \var{identity}
|
||||
&& \text{$\refl$ is a neutral element for $\var{subst}$}\\
|
||||
& \equiv f \lll \inv{(\var{idToIso}\ \refl)}
|
||||
&& \text{By definition of $\var{idToIso}$}\\
|
||||
\end{align*}
|
||||
%
|
||||
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
|
||||
with the fact that $\var{idToIso}$ is constructed by substituting according to
|
||||
the supplied path and since reflexivity is also the neutral element for
|
||||
substitutions we arrive at the desired expression. To close the
|
||||
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.
|
||||
|
||||
To close the 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.
|
||||
In summary the proof of \ref{eq:coeDomIso} is the term:
|
||||
%
|
||||
\begin{equation}
|
||||
\label{eq:pathJ-example}
|
||||
\var{pathJ}\ D\ d\ B\ p
|
||||
\end{equation}
|
||||
%
|
||||
And this finishes the proof of \ref{eq:coeDomIso} and thus \ref{eq:coeDom}.
|
||||
%
|
||||
\section{Categories}
|
||||
|
|
@ -546,7 +562,7 @@ arguments. Or in other words; since $\Arrow\ A\ B$ is a set for all $A\;B \tp
|
|||
\Object$ then so is $Arrow\ B\ A$.
|
||||
|
||||
Now, to show that this category is univalent is not as straight-forward. Luckily
|
||||
section \ref{sec:equiv} gave us some tools to work with equivalences. We saw
|
||||
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
|
||||
$\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
|
||||
|
|
@ -635,7 +651,7 @@ $$
|
|||
(\var{hA} \equiv \var{hB}) \simeq (\var{hA} \approxeq \var{hB})
|
||||
$$
|
||||
%
|
||||
Which, as we saw in section \ref{sec:univalence}, is sufficient to show that the
|
||||
Which, as we saw in section \S\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:
|
||||
|
|
@ -721,7 +737,7 @@ choose:
|
|||
& \tp \var{Isomorphism}\ f \to \isEquiv\ f
|
||||
\end{align*}
|
||||
%
|
||||
As mentioned in section \ref{sec:equiv}. These maps are not in general inverses
|
||||
As mentioned in section \S\ref{sec:equiv}. These maps are not in general inverses
|
||||
of each other. In stead, we will use the fact that $A$ and $B$ are sets. The first thing we must prove is:
|
||||
%
|
||||
\begin{align*}
|
||||
|
|
@ -777,6 +793,7 @@ where we have a witness to this being a category. This is useful if this library
|
|||
is later extended to talk about higher categories.
|
||||
|
||||
\section{Products}
|
||||
\label{sec:products}
|
||||
In the following I'll demonstrate a technique for using categories to prove
|
||||
properties. The goal in this section is to show that products are propositions:
|
||||
%
|
||||
|
|
@ -1214,6 +1231,7 @@ That in any category:
|
|||
\end{align}
|
||||
%
|
||||
\section{Monads}
|
||||
\label{sec:monads}
|
||||
In this section I present two formulations of monads. The two representations
|
||||
are referred to as the monoidal- and Kleisli- representation respectively or
|
||||
simply monoidal monads and Kleisli monads for short. We then show that the two
|
||||
|
|
|
|||
|
|
@ -16,6 +16,7 @@ In the following two sections I present two examples that illustrate some
|
|||
limitations inherent in ITT and -- by extension -- Agda.
|
||||
%
|
||||
\subsection{Functional extensionality}
|
||||
\label{sec:functional-extensionality}
|
||||
Consider the functions:
|
||||
%
|
||||
\begin{multicols}{2}
|
||||
|
|
@ -92,7 +93,7 @@ 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
|
||||
in section \ref{sec:equiv}, but for now it is sufficient to think of an
|
||||
in section \S\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:
|
||||
%
|
||||
|
|
|
|||
|
|
@ -31,7 +31,7 @@
|
|||
\resizebox{\@tempdima}{\height}{=}%
|
||||
}
|
||||
\makeatother
|
||||
\newcommand{\var}[1]{\ensuremath{\mathit{#1}}}
|
||||
\newcommand{\var}[1]{\ensuremath{\mathit{#1}}\index{#1}}
|
||||
\newcommand{\Hom}{\var{Hom}}
|
||||
\newcommand{\fmap}{\var{fmap}}
|
||||
\newcommand{\bind}{\var{bind}}
|
||||
|
|
@ -86,3 +86,4 @@
|
|||
\newcommand\NT[2]{\NTsym\ #1\ #2}
|
||||
\newcommand\Endo[1]{\var{Endo}\ #1}
|
||||
\newcommand\EndoR{\mathcal{R}}
|
||||
\newcommand\funExt{\var{funExt}}
|
||||
|
|
|
|||
|
|
@ -68,6 +68,7 @@
|
|||
\nocite{coquand-2013}
|
||||
|
||||
\bibliography{refs}
|
||||
%% \printindex
|
||||
\begin{appendices}
|
||||
\setcounter{page}{1}
|
||||
\pagenumbering{roman}
|
||||
|
|
|
|||
|
|
@ -16,7 +16,8 @@
|
|||
\usepackage[toc,page]{appendix}
|
||||
\usepackage{xspace}
|
||||
\usepackage[a4paper]{geometry}
|
||||
|
||||
\usepackage{makeidx}
|
||||
\makeindex
|
||||
% \setlength{\parskip}{10pt}
|
||||
|
||||
% \usepackage{tikz}
|
||||
|
|
|
|||
|
|
@ -10,6 +10,7 @@ those.
|
|||
\section{Cubical}
|
||||
\label{sec:app-cubical}
|
||||
\begin{figure}[h]
|
||||
\label{fig:path}
|
||||
\begin{Verbatim}
|
||||
postulate
|
||||
PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ
|
||||
|
|
|
|||
Loading…
Reference in a new issue