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

Final touch-up on report and acknowledgments

This commit is contained in:
Frederik Hanghøj Iversen 2018-05-29 15:09:38 +02:00
parent b992d5a7f2
commit 37a675a84f
5 changed files with 715 additions and 676 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
doc/acknowledgement.tex Normal file
View File

@ -0,0 +1 @@
\chapter*{Acknowledgements}

50
doc/conclusion.tex
View File

@ -3,34 +3,34 @@ This thesis highlighted some issues with the standard inductive
definition of propositional equality used in Agda. Functional
extensionality and univalence are examples of two propositions not
admissible in Intensional Type Theory (ITT). This has a big impact on
what is provable and the reusability of proofs. This issue is overcome
with an extension to Agda's type system called Cubical Agda. With
Cubical Agda both functional extensionality and univalence are
what is provable and the reusability of proofs. This issue is
overcome with an extension to Agda's type system called Cubical Agda.
With Cubical Agda both functional extensionality and univalence are
admissible. Cubical Agda is more expressive, but there are certain
issues that arise that are not present in standard Agda. For one thing
Agda enjoys Uniqueness of Identity Proofs (UIP) though a flag exists
to turn this off, which is the case in Cubical Agda. In stead
there exists a hierarchy of types with increasing \nomen{homotopical
issues that arise that are not present in standard Agda. For one
thing Agda enjoys Uniqueness of Identity Proofs (UIP) though a flag
exists to turn this off. This feature is not present in Cubical Agda.
Rather than having unique identity proofs cubical Agda gives rise to a
hierarchy of types with increasing \nomen{homotopical
structure}{homotopy levels}. It turns out to be useful to built the
formalization with this hierarchy in mind as it can simplify proofs
considerably. Another issue one must overcome in Cubical Agda is when
a type has a field whose type depends on a previous field. In this
case paths between such types will be heterogeneous paths. This
problem is related to Cubical Agda not having the K-rule. In practice
it turns out to be considerably more difficult to work heterogeneous
paths than with homogeneous paths. The thesis demonstrated some
techniques to overcome these difficulties, such as based
path-induction.
case paths between such types will be heterogeneous paths. In
practice it turns out to be considerably more difficult to work with
heterogeneous paths than with homogeneous paths. The thesis
demonstrated the application of some techniques to overcome these
difficulties, such as based path induction.
This thesis formalized some of the core concepts from category theory
This thesis formalizes some of the core concepts from category theory
including; categories, functors, products, exponentials, Cartesian
closed categories, natural transformations, the yoneda embedding,
monads and more. Category theory is an interesting case-study for the
application of Cubical Agda for two reasons in particular: Because
monads and more. Category theory is an interesting case study for the
application of cubical Agda for two reasons in particular: Because
category theory is the study of abstract algebra of functions, meaning
that functional extensionality is particularly relevant. Another
reason is that in category theory it is commonplace to identify
isomorphic structures and univalence allows for making this notion
isomorphic structures. Univalence allows for making this notion
precise. This thesis also demonstrated another technique that is
common in category theory; namely to define categories to prove
properties of other structures. Specifically a category was defined
@ -40,14 +40,14 @@ and proved that they indeed are equivalent: Namely monads in the
monoidal- and Kleisli- form. The monoidal formulation is more typical
to category theoretic formulations and the Kleisli formulation will be
more familiar to functional programmers. It would have been very
difficult to make a similar proof with setoids. In the formulation we
also saw how paths can be used to extract functions. A path between
two types induce an isomorphism between the two types. This
e.g. permits developers to write a monad instance for a given type
using the Kleisli formulation. By transporting along the path between
the monoidal- and Kleisli- formulation one can reuse all the
operations and results shown for monoidal- monads in the context of
kleisli monads.
difficult to make a similar proof with setoids and the proof would be
very difficult to read. In the formulation we also saw how paths can
be used to extract functions. A path between two types induce an
isomorphism between the two types. This e.g.\ permits developers to
write a monad instance for a given type using the Kleisli formulation.
By transporting along the path between the monoidal- and Kleisli-
formulation one can reuse all the operations and results shown for
monoidal- monads in the context of kleisli monads.
%%
%% problem with inductive type
%% overcome with cubical

97
doc/discussion.tex
View File

@ -16,41 +16,43 @@ interesting result of this development is how much this influenced the
development. In particular having a functional extensionality that
``computes'' should simplify some proofs.
I have tested this theory by using a feature of Agda where one can
mark certain bindings as being \emph{abstract}. This means that the
type-checker will not try to reduce that term further when
type-checking is performed. I tried making univalence and functional
extensionality abstract. It turns out that the conversion behaviour of
univalence is not used anywhere. For functional extensionality there
are two places in the whole solution where the reduction behaviour is
used to simplify some proofs. This is in showing that the maps between
the two formulations of monads are inverses. See the notes in this
I have tested this by using a feature of Agda where one can mark
certain bindings as being \emph{abstract}. This means that the
type-checker will not try to reduce that term further during type
checking. I tried making univalence and functional extensionality
abstract. It turns out that the conversion behaviour of univalence is
not used anywhere. For functional extensionality there are two places
in the whole solution where the reduction behaviour is used to
simplify some proofs. This is in showing that the maps between the
two formulations of monads are inverses. See the notes in this
module:
%
\begin{center}
\sourcelink{Cat.Category.Monad.Voevodsky}
\end{center}
%
I've also put this in a source listing in \ref{app:abstract-funext}. I
will not reproduce it in full here as the type is quite involved. The
method used to find in what places the computational behaviour of
these proofs are needed has the caveat of only working for places that
directly or transitively uses these two proofs. Fortunately though the
code is structured in such a way that this should be the case.
Nonetheless it is quite surprising that this computational behaviours
is not used more widely in the formalization.
Barring this, however, the computational behaviour of paths can still
be useful. E.g. if a programmer want's to reuse functions that operate
on a monoidal monads to work with a monad in the Kleisli form that
this programmer has specified. To make this idea concrete, say we are
I will not reproduce it in full here as the type is quite involved. In
stead I have put this in a source listing in \ref{app:abstract-funext}.
The method used to find in what places the computational behaviour of
these proofs are needed has the caveat of only working for places that
directly or transitively uses these two proofs. Fortunately though
the code is structured in such a way that this is the case. So in
conclusion the way I have structured these proofs means that the
computational behaviour of functional extensionality and univalence
has not been so relevant.
Barring this the computational behaviour of paths can still be useful.
E.g.\ if a programmer wants to reuse functions that operate on a
monoidal monads to work with a monad in the Kleisli form that the
programmer has specified. To make this idea concrete, say we are
given some function $f \tp \Kleisli \to T$ having a path between $p
\tp \Monoidal \equiv \Kleisli$ induces a map $\coe\ p \tp \Monoidal
\to \Kleisli$. We can compose $f$ with this map to get $f \comp
\coe\ p \tp \Monoidal \to T$. Of course, since that map was
constructed with an isomorphism these maps already exist and could be
used directly. So this is arguably only interesting when one wants to
prove properties of such functions.
used directly. So this is arguably only interesting when one also
wants to prove properties of applying such functions.
\subsection{Reusability of proofs}
The previous example illustrate how univalence unifies two otherwise
@ -68,18 +70,18 @@ course generalizes to any family $P \tp 𝒰 → 𝒰$ where $P$ is inhabited
at either formulation (i.e.\ either $P\ \Monoidal$ or $P\ \Kleisli$
holds).
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 interesting place where this becomes
apparent is in interfacing with the Agda standard library. Multiple
definitions in the Agda standard library have been designed with the
setoid-interpretation in mind. E.g. the notion of ``unique
existential'' is indexed by a relation that should play the role of
propositional equality. Likewise for equivalence relations, they are
indexed, not only by the actual equivalence relation, but also by
another relation that serve as propositional equality.
The introduction (section \S\ref{sec:context}) mentioned that a
typical way of getting access to functional extensionality is to work
with setoids. Nowhere in this formalization has this been necessary,
$\Path$ has been used globally in the project for propositional
equality. One interesting place where this becomes apparent is in
interfacing with the Agda standard library. Multiple definitions in
the Agda standard library have been designed with the
setoid-interpretation in mind. E.g.\ the notion of \emph{unique
existential} is indexed by a relation that should play the role of
propositional equality. Equivalence relations are likewise indexed,
not only by the actual equivalence relation but also by another
relation that serve as propositional equality.
%% Unfortunately we cannot use the definition of equivalences found in
%% the standard library to do equational reasoning directly. The
%% reason for this is that the equivalence relation defined there must
@ -89,14 +91,12 @@ In the formalization at present a significant amount of energy has
been put towards proving things that would not have been needed in
classical Agda. The proofs that some given type is a proposition were
provided as a strategy to simplify some otherwise very complicated
proofs (e.g. \ref{eq:proof-prop-IsPreCategory}
proofs (e.g.\ \ref{eq:proof-prop-IsPreCategory}
and \ref{eq:productPath}). Often these proofs would not be this
complicated. If the J-rule holds definitionally the proof-assistant
can help simplify these goals considerably. The lack of the J-rule has
a significant impact on the complexity of these kinds of proofs.
\TODO{Universe levels.}
\subsection{Motifs}
An oft-used technique in this development is using based path
induction to prove certain properties. One particular challenge that
@ -121,20 +121,19 @@ This means that even though the path-type gives us a computational
interpretation of functional extensionality, univalence, transport,
etc., we do not have a way of actually using this to compile our
programs that use these primitives. It would be interesting to see
practical applications of this. The path between monads that this
library exposes could provide one particularly interesting case-study.
\subsection{Higher inductive types}
This library has not explored the usefulness of higher inductive types
in the context of Category Theory.
\subsection{Initiality conjecture}
A fellow student here at Chalmers, Andreas Källberg, is currently
working on proving the initiality conjecture\TODO{Citation}. He will
be using this library to do so.
practical applications of this.
\subsection{Proving laws of programs}
Another interesting thing would be to use the Kleisli formulation of
monads to prove properties of functional programs. The existence of
univalence will make it possible to re-use proofs stated in terms of
the monoidal formulation in this setting.
%% \subsection{Higher inductive types}
%% This library has not explored the usefulness of higher inductive types
%% in the context of Category Theory.
\subsection{Initiality conjecture}
A fellow student at Chalmers, Andreas Källberg, is currently working
on proving the initiality conjecture. He will be using this library
to do so.

485
doc/implementation.tex
View File

@ -182,10 +182,10 @@ f \lll \identity ≡ f
\isEquiv\ (A ≡ B)\ (A ≊ B)\ \idToIso
\end{align}
%
$\lll$ denotes arrow composition (right-to-left), and reverse function
composition (left-to-right, diagrammatic order) is denoted $\rrr$. The objects
($A$, $B$ and $C$) and arrow ($f$, $g$, $h$) are implicitly universally
quantified.
The function $\lll$ denotes arrow composition (right-to-left), and
reverse function composition (left-to-right, diagrammatic order) is
denoted $\rrr$. The objects ($A$, $B$ and $C$) and arrow ($f$, $g$,
$h$) are implicitly universally quantified.
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
@ -298,18 +298,17 @@ equalities at different levels. It is worth noting that proving this
theorem with the regular inductive equality type would already not be
possible, since we at least need functional
extensionality\index{functional extensionality} (the projections are
all $∏$-types). Assuming we had functional extensionality
available to us as an axiom, we would use functional extensionality
\TODO{in reverse?} to retrieve the equalities in $a$ and $b$,
pattern-match on them to see that they are both $\refl$ and then close
the proof with $\refl$. Of course this theorem is not so interesting
in the setting of ITT since we know a priori that equality proofs are
unique.
all $∏$-types). Assuming we had functional extensionality available to
us as an axiom, we would use functional extensionality to retrieve the
equalities in $a$ and $b$; pattern match on them to see that they are
both $\refl$ and then close the proof with $\refl$. Of course this
theorem is not so interesting in the setting of ITT since we know
a~priori that equality proofs are unique.
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
For instance when we want to show that $\IsCategory$ is a mere
proposition. The type $\IsCategory$ is a record with two fields, a
witness to being a pre-category and the univalence condition. Recall
witness of being a pre-category and the univalence condition. Recall
that the univalence condition is indexed by the 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 homogeneous:
@ -324,23 +323,33 @@ $$
\Path\ (\lambda\; i → (p\ i).Univalent)\ a.\isPreCategory\ b.\isPreCategory
$$
%
Which depends on the choice of $p$. 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 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 \S\ref{sec:lemPropF}.
This path depends on the choice of $p$. 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 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
\S\ref{sec:lemPropF}.
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
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
congruence of paths:
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 of identity proof so it will also
hold for the witness obtained at an arbitrary point along $p$. 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 congruence
of paths:
%
$$
\congruence\ \isIdentity\ p
$$
%
In summary the heterogeneous path is inhabited by:
%
$$
\var{lemPropF}\ \var{propUnivalent}\ (\var{cong}\ p.\var{isIdentity})
$$
%
And this finishes the proof that being-a-category is a mere proposition
(\ref{eq:propIsPreCategory}).
@ -403,9 +412,10 @@ The maps $\var{fromIso}$ and $\var{toIso}$ naturally extend to these maps:
\var{toIsomorphism} & \tp A ≃ B → A \cong B
\end{align}
%
Having this interface gives us both: a way to think rather abstractly about how
to work with equivalences and a way to use ad hoc definitions of equivalences.
The specific instantiation of $\isEquiv$ as defined in \cite{cubical-agda} is:
Having this interface gives us both a way to think rather abstractly
about how to work with equivalences and a way to use ad~hoc
definitions of equivalences. The specific instantiation of $\isEquiv$
as defined in \cite{cubical-agda} is:
%
$$
isEquiv\ f ≜ ∏_{b \tp B} \isContr\ (\fiber\ f\ b)
@ -468,14 +478,16 @@ $$
(A ≡ B) \cong (A ≊ B)
$$
%
That is, we must demonstrate that there is an isomorphism (on types) between
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
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 of all pre-category since morphisms in a category are not regular
functions -- in stead they can be thought of as a generalization hereof. The univalence criterion therefore is simply a way of restricting arrows
to behave similarly to maps.
That is, we must demonstrate that there is an isomorphism (on types)
between 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 therefore perhaps a bit more intuitive to
grasp the implications of. Of course univalence for types (which is a
theorem -- i.e.\ provably holds) does not imply univalence of all
pre-category since morphisms in a category are not regular functions
-- in stead they can be thought of as a generalization hereof. The
univalence criterion therefore is simply a way of restricting arrows
to behave like maps with respect to univalence.
I will now mention a few helpful theorems that follow from univalence that will
become useful later.
@ -491,14 +503,22 @@ $$
\isoToId \tp A ≊ B → A ≡ B
$$
%
The next few theorems are variations on theorem 9.1.9 from \cite{hott-2013}. Let
an isomorphism $A ≊ B$ in some category $\bC$ be given. Name the
isomorphism $\iota \tp A → B$ and its inverse $\inv{\iota} \tp B → A$.
Since $\bC$ is a category (and therefore univalent) the isomorphism induces a
path $p \tp A ≡ B$. From this equality we can get two further paths:
$p_{\var{dom}} \tp \Arrow\ A\ X ≡ \Arrow\ B\ X$ and
$p_{\var{cod}} \tp \Arrow\ X\ A ≡ \Arrow\ X\ B$. We
then have the following two theorems:
The next few theorems are variations on theorem 9.1.9 from
\cite{hott-2013}. Let an isomorphism $A ≊ B$ in some category $\bC$ be
given. Name the isomorphism $\iota \tp A → B$ and its inverse
$\inv{\iota} \tp B → A$. Since $\bC$ is a category (and therefore
univalent) the isomorphism induces a path
%
$$p \defeq \idToIso\ (\iota, \inv{\iota}, \dots) \tp A ≡ B$$
%
From this equality we can get two further paths:
%
\begin{align*}
p_{\var{dom}} & \tp \Arrow\ A\ X ≡ \Arrow\ B\ X \\
p_{\var{cod}} & \tp \Arrow\ X\ A ≡ \Arrow\ X\ B
\end{align*}
%
We then have the following two theorems:
%
\begin{align}
\label{eq:coeDom}
@ -514,54 +534,56 @@ I will give the proof of the first theorem here, the second one is analogous.
%
\begin{align*}
\var{coe}\ p_{\var{dom}}\ f
& ≡ f \lll \inv{(\idToIso\ p)} && \text{lemma} \\
& ≡ f \lll (\idToIso\ p)_2 && \text{lemma} \\
& ≡ f \lll \inv{\iota}
&& \text{$\idToIso$ and $\isoToId$ are inverses}\\
\end{align*}
%
In the second step we use the fact that $p$ is constructed from the isomorphism
$\iota$ -- $\inv{(\idToIso\ p)}$ denotes the map $B → A$ induced by the
isomorphism $\idToIso\ p \tp A \cong B$. The helper-lemma is similar to
what we are trying to prove but talks about paths rather than isomorphisms:
In the second step we use the fact that $p$ is constructed from the
isomorphism $\iota$. The subscript in term $(\idToIso\ p)_2$ is
intended to denote the inverse map $B → A$ from the isomorphism
$\idToIso\ p \tp A \cong B$. The helper-lemma is similar to what we
are trying to prove but talks about paths rather than isomorphisms:
%
\begin{equation}
\label{eq:coeDomIso}
∏_{f \tp \Arrow\ A\ B} ∏_{p \tp A ≡ B}
\var{coe}\ p_{\var{dom}}\ f ≡ f \lll \inv{(\idToIso\ p)}
\var{coe}\ p_{\var{dom}}\ f ≡ f \lll (\idToIso\ p)_{2}
\end{equation}
%
Again $p_{\var{dom}}$ denotes the path $\Arrow\ A\ X ≡
\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 \Object$ Let $\widetilde{B} \tp \Object$ and $\widetilde{p} \tp A
≡ \widetilde{B}$ be given. The family that we perform induction over will
be:
Again $p_{\var{dom}}$ denotes the path $\Arrow\ A\ X ≡ \Arrow\ B\ X$
induced by $p$. To prove this statement let $f$ and $p$ be given then
we invoke based path induction. The induction will be based at $A \tp
\Object$ Let $\widetilde{B} \tp \Object$ and $\widetilde{p} \tp A ≡
\widetilde{B}$ be given. The family that we perform induction over
will be:
%
\begin{align}
D\ \widetilde{B}\ \widetilde{p} ≜
%% ∏_{\widetilde{B} \tp \Object}
%% ∏_{\widetilde{p} \tp A ≡ \widetilde{B}}
\var{coe}\ {\widetilde{p}}^*\ f
\var{coe}\ {\widetilde{p}_{\var{dom}}}\ f
≡
f \lll \inv{(\idToIso\ \widetilde{p})}
f \lll (\idToIso\ \widetilde{p})_{2}
\end{align}
The base-case therefore becomes
$d \tp \var{coe}\ \refl^*\ f ≡ f \lll \inv{(\idToIso\ \refl)}$
$d \tp \var{coe}\ \refl_{\var{dom}}\ f ≡ f \lll (\idToIso\ \refl)_{2}$
and is inhabited by:
\begin{align*}
\var{coe}\ \refl^*\ f
\var{coe}\ \refl_{\var{dom}}\ f
& ≡ f
&& \text{$\refl$ is a neutral element for $\var{coe}$}\\
& ≡ f \lll \identity \\
& ≡ f \lll \var{subst}\ \refl\ \identity
&& \text{$\refl$ is a neutral element for $\var{subst}$}\\
& ≡ f \lll \inv{(\idToIso\ \refl)}
& = f \lll (\idToIso\ \refl)_{2}
&& \text{By definition of $\idToIso$}\\
\end{align*}
%
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 ≡ B$ which we have.
In summary the proof of \ref{eq:coeDomIso} is the term:
To close the based-path-induction we must supply the value ``at the
other end''. In this case this is simply $B \tp \Object$ and $p \tp A
≡ B$ which we have. In summary the proof of \ref{eq:coeDomIso} is the
term:
%
\begin{equation}
\label{eq:pathJ-example}
@ -619,12 +641,13 @@ B)$ is an isomorphism. Let us denote its inverse with $\isoToId \tp (A
≊ B) → (A ≡ B)$. If we squint we can see what we need is a way to
go between $\wideoverbar{≊}$ and $≊$.
An inhabitant of $A ≊ B$ is simply an arrow $f \tp \Arrow\ A\ B$
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
go in the opposite direction. I name these maps $\shufflef \tp (A ≊
B) → (A \wideoverbar{≊} B)$ and $\shufflef^{-1} \tp (A
\wideoverbar{≊} B) → (A ≊ B)$ respectively.
An inhabitant of $A ≊ B$ is simply an arrow $f \tp \Arrow\ A\ B$ and
its inverse $g \tp \Arrow\ B\ A$ (and a witness to them being
inverses). In the opposite category $g$ will play the role of the
isomorphism and $f$ will be the inverse. Similarly we can go in the
opposite direction. I name these maps $\shufflef \tp (A ≊ B) → (A
\wideoverbar{≊} B)$ and $\shufflef^{-1} \tp (A \wideoverbar{≊} B) → (A
≊ B)$ respectively.
As the inverse of $\wideoverbar{\idToIso}$ I will pick $\wideoverbar{\isoToId}
≜ \isoToId \comp \shufflef$. The proof that they are inverses go as
@ -656,19 +679,18 @@ since being-an-inverse-of is a proposition, so it suffices to show that their
first components are equal, but this holds judgmentally.
This finished the proof that the opposite category is in fact a category. Now,
to prove that that opposite-of is an involution we must show:
to prove that opposite-of is an involution we must show:
%
$$
∏_{\bC \tp \Category} \left(\bC^{\var{Op}}\right)^{\var{Op}} ≡ \bC
$$
%
As we have seen the laws in $\left(\bC^{\var{Op}}\right)^{\var{Op}}$ get quite
involved\footnote{We have not even seen the full story because we have used
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.
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
must provide is the following proof:
The laws in $\left(\bC^{\var{Op}}\right)^{\var{Op}}$ get quite
involved. Luckily since being-a-category is a mere 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 just by giving an equality on the data-part. So, given a
category $\bC$ all we must provide is the following proof:
%
$$
\var{raw}\ \left(\bC^{\var{Op}}\right)^{\var{Op}} ≡ \var{raw}\ \bC
@ -685,7 +707,7 @@ $$\Set ≜ ∑_{A \tp \MCU} \isSet\ A$$
%
The more straightforward notion of a category where the objects are types is
not a valid \mbox{(1-)category}. This stems from the fact that types in cubical
Agda types can have higher homotopic structure.
Agda can have higher homotopic structure.
Univalence does not follow immediately from univalence for types:
%
@ -702,7 +724,7 @@ $$
%
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
process. For objects $(A, s_A), (B, s_B) \tp \Set$ I show the following chain
of equivalences:
%
\begin{align*}
@ -713,18 +735,18 @@ of equivalences:
\end{align*}
And since $≃$ is an equivalence relation we can chain these equivalences
together. Step one will be proven with the following lemma:
together. Step one will be proven with the lemma:
%
\begin{align}
\label{eq:equivPropSig}
\left(∏_{a \tp A} \isProp\ (P\ a)\right) → ∏_{x\;y \tp ∑_{a \tp A} P\ a} (x ≡ y) ≃ (\fst\ x ≡ \fst\ y)
\end{align}
%
The lemma states that for pairs whose second component are mere propositions
equality is equivalent to equality of the first components. In this case the
type-family $P$ is $\isSet$ which itself is a proposition for any type $A \tp
\Type$. Step two is univalence. Step three will be proven with the following
lemma:
The lemma states that for pairs whose second component are mere
propositions equality is equivalent to equality of the first
components. In this case the type-family $P$ is $\isSet$ which itself
is a proposition for any type $A \tp \Type$. Step two is univalence
for types. Step three will be proven with the following lemma:
%
\begin{align}
\label{eq:equivSig}
@ -755,10 +777,9 @@ $x ≡ y$ and $\fst\ x ≡ \fst\ y$:
\end{aligned}
\end{equation*}
%
\TODO{Is it confusing that I use point-free style here?}Here $\var{lemSig}$ is
a lemma that says that if the second component of a pair is a proposition, it
suffices to give a path between its first components to construct an equality of
the two pairs:
Here $\var{lemSig}$ is a lemma that says that if the second component
of a pair is a proposition, it suffices to give a path between its
first components to construct an equality of the two pairs:
%
\begin{align*}
\var{lemSig} \tp \left( ∏_{x \tp A} \isProp\ (B\ x) \right) →
@ -766,14 +787,14 @@ the two pairs:
\left( \fst\ u ≡ \fst\ v \right) → u ≡ v
\end{align*}
%
The proof that these are indeed inverses has been omitted. The details
can be found in the module:
The proof that these are indeed inverses of one another has been
omitted. The details can be found in the module:
\begin{center}
\sourcelink{Cat.Categories.Sets}
\end{center}
Now to prove \ref{eq:equivSig}: Let $e \tp ∏_{a \tp A} \left( P\ a
≃ Q\ a \right)$ be given. To prove the equivalence, it suffices
≃ Q\ a \right)$ be given. To prove the equivalence it suffices
to give an isomorphism between $∑_{a \tp A} P\ a$ and $∑_{a \tp
A} Q\ a$, but since they have identical first components it suffices
to give an isomorphism between $P\ a$ and $Q\ a$ for all $a \tp A$.
@ -803,13 +824,13 @@ For the other direction:
\var{toIso} \comp \var{fromIso} ≡ \identity_{\Isomorphism\ f}
\end{align*}
%
We will show that $\Isomorphism\ f$ is also a mere proposition. To this
end, let $X\;Y \tp \Isomorphism\ f$ be given. Name the maps $x\;y \tp B
→ A$ respectively. Now, the proof that $X$ and $Y$ are the same is a pair of
paths: $p \tp x ≡ y$ and $\Path\ (\lambda\; i →
\var{AreInverses}\ f\ (p\ i))\ \mathcal{X}\ \mathcal{Y}$ where $\mathcal{X}$
and $\mathcal{Y}$ denotes the witnesses that $x$ (respectively $y$) is an
inverse to $f$. The path $p$ is inhabited by:
We will show that $\Isomorphism\ f$ is also a mere proposition. To
this end, let $X, Y \tp \Isomorphism\ f$ be given. Name the maps $x, y
\tp B → A$ respectively. Now, the proof that $X$ and $Y$ are the same
is a pair of paths: $p \tp x ≡ y$ and $\Path\ (\lambda\; i →
\var{AreInverses}\ f\ (p\ i))\ \mathcal{X}\ \mathcal{Y}$ where
$\mathcal{X}$ and $\mathcal{Y}$ denotes the witnesses that $x$
(respectively $y$) is an inverse to $f$. The path $p$ is inhabited by:
%
\begin{align*}
x
@ -857,18 +878,21 @@ $$
∏_{\bC \tp \Category} ∏_{A\;B \tp \Object} \isProp\ (\var{Product}\ \bC\ A\ B)
$$
%
Where $\var{Product}\ \bC\ A\ B$ denotes the type of products of objects $A$
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
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,
we recall the definition of products.
Where $\var{Product}\ \bC\ A\ B$ denotes the type of products of
objects $A$ 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 are propositional in a proper category and
equivalences preserve homotopy level, then we know that products are
also propositions. But before we get to that, we recall the definition
of products.
\subsection{Definition of products}
Given a category $\bC$ and two objects $A$ and $B$ in $\bC$ we define the
product (object) of $A$ and $B$ to be an object $A \x B$ in $\bC$ and two arrows
$\pi_1 \tp A \x B → A$ and $\pi_2 \tp A \x B → B$ called the projections of
the product. The projections must satisfy the following property:
Given a category $\bC$ and two objects $A$ and $B$ in $\bC$ we say
that a product is triple consisting of an object and a pair of arrows.
The object is denoted with $A × B$ in $\bC$ and is also referred to as
the product (object) of $A$ and $B$. The arrows will be named $\pi_1
\tp A \x B → A$ and $\pi_2 \tp A \x B → B$ also called the projections
of the product. The projections must satisfy the following property:
For all $X \tp Object$, $f \tp \Arrow\ X\ A$ and $g \tp \Arrow\ X\ B$ we have
that there exists a unique arrow $\pi \tp \Arrow\ X\ (A \x B)$ satisfying
@ -877,31 +901,30 @@ that there exists a unique arrow $\pi \tp \Arrow\ X\ (A \x B)$ satisfying
\label{eq:umpProduct}
%% ∏_{X \tp Object} ∏_{f \tp \Arrow\ X\ A} ∏_{g \tp \Arrow\ X\ B}\\
%% \uexists_{f \x g \tp \Arrow\ X\ (A \x B)}
\pi_1 \lll \pi ≡ f \x \pi_2 \lll \pi ≡ g
\pi_1 \lll \pi ≡ f \x \pi_{2} \lll \pi ≡ g
\end{align}
%
$\pi$ is called the product (arrow) of $f$ and $g$.
The arrow $\pi$ is called the product (arrow) of $f$ and $g$.
%
\subsection{Span category}
Given a base category $\bC$ and two objects in this category $\pairA$ and
$\pairB$ we can construct the \nomenindex{span category}:
The type of objects in this category will be an object in the underlying
Given a base category $\bC$ and two objects in this category $\pairA$
and $\pairB$ we construct the \nomenindex{span category}. The type of
objects in this category shall be an object in the underlying
category, $X$, and two arrows (also from the underlying category)
$\Arrow\ X\ \pairA$ and $\Arrow\ X\ \pairB$.
\newcommand\pairf{\ensuremath{f}}
\newcommand\pairFst{\mathcal{\pi_1}}
\newcommand\pairSnd{\mathcal{\pi_2}}
\newcommand\pairSnd{\mathcal{\pi_{2}}}
An arrow between objects $A ,\ a_0 ,\ a_1$ and $B ,\ b_0 ,\ b_1$ in this
An arrow between objects $A ,\ a_{\pairA} ,\ a_{\pairB}$ and $B ,\ b_{\pairA} ,\ b_{\pairB}$ in this
category will consist of an arrow from the underlying category $\pairf \tp
\Arrow\ A\ B$ satisfying:
%
\begin{align}
\label{eq:pairArrowLaw}
b_0 \lll f ≡ a_0 \x
b_1 \lll f ≡ a_1
b_{\pairA} \lll f ≡ a_{\pairA} \x
b_{\pairB} \lll f ≡ a_{\pairB}
\end{align}
The identity morphism is the identity morphism from the underlying category.
@ -913,15 +936,15 @@ choose $g \lll f$ and we must now verify that it satisfies
\ref{eq:pairArrowLaw}:
%
\begin{align*}
c_0 \lll (f \lll g)
c_{\pairA} \lll (f \lll g)
& ≡
(c_0 \lll f) \lll g
(c_{\pairA} \lll f) \lll g
&& \text{Associativity} \\
& ≡
b_0 \lll g
b_{\pairA} \lll g
&& \text{$f$ satisfies \ref{eq:pairArrowLaw}} \\
& ≡
a_0
a_{\pairA}
&& \text{$g$ satisfies \ref{eq:pairArrowLaw}} \\
\end{align*}
%
@ -942,7 +965,7 @@ underlying category ($f$, $g$ and $h$) and a pair of witnesses to
\ref{eq:pairArrowLaw}.
%% Luckily those winesses are paths in the hom-set of the
%% underlying category which is a set, so these are mere propositions.
The proof obligations is consists of two things. The first one is:
The proof obligations consists of two things. The first one is:
%
\begin{align}
\label{eq:productAssocUnderlying}
@ -954,19 +977,21 @@ h \lll (g \lll f)
And the other proof obligation is that the witness to \ref{eq:pairArrowLaw} for
the left-hand-side and the right-hand-side are the same.
The proof of the first goal comes directly from the underlying category. The
type of the second goal is very complicated. I will not write it out in full
here, but it suffices to show the type of the path-space. Note that the arrows
in \ref{eq:productAssoc} are arrows from $\mathcal{A} = (A , a_{\pairA} ,
a_{\pairB})$ to $\mathcal{D} = (D , d_{\pairA} , d_{\pairB})$ where
$a_{\pairA}$, $a_{\pairB}$, $d_{\pairA}$ and $d_{\pairB}$ are arrows in the
The proof of the first goal comes directly from the underlying
category. The type of the second goal is very complicated. I will not
write it out in full here, but for the purpose of the present
exposition it will suffices to show the type of the path-space. Note
that the arrows in \ref{eq:productAssoc} are arrows between objects on
the form $\wideoverbar{A} = (A , a_{\pairA} , a_{\pairB})$ to
$\wideoverbar{D} = (D , d_{\pairA} , d_{\pairB})$ where $a_{\pairA}$,
$a_{\pairB}$, $d_{\pairA}$ and $d_{\pairB}$ are arrows in the
underlying category. Given that $p$ is the chosen proof of
\ref{eq:productAssocUnderlying} we then have that the witness to
\ref{eq:pairArrowLaw} vary over the type:
%
\begin{align}
\label{eq:productPath}
λ \; i → d_{\pairA} \lll p\ i ≡ 2 a_{\pairA} × d_{\pairB} \lll p\ i ≡ a_{\pairB}
λ \; i → d_{\pairA} \lll p\ i ≡ a_{\pairA} × d_{\pairB} \lll p\ i ≡ a_{\pairB}
\end{align}
%
And these paths are in the type of the hom-set of the underlying category, so
@ -979,11 +1004,12 @@ stead we generalize \ref{eq:productPath} to:
∏_{f \tp \Arrow\ X\ Y} \isProp\ \left( y_{\pairA} \lll f ≡ x_{\pairA} × y_{\pairB} \lll f ≡ x_{\pairB} \right)
\end{align}
%
For all objects $X , x_{\pairA} , x_{\pairB}$ and $Y , y_{\pairA} , y_{\pairB}$,
but this follows from pairs preserving homotopical structure and arrows in the
underlying category being sets. This gives us an equality principle for arrows
in this category that says that to prove two arrows $f, f_0, f_1$ and $g, g_0,
g_1$ equal it suffices to give a proof that $f$ and $g$ are equal.
For all objects $X , x_{\pairA} , x_{\pairB}$ and $Y , y_{\pairA} ,
y_{\pairB}$, but this follows from the fact that $∏$ and $∑$ preserve
homotopical structure. This gives us an equality principle for arrows
in this category that says that to prove two arrows $f, f_0, f_1$ and
$g, g_0, g_1$ equal it suffices to give a proof that $f$ and $g$ are
equal.
%% %
%% $$
%% ∏_{(f, f_0, f_1)\; (g,g_0,g_1) \tp \Arrow\ X\ Y} f ≡ g \to (f, f_0, f_1) ≡ (g,g_0,g_1)
@ -995,13 +1021,14 @@ And thus we have proven \ref{eq:productAssoc} simply with
Now we must prove that arrows form a set:
%
$$
\isSet\ (\Arrow\ \mathcal{X}\ \mathcal{Y})
\isSet\ (\Arrow\ \wideoverbar{X}\ \wideoverbar{Y})
$$
%
Since pairs preserve homotopical structure this reduces to:
Since pairs preserve homotopical structure this reduces to the two
obligations:
%
$$
\isSet\ (\Arrow_{\bC}\ X\ Y)
\isSet\ (\bC.\Arrow\ X\ Y)
$$
%
Which holds. And
@ -1068,11 +1095,19 @@ Finally we have the type:
\label{eq:univ-3}
(X , x_{\mathcal{A}} , x_{\mathcal{B}}) ≊ (Y , y_{\mathcal{A}} , y_{\mathcal{B}})
\end{align}
%
So the proof is a chain of isomorphisms between the types
\ref{eq:univ-0}, \ref{eq:univ-1}, \ref{eq:univ-2} and
\ref{eq:univ-3}. I will highlight the most interesting bits of this
proof. For the full proof see the implementation in the module:
%
\begin{center}
\sourcelink{Cat.Categories.Span}
\end{center}
\emph{Proposition} \ref{eq:univ-0} is isomorphic to \ref{eq:univ-1}: This is
just an application of the fact that a path between two pairs $a_0, a_1$ and
$b_0, b_1$ corresponds to a pair of paths between $a_0,b_0$ and $a_1,b_1$ (check
the implementation for the details).
$b_0, b_1$ corresponds to a pair of paths between $a_0,b_0$ and $a_1,b_1$.
\emph{Proposition} \ref{eq:univ-1} is isomorphic to \ref{eq:univ-2}:
This proof of this has been omitted but can be found in the module:
@ -1110,11 +1145,13 @@ p_{\mathcal{A}} & \tp \Path\ (\lambda\; i → p_{\var{dom}}\ i)\ x_{\mathcal{A}}
q_{\mathcal{B}} & \tp \Path\ (\lambda\; i → p_{\var{dom}}\ i)\ x_{\mathcal{B}}\ y_{\mathcal{B}}
\end{align*}
%
all as in \ref{eq:univ-2}. I use $p_{\var{dom}}$ here again to mean the path
induced by the isomorphism $f, \inv{f}$. I must now construct an isomorphism
$(X, x_{\mathcal{A}}, x_{\mathcal{B}}) ≊ (Y, y_{\mathcal{A}}, y_{\mathcal{B}})$
as in \ref{eq:univ-3}. That is, an isomorphism in the present category. I remind
the reader that such a gadget is a triple. The first component shall be:
all as in \ref{eq:univ-2}. I use $p_{\var{dom}}$ here again to mean
the path induced by the isomorphism $(f, \inv{f}, \var{inv}_f)$. We
must now construct an isomorphism $(X, x_{\mathcal{A}},
x_{\mathcal{B}}) ≊ (Y, y_{\mathcal{A}}, y_{\mathcal{B}})$ as in
\ref{eq:univ-3}. That is, an isomorphism in the present category. I
remind the reader that such a gadget is a triple. The first component
shall be:
%
\begin{align}
f \tp \Arrow\ X\ Y
@ -1134,10 +1171,10 @@ exactly what \ref{eq:domain-twist-0} gives us.
The other direction is quite analogous. We choose $\inv{f}$ as the morphism and
prove that it satisfies \ref{eq:pairArrowLaw} with \ref{eq:domain-twist-1}.
We must now show that this choice of arrows indeed form an isomorphism. Our
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
$\var{inv}_f$.
We must now show that this choice of arrows indeed form an
isomorphism. Our equality principle for arrows in this category
(\ref{eq:productEqPrinc}) gives us that it suffices to show that $f$
and $\inv{f}$ are inverses, but this is of course just $\var{inv}_f$.
This concludes the first direction of the isomorphism that we are constructing.
For the other direction we are given the isomorphism:
@ -1201,14 +1238,15 @@ The proof of the first one is:
%
\begin{align*}
\var{coe}\ \widetilde{p}_{\mathcal{A}}\ x_{\mathcal{A}}
& ≡ x_{\mathcal{A}} \lll \fst\ \inv{f} && \text{\ref{eq:coeDom} and the isomorphism $f, \inv{f}$} \\
& ≡ x_{\mathcal{A}} \lll \fst\ \inv{f} && \text{\ref{eq:coeDom} and the isomorphism $(f, \inv{f}, \var{inv}_{f})$} \\
& ≡ y_{\mathcal{A}} && \text{\ref{eq:pairArrowLaw} for $\inv{f}$}
\end{align*}
%
We have now constructed the maps between \ref{eq:univ-0} and \ref{eq:univ-1}. It
remains to show that they are inverses of each other. To cut a long story short,
the proof uses the fact that isomorphism-of is propositional and that arrows (in
both categories) are sets. The reader is referred to the implementation for the
We have now constructed the maps between \ref{eq:univ-0} and
\ref{eq:univ-1}. It remains to show that they are inverses of each
other. To cut a long story short, the proof uses the fact that
isomorphism-of is a proposition and that arrows (in both categories)
are sets. The reader is referred to the implementation for the full
gory details.
%
\subsection{Products are propositions}
@ -1217,11 +1255,10 @@ Now that we have constructed the span category\index{span category} I
will demonstrate how to use this to prove that products are
propositions. On the face of it this may seem surprising. Products
look like they are a structure on categories. After all it consist of
a select element and two arrows given some two objects. If formulated
in set theory this would be the case but in the present setting
univalence of categories give us that products are properties. I will
show this by showing that terminal objects in the span category are
equivalent to products:
a select object and two arrows. If formulated in set theory this
would be the case but in the present setting univalence of categories
give us that products are properties. I will show this by showing
that terminal objects in the span category are equivalent to products:
%
\begin{align}
\var{Terminal} ≃ \var{Product}\ ℂ\ \mathcal{A}\ \mathcal{B}
@ -1245,22 +1282,23 @@ indeed a product. That is, for an object $Y$ and two arrows $y_𝒜 \tp
%% \end{split}
\end{align}
%
Since $X, x_𝒜, x_ℬ$ is a terminal object there is a \emph{unique} arrow from
this object to any other object, so also $Y, y_𝒜, y_ℬ$ in particular (which is
also an object in the span category). The arrow we will play the role of $f$ and
it immediately satisfies \ref{eq:pairCondRev}. Any other arrow satisfying these
Since $X, x_𝒜, x_ℬ$ is a terminal object there is a \emph{unique}
arrow from this object to any other object, so in particular also $Y,
y_𝒜, y_ℬ$. The arrow we will play the role of $f$ and it immediately
satisfies \ref{eq:pairCondRev}. Any other arrow satisfying these
conditions will be equal since $f$ is unique.
For the other direction we are now given a product $X, x_𝒜, x_ℬ$. Again this
will be the terminal object. So now it remains that for any other object there
is a unique arrow from that object into $X, x_𝒜, x_ℬ$. Let $Y, y_𝒜, y_ℬ$ be
another object. As the arrow $\Arrow\ Y\ X$ we choose the product-arrow $y_𝒜 \x
y_ℬ$. Since this is a product-arrow it satisfies \ref{eq:pairCondRev}. Let us
name the witness to this $\phi_{y_𝒜 \x y_ℬ}$. So we have picked as our center of
contraction $y_𝒜 \x y_ℬ , \phi_{y_𝒜 \x y_ℬ}$ we must now show that it is
contractible. So let $f \tp \Arrow\ X\ Y$ and $\phi_f$ be given (here $\phi_f$
is the proof that $f$ satisfies \ref{eq:pairCondRev}). The proof will be a pair
of proofs:
For the other direction we are now given a product $X, x_𝒜, x_ℬ$.
Again this will be the terminal object. So now it remains that for
any other object there is a unique arrow from that object into $X,
x_𝒜, x_ℬ$. Let $Y, y_𝒜, y_ℬ$ be another object. As the arrow
$\Arrow\ Y\ X$ we choose the product-arrow $y_𝒜 \x y_ℬ$. Since this
is a product-arrow it satisfies \ref{eq:pairCondRev}. Let us name the
witness to this $\phi_{y_𝒜 \x y_ℬ}$. So we have picked as our center
of contraction $y_𝒜 \x y_ℬ , \phi_{y_𝒜 \x y_ℬ}$ we must now show that
it is contractible. So let $f \tp \Arrow\ X\ Y$ and $\phi_f$ be given
(here $\phi_f$ is the proof that $f$ satisfies \ref{eq:pairCondRev}).
The proof will be a pair of proofs:
%
\begin{alignat}{3}
p \tp & \Path\ (\lambda\; i → \Arrow\ X\ Y)\quad
@ -1277,9 +1315,9 @@ $$
( x_ℬ \lll f ≡ y_ℬ )
$$
%
$p$ follows from the universal property of $y_𝒜 \x y_ℬ$. For the latter we will
again use the same trick we did in \ref{eq:propAreInversesGen} and prove this
more general result:
We can construct $p$ from the universal property of $y_𝒜 \x y_ℬ$. For
the latter we use the same trick we did in \ref{eq:propAreInversesGen}
and prove this more general result:
%
$$
∏_{f \tp \Arrow\ Y\ X} \isProp\ (
@ -1292,19 +1330,20 @@ $$
Which follows from arrows being sets and pairs preserving such. Thus we can
close the final proof with an application of $\lemPropF$.
This concludes the proof $\var{Terminal} ≃
\var{Product}\ ℂ\ \mathcal{A}\ \mathcal{B}$ and since we have that equivalences
preserve homotopic levels along with \ref{eq:termProp} we get our final result.
That in any category:
This concludes the proof
$\var{Terminal} ≃ \var{Product}\ ℂ\ \mathcal{A}\ \mathcal{B}$
and since we have that equivalences preserve homotopic levels along
with \ref{eq:termProp} we get our final result. That is, in any
category $\bC$ we have:
%
\begin{align}
∏_{A, B \tp \Object} \isProp\ (\var{Product}\ \bC\ A\ B)
\end{align}
%
\section{Functors and natural transformations}
For the sake of completeness I will mention the definition of functors
and natural transformations. Please refer to the implementation for
the full details.
For the sake of completeness I will briefly mention the definition of
functors and natural transformations. Please refer to the
implementation for the full details.
%
\subsection{Functors}
Given two categories $\bC$ and $\bD$ a functor consists of the
@ -1327,6 +1366,7 @@ The implementation can be found here:
\sourcelink{Cat.Category.Functor}
\end{center}
\subsection{Natural Transformation}
\label{sec:nat-trans}
Given two functors between categories $\bC$ and $\bD$. Name them
$\FunF$ and $\FunG$. A natural transformation is a family of arrows:
%
@ -1352,11 +1392,11 @@ The implementation can be found here:
\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
formulations are equivalent, which due to univalence gives us a path between the
two types.
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. We then show that the two formulations are equivalent, which
due to univalence gives us a path between the two types.
Let a category $\bC$ be given. In the remainder of this sections all
objects and arrows will implicitly refer to objects and arrows in this
@ -1365,7 +1405,7 @@ endofunctor on this category. Its map on objects will be denoted
$\omapR$ and its map on arrows will be denoted $\fmap$. Likewise I
will use the notation $\pureNT$ to refer to a natural transformation
and its component at a given (implicit) object will be denoted
$\pure$.
$\pure$. This is the same notation as in \S\ref{sec:nat-trans}.
%
\subsection{Monoidal formulation}
The monoidal formulation of monads consists of the following data:
@ -1374,18 +1414,16 @@ The monoidal formulation of monads consists of the following data:
\label{eq:monad-monoidal-data}
\begin{split}
\EndoR & \tp \Functor\ ℂ\ \bC \\
\pureNT & \tp \NT{\EndoR^0}{\EndoR} \\
\joinNT & \tp \NT{\EndoR^2}{\EndoR}
\pureNT & \tp \NT{\widehat{\identity}}{\EndoR} \\
\joinNT & \tp \NT{(\EndoR \oplus \EndoR)}{\EndoR}
\end{split}
\end{align}
%
Here $\NTsym$ denotes natural transformations, the super-script in $\EndoR^2$
Denotes the composition of $\EndoR$ with itself. By the same token $\EndoR^0$ is
a curious way of denoting the identity functor. This notation has been chosen
for didactic purposes.
Here $\NTsym$ denotes natural transformations and $\oplus$ means
functor composition.
Denote the arrow-map of $\EndoR$ as $\fmap$, then this data must satisfy the
following laws:
Note that $\fmap$ is $\EndoR$'s map on arrows. This data must satisfy
the following laws.
%
\begin{align}
\label{eq:monad-monoidal-laws-0}
@ -1400,7 +1438,7 @@ following laws:
%
The implicit arguments to the arrows above have been left out and the objects
they range over are universally quantified.
%
\subsection{Kleisli formulation}
%
The Kleisli-formulation consists of the following data:
@ -1411,8 +1449,7 @@ The Kleisli-formulation consists of the following data:
\omapR & \tp \Object → \Object \\
\pure & \tp % ∏_{X \tp Object}
\Arrow\ X\ (\omapR\ X) \\
\bind & \tp % ∏_{X\;Y \tp Object} → \Arrow\ X\ (\omapR\ Y)
\Arrow\ (\omapR\ X)\ (\omapR\ Y)
\bind & \tp \Arrow\ X\ (\omapR\ Y) → \Arrow\ (\omapR\ X)\ (\omapR\ Y)
\end{split}
\end{align}
%
@ -1425,15 +1462,15 @@ The objects $X$ and $Y$ are implicitly universally quantified. With this data we
f \fish g & ≜ f \rrr (\bind\ g)
\end{align*}
%
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
is a regular maps on objects and a pair of arrows.
It is interesting to note here that this formulation does mention
functors nor natural transformations. All we have here is a regular
map on objects and a pair of arrows.
%
This data must satisfy:
%
\begin{align}
\label{eq:monad-kleisli-laws-0}
\bind\ \pure & ≡ \identity_{\EndoR\ X} \\
\bind\ \pure & ≡ \identity_{\omapR\ X} \\
\label{eq:monad-kleisli-laws-1}
\pure \fish f & ≡ f \\
\label{eq:monad-kleisli-laws-2}
@ -1443,15 +1480,16 @@ This data must satisfy:
%
Here likewise the arrows $f \tp \Arrow\ X\ (\omapR\ Y)$ and $g \tp
\Arrow\ Y\ (\omapR\ Z)$ are universally quantified as well as the
objects they range over.
objects they range over. The third law is stated in terms of reverse
function composition to mirror the way in which it interacts with the
Kleisli arrow.
%
\subsection{Equivalence of formulations}
%
The notation I have chosen here in the report
overloads e.g.\ $\pure$ to both refer to a natural transformation and an arrow.
This is of course not a coincidence as the arrow in the Kleisli formulation
shall correspond exactly to the map on arrows from the natural transformation
called $\pure$.
Both formulations mention a map called $\pure$. This is of course no
coincidence as that arrow in the Kleisli formulation shall correspond
exactly to the map on arrows for the natural transformation in the
monoidal formulation.
In the monoidal formulation we can define $\bind$:
%
@ -1525,7 +1563,7 @@ For \ref{eq:monad-kleisli-laws-2}:
\join \lll \join \lll (\fmap \comp \fmap)\ f \lll \fmap\ g
&& \text{$\join$ is a natural transformation} \\ & ≡
\join \lll \fmap\ \join \lll (\fmap \comp \fmap)\ f \lll \fmap\ g
&& \text{By \ref{eq:monad-monoidal-laws-0}} \\ & ≡
&& \text{By \ref{eq:monad-monoidal-laws-0}} \\ & =
\join \lll \fmap\ \join \lll \fmap\ (\fmap\ f) \lll \fmap\ g
&& \text{} \\ & ≡
\join \lll \fmap\ (\join \lll \fmap\ f \lll g)
@ -1558,8 +1596,9 @@ the monoidal formulation we pick:
We must now not only show the monad laws given for the monoidal
formulation (\monoidallaws), we must also verify that $\EndoR$ is a
functor and that $\pure$ and $\join$ are natural transformations. I
will ommit this here. In stead we shall see how these two mappings are
indeed inverses. The full construction can be found in the module:
will ommit this here. In stead we shall see how these two mappings
are indeed inverses. The full construction can be found in the
module:
\begin{center}
\mbox{\sourcelink{Cat.Category.Monad.Kleisli}}
\end{center}
@ -1598,14 +1637,14 @@ left implicit. Now we must show:
%
For \ref{eq:monad-forwards} let $(\omapR, \pure, \bind)$ be a monad in
the Kleisli form. Since being-a-monad is a proposition\footnote{The
proof can be found in the implementation.} we get an
equality-principle for kleisli-monads that say that to equate two such
monads it suffices to equate their data-part. So it suffices to equate
the data-parts of the \ref{eq:monad-forwards}. Such a proof is a
triple equating the three projections of \ref{eq:monad-kleisli-data}.
The first two hold definitionally -- essentially one just wraps and
unwraps the morphism in a functor. For the last equation a little more
work is required:
proof was omitted here but can be found in the implementation.} we
get an equality-principle for kleisli-monads that say that to equate
two such monads it suffices to equate their data-part. So it suffices
to equate the data-parts of the \ref{eq:monad-forwards}. Such a proof
is a triple equating the three projections of
\ref{eq:monad-kleisli-data}. The first two hold definitionally --
essentially one just wraps and unwraps the morphism in a functor. For
the last equation a little more work is required:
%
\begin{align*}
\join \lll \fmap\ f & =

4
doc/introduction.tex
View File

@ -207,13 +207,13 @@ with \nomenindex{extensional sets} $(X, \sim)$. That is a type $X \tp
\MCU$ and an equivalence relation $\sim\ \tp X \to X \to \MCU$ on that
type. Under the setoid interpretation the equivalence relation serve
as a sort of ``local'' propositional equality. Since the developer
gets to pick this relation it is not a\~priori a congruence
gets to pick this relation it is not a~priori a congruence
relation. So this must be verified manually by the developer.
Furthermore, functions between different setoids must be shown to be
setoid homomorphism, that is; they preserve the relation.
This approach has other drawbacks; it does not satisfy all
propositional equalities of type theory a priori. That is, the
propositional equalities of type theory a\~priori. That is, the
developer must manually show that e.g.\ the relation is a congruence.
Equational proofs $a \sim_{X} b$ are in some sense `local' to the
extensional set $(X , \sim)$. To e.g.\ prove that $x ∼ y → f\ x ∼