TENTATIVE COMMIT

doc/cubical.tex

@@ -11,8 +11,8 @@ 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
+The source code can be browsed online and is linked in the beginning
-\S\ref{sec:app-cubical}.
+of \S\ref{ch:implementation}.
 
 \subsection{The equality type}
 The usual notion of judgmental equality says that given a type $A \tp \MCU$ and
@@ -137,11 +137,13 @@ With this we can now prove the desired equality $f \equiv g$ from section
 %
 \begin{align*}
   p & \tp f \equiv g \\
-  p & \defeq \funExt\ \lambda n \to \refl
+  p & \defeq \funExt\ \phi
 \end{align*}
 %
-Paths have some other important properties, but they are not the focus of
+Here $\phi \tp \prod_{n \tp \bN} \var{zeroLeft}\ n \equiv
-this thesis. \TODO{Refer the reader somewhere for more info.}
+\var{zeroRight} n$. 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,
@@ -273,7 +275,7 @@ $$
 We have the function:
 %
 \begin{equation}
-\pathJ\ D\ d \tp \prod_{b \tp A} \prod_{p \tp a ≡ b} D\ a\ p
+\pathJ\ D\ d \tp \prod_{b \tp A} \prod_{p \tp a ≡ b} D\ b\ p
 \end{equation}
 %
 A simple application of $\pathJ$ is for proving that $\var{sym}$ is an

doc/implementation.tex

@@ -1,12 +1,27 @@
 \chapter{Category Theory}
 \label{ch:implementation}
+This implementaiton, including this report, is available as open
+source software at:
+%
+\begin{center}
+  \gitlink
+\end{center}
+%
+All modules imported for this formalization can be browsed at this
+link\footnote{%
+  In case the linked sources are unavailable the html
+  documentation can be generated by navigating to the root directory
+  of the project and executing \texttt{make html}.%
+}:
+%
+\begin{center}
+\doclink
+\end{center}
 This implementation formalizes the following concepts:
 %
-\newcommand{\sourcebasepath}{http://web.student.chalmers.se/~hanghj/cat/doc/html/}
-\newcommand{\sourcelink}[1]{\href{\sourcebasepath#1.html}{\texttt{#1}}}
 \begin{center}
 \begin{tabular}{ l l }
-Name & Link \\
+Name & Module \\
 \hline
 Equivalences & \sourcelink{Cat.Equivalence} \\
 Categories & \sourcelink{Cat.Category} \\
@@ -30,7 +45,7 @@ Furthermore the following items have been partly formalized:
 %
 \begin{center}
 \begin{tabular}{ l l }
-Name & Link \\
+Name & Module \\
 \hline
 Category of categories & \sourcelink{Cat.Categories.Cat} \\
 Category of relations & \sourcelink{Cat.Categories.Rel} \\
@@ -40,7 +55,7 @@ Monoids & \sourcelink{Cat.Category.Monoid} \\
 \end{tabular}
 \end{center}
 %
-As well as a range of various results about these. E.g. I have shown
+As well as a range of various results about these. E.g.\ I have shown
 that the category of sets has products. In the following I aim to
 demonstrate some of the techniques employed in this formalization and
 in the interest of brevity I will not detail all the things I have
@@ -64,15 +79,10 @@ where one can reason about two categories by simply focusing on the data. This
 is achieved by creating a function embodying the ``equality principle'' for a
 given type.
 
-For the rest of this chapter I will present some of these results. For didactic
+For the rest of this chapter I will present some of these results. For
-reasons no source-code has been included in this chapter. To see the formal
+didactic reasons no source-code has been included in this chapter. To
-definitions excerpts of the implementation have been included in appendix
+see the formal definitions the reader is referred to the
-\S\ref{ch:app-sources}:
+implementation which is linked in \S\ref{ch:implementation}.
-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}
@@ -191,7 +201,7 @@ So the proof goes like this: We `eliminate' the 3 function abstractions by
 applying $\propPi$ three times. So our proof obligation becomes:
 %
 $$
-\isProp \left( \id \comp f \equiv f \x f \comp \id \equiv f \right)
+\isProp\ \left( \id \comp f \equiv f \x f \comp \id \equiv f \right)
 $$
 %
 Then we eliminate the (non-dependent) sigma-type by applying $\propSig$ giving
@@ -224,19 +234,21 @@ 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
 combinators available to help us here. In stead the paths must be used directly.
 
-\ref{eq:propIsPreCategory} is judgmentally the same as
+\ref{eq:propIsPreCategory} is judgmentally the same as:
 %
 $$
 \prod_{a\ b \tp \IsPreCategory} a \equiv b
 $$
 %
-So let $a\ b \tp \IsPreCategory$ be given. To prove the equality $a \equiv b$ is
+So to prove the proposition let $a\ b \tp \IsPreCategory$ be given. To
-to give a continuous path from the index-type into the path-space. I.e. a
+prove the equality $a \equiv b$ is to give a continuous path from the
-function $I \to \IsPreCategory$. This path must satisfy being being judgmentally
+index-type into the path-space. I.e.\ a function $I \to
-the same as $a$ at the left endpoint and $b$ at the right endpoint. We know we
+\IsPreCategory$. This path must satisfy being being judgmentally the
-can form a continuous path between all projections of $a$ and $b$, this follows
+same as $a$ at the left endpoint and $b$ at the right endpoint. We
-from the type of all the projections being mere propositions. For instance, the
+know we can form a continuous path between all projections of $a$ and
-path between $a.\isIdentity$ and $b.\isIdentity$ is simply formed by:
+$b$, this follows from the type of all the projections being mere
+propositions. For instance, the path between $a.\isIdentity$ and
+$b.\isIdentity$ is simply formed by:
 %
 $$
 \propIsIdentity\ a.\isIdentity\ b.\isIdentity
@@ -270,18 +282,19 @@ 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
 type would already not be possible, since we at least need extensionality (the
 projections are all $\prod$-types). Assuming we had functional extensionality
-available to us as an axiom, we would use functional extensionality (in
+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
+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.
 
-The situation is a bit more complicated when we have a dependent type. For
+The situation is a bit more complicated when we have a dependent type.
-instance, when we want to show that $\IsCategory$ is a mere proposition.
+For instance, when we want to show that $\IsCategory$ is a mere
-$\IsCategory$ is a record with two fields, a witness to being a pre category and
+proposition. The type $\IsCategory$ is a record with two fields, a
-the univalence condition. Recall that the univalence condition is indexed by the
+witness to being a pre category and the univalence condition. Recall
-identity-proof. So to follow the same recipe as above, let $a\ b \tp
+that the univalence condition is indexed by the identity-proof. So to
-\IsCategory$ be given, to show them equal, we now need to give two paths. One homogeneous:
+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:
 %
 $$
 p \tp a.\isPreCategory \equiv b.\isPreCategory
@@ -340,7 +353,7 @@ The usual notion of a function $f \tp A \to B$ having an inverses is:
 %
 \begin{equation}
 \label{eq:isomorphism}
-\sum_{g \tp B \to A} f \comp g \equiv \identity_{B} \x g \comp f \equiv \identity_{A}
+\sum_{g \tp B \to A} f \comp g \equiv \identity \x g \comp f \equiv \identity
 \end{equation}
 %
 This is defined in \cite[p. 129]{hott-2013} where it is referred to as the a
@@ -384,9 +397,10 @@ I give its definition here mainly for completeness, because as I stated we can
 move away from this specific instantiation and think about it more abstractly
 once we have shown that this definition actually works as an equivalence.
 
-$\var{fromIso}$ can be found in \cite{cubical-agda} where it is known as
+The implementation of $\var{fromIso}$ can be found in
-$\var{gradLemma}$. The implementation of $\var{fromIso}$ as well as the proof
+\cite{cubical-agda} where it is known as $\var{gradLemma}$. The
-that this equivalence is a proposition (\ref{eq:propIsEquiv}) can be found in my
+implementation of $\var{fromIso}$ as well as the proof that this
+equivalence is a proposition (\ref{eq:propIsEquiv}) can be found in my
 implementation.
 
 We say that two types $A\;B \tp \Type$ are equivalent exactly if there exists an
@@ -586,27 +600,27 @@ go between $\wideoverbar{\approxeq}$ and $\approxeq$.
 An inhabitant of $A \approxeq 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 $\shuffle \tp (A \approxeq
+go in the opposite direction. I name these maps $\shufflef \tp (A \approxeq
 B) \to (A \wideoverbar{\approxeq} B)$ and $\shuffle^{-1} \tp (A
 \wideoverbar{\approxeq} B) \to (A \approxeq B)$ respectively.
 
 As the inverse of $\wideoverbar{\idToIso}$ I will pick $\wideoverbar{\isoToId}
-\defeq \isoToId \comp \shuffle$. The proof that they are inverses go as
+\defeq \isoToId \comp \shufflef$. The proof that they are inverses go as
 follows:
 %
 \begin{align*}
 \wideoverbar{\isoToId} \comp \wideoverbar{\idToIso} & =
-\isoToId \comp \shuffle \comp \wideoverbar{\idToIso}
+\isoToId \comp \shufflef \comp \wideoverbar{\idToIso}
 \\
 %% ≡⟨ cong (λ φ → φ x) (cong (λ φ → η ⊙ shuffle ⊙ φ) (funExt lem)) ⟩ \\
 %
 & \equiv
-\isoToId \comp \shuffle \comp \inv{\shuffle} \comp \idToIso
+\isoToId \comp \shufflef \comp \inv{\shufflef} \comp \idToIso
 && \text{lemma} \\
 %%   ≡⟨⟩ \\
 & \equiv
 \isoToId \comp \idToIso
-&& \text{$\shuffle$ is an isomorphism} \\
+&& \text{$\shufflef$ is an isomorphism} \\
 & \equiv
 \identity
 && \text{$\isoToId$ is an isomorphism}
@@ -615,7 +629,7 @@ follows:
 The other direction is analogous.
 
 The lemma used in step 2 of this proof states that $\wideoverbar{idToIso} \equiv
-\inv{\shuffle} \comp \idToIso$. This is a rather straight-forward proof
+\inv{\shufflef} \comp \idToIso$. This is a rather straight-forward proof
 since being-an-inverse-of is a proposition, so it suffices to show that their
 first components are equal, but this holds judgmentally.
 
@@ -681,7 +695,7 @@ together. Step one will be proven with the following lemma:
 %
 \begin{align}
   \label{eq:equivPropSig}
-\left(\prod_{a \tp A} \isProp (P\ a)\right) \to \prod_{x\;y \tp \sum_{a \tp A} P\ a} (x \equiv y) \simeq (\fst\ x \equiv \fst\ y)
+\left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \prod_{x\;y \tp \sum_{a \tp A} P\ a} (x \equiv y) \simeq (\fst\ x \equiv \fst\ y)
 \end{align}
 %
 The lemma states that for pairs whose second component are mere propositions
@@ -705,7 +719,7 @@ also be equivalent. For our purposes $P \defeq \isEquiv\ A\ B$ and $Q \defeq
 \prod_{f \tp A \to B} \left( \isEquiv\ A\ B\ f \simeq \Isomorphism\ f \right)
 \end{align}
 
-First, lets prove \ref{eq:equivPropSig}: Let $propP \tp \prod_{a \tp A} \isProp (P\ a)$ and $x\;y \tp \sum_{a \tp A} P\ a$ be given. Because
+First, lets prove \ref{eq:equivPropSig}: Let $propP \tp \prod_{a \tp A} \isProp\ (P\ a)$ and $x\;y \tp \sum_{a \tp A} P\ a$ be given. Because
 of $\var{fromIsomorphism}$ it suffices to give an isomorphism between
 $x \equiv y$ and $\fst\ x \equiv \fst\ y$:
 %
@@ -770,7 +784,7 @@ end, let $X\;Y \tp \Isomorphism\ f$ be given. Name the maps $x\;y \tp B
 paths: $p \tp x \equiv y$ and $\Path\ (\lambda\; i \to
 \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$. $p$ is inhabited by:
+inverse to $f$. The path $p$ is inhabited by:
 %
 \begin{align*}
   x
@@ -844,9 +858,6 @@ that there exists a unique arrow $\pi \tp \Arrow\ X\ (A \x B)$ satisfying
 $\pi$ is called the product (arrow) of $f$ and $g$.
 
 \subsection{Span category}
-
-\newcommand\pairA{\mathcal{A}}
-\newcommand\pairB{\mathcal{B}}
 Given a base category $\bC$ and two objects in this category $\pairA$ and
 $\pairB$ we can construct the \nomenindex{span category}:
 
@@ -1018,7 +1029,7 @@ isomorphism, and create a path from this:
 \begin{align}
 \label{eq:univ-2}
 \begin{split}
-\var{iso} \tp & X \cong Y \\
+\var{iso} \tp & X \approxeq Y \\
 & \Path\ (λ i → \Arrow\ (\widetilde{p}\ i)\ \mathcal{A})\ x_{\mathcal{A}}\ y_{\mathcal{A}} \\
 & \Path\ (λ i → \Arrow\ (\widetilde{p}\ i)\ \mathcal{B})\ x_{\mathcal{B}}\ y_{\mathcal{B}}
 \end{split}
@@ -1084,7 +1095,7 @@ To show that this choice fits the bill I must now verify that it satisfies
 y_{\mathcal{A}} \lll f ≡ x_{\mathcal{A}} × y_{\mathcal{B}} \lll f ≡ x_{\mathcal{B}}
 \end{align}
 %
-Which, since $f$ is an isomorphism and $p_{\mathcal{A}}$ (resp. $p_{\mathcal{B}}$)
+Which, since $f$ is an isomorphism and $p_{\mathcal{A}}$ (resp.\ $p_{\mathcal{B}}$)
 is a path varying according to a path constructed from this isomorphism, this is
 exactly what \ref{eq:domain-twist-0} gives us.
 %
@@ -1100,7 +1111,7 @@ This concludes the first direction of the isomorphism that we are constructing.
 For the other direction we are given the isomorphism:
 %
 $$
-(f, \inv{f}, \var{inv}_f)
+(f, \inv{f}, \var{inv}_f, \var{inv}_{\inv{f}})
 \tp
 (X, x_{\mathcal{A}}, x_{\mathcal{B}}) \approxeq (Y, y_{\mathcal{A}}, y_{\mathcal{B}})
 $$
@@ -1108,7 +1119,10 @@ $$
 Projecting out the first component gives us the isomorphism
 %
 $$
-(\fst\ f, \fst\ \inv{f}, \congruence\ \fst\ \var{inv}_f, \congruence\ \fst\ \var{inv}_{\inv{f}})
+(\fst\ f, \fst\ \inv{f}
+, \congruence\ \fst\ \var{inv}_f
+, \congruence\ \fst\ \var{inv}_{\inv{f}}
+)
 \tp X \approxeq Y
 $$
 %
@@ -1141,11 +1155,11 @@ This is achieved with the following lemma:
 %
 Which is used without proof. See the implementation for the details.
 
-\ref{eq:product-paths} is the proven with the propositions:
+\ref{eq:product-paths} is then proven with the propositions:
 %
 \begin{align}
 \begin{split}
-\label{eq:product-paths}
+%% \label{eq:product-paths}
 \var{coe}\ \widetilde{p}_{\mathcal{A}}\ x_{\mathcal{A}} ≡ y_{\mathcal{A}}\\
 \var{coe}\ \widetilde{p}_{\mathcal{B}}\ x_{\mathcal{B}} ≡ y_{\mathcal{B}}
 \end{split}
@@ -1155,7 +1169,7 @@ 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{$\var{coeDom}$ and the isomorphism $f, \inv{f}$} \\
+  & ≡ x_{\mathcal{A}} \lll \fst\ \inv{f} && \text{\ref{eq:coeDom} and the isomorphism $f, \inv{f}$} \\
   & ≡ y_{\mathcal{A}} && \text{\ref{eq:pairArrowLaw} for $\inv{f}$}
 \end{align*}
 %
@@ -1167,10 +1181,10 @@ gory details.
 %
 \subsection{Propositionality of products}
 %
-Now that we have constructed the span category\index{span category} I will
+Now that we have constructed the span category\index{span category} I
-    demonstrate how to use this to prove that products are propositional. I will
+will demonstrate how to use this to prove that products are
-    do this by showing that terminal objects in this category are equivalent to
+propositional. I will do this by showing that terminal objects in this
-    products:
+category are equivalent to products:
 %
 \begin{align}
 \var{Terminal} ≃ \var{Product}\ ℂ\ \mathcal{A}\ \mathcal{B}
@@ -1179,7 +1193,7 @@ Now that we have constructed the span category\index{span category} I will
 And as always we do this by constructing an isomorphism:
 %
 In the direction $\var{Terminal} → \var{Product}\ ℂ\ \mathcal{A}\ \mathcal{B}$
-we are 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
 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
@@ -1265,8 +1279,8 @@ The monoidal formulation of monads consists of the following data:
 \label{eq:monad-monoidal-data}
 \begin{split}
     \EndoR      & \tp \Endo ℂ \\
-    \pure  & \tp \NT{\EndoR^0}{\EndoR} \\
+    \pureNT  & \tp \NT{\EndoR^0}{\EndoR} \\
-    \join  & \tp \NT{\EndoR^2}{\EndoR}
+    \joinNT  & \tp \NT{\EndoR^2}{\EndoR}
 \end{split}
 \end{align}
 %
@@ -1299,11 +1313,11 @@ The Kleisli-formulation consists of the following data:
 \begin{align}
 \begin{split}
 \label{eq:monad-kleisli-data}
-\EndoR & \tp \Object → \Object \\
+\omapR & \tp \Object → \Object \\
 \pure  & \tp % \prod_{X \tp Object}
-      \Arrow\ X\ (\EndoR\ X) \\
+      \Arrow\ X\ (\omapR\ X) \\
-    \bind  & \tp % \prod_{X\;Y \tp Object} → \Arrow\ X\ (\EndoR\ Y)
+    \bind  & \tp % \prod_{X\;Y \tp Object} → \Arrow\ X\ (\omapR\ Y)
-    \Arrow\ (\EndoR\ X)\ (\EndoR\ Y)
+    \Arrow\ (\omapR\ X)\ (\omapR\ Y)
 \end{split}
 \end{align}
 %
@@ -1346,22 +1360,20 @@ In the monoidal formulation we can define $\bind$:
 \newcommand\pureX{\wideoverbar{\pure}}%
 \newcommand\fmapX{\wideoverbar{\fmap}}%
 \begin{align}
-\bind\ f \defeq \joinX \lll \fmap\ f
+\bind\ f \defeq \join \lll \fmap\ f
 \end{align}
 %
 And likewise in the Kleisli formulation we can define $\join$:
 %
 \begin{align}
-\join \defeq \bindX\ \identity
+\join \defeq \bind\ \identity
 \end{align}
 %
-Here $\joinX$ corresponds to the arrow from the natural
+It now remains to show that this construction indeed gives rise to a
-transformation $\join$. $\bindX$ on the other hand corresponds to a
+monad. This will be done in two steps. First we will assume that we
-natural transformation constructed from $\bind$. It now remains to show that
+have a monad in the monoidal form; $(\EndoR, \pure, \join)$ and then
-this construction indeed gives rise to a monad. This will be done in two steps.
+show that $(\omapR, \pure, \bind)$ is indeed a monad in the Kleisli
-First we will assume that we have a monad in the monoidal form; $(\EndoR, \pure,
+form. In the second part we will show the other direction.
-\join)$ and then show that $\EndoR, \pure, \bind$ is indeed a monad in the
-Kleisli form. In the second part we will show the other direction.
 
 \subsubsection{Monoidal to Kleisli}
 Let $(\EndoR, \pure, \join)$ be given as in \ref{eq:monad-monoidal-data}
@@ -1376,11 +1388,11 @@ formulation we pick:
 \end{split}
 \end{align}
 %
-$\EndoRX$ is the object map of the endo-functor $\EndoR$,
+$\EndoRX$ is the object map of the endo-functor $\EndoR$, $\pureX$ and
-$\pureX$ and $\joinX$ are the arrows from the natural
+$\joinX$ are the arrows from the natural transformations $\pure$ and
-transformations $\pure$ and $\join$ respectively. $\fmapX$ is the
+$\join$ respectively. The term $\fmapX$ is the arrow map of the
-arrow map of the endo-functor $\EndoR$. It now just remains to verify
+endo-functor $\EndoR$. It now just remains to verify the laws
-the laws \kleislilaws. For \ref{eq:monad-kleisli-laws-0}:
+\kleislilaws. For \ref{eq:monad-kleisli-laws-0}:
 %
 \begin{align*}
 \bind\ \pure & ≡

doc/macros.tex

@@ -72,13 +72,17 @@
 \newcommand\isequiv{\varindex{isequiv}}
 \newcommand\qinv{\varindex{qinv}}
 \newcommand\fiber{\varindex{fiber}}
-\newcommand\shuffle{\varindex{shuffle}}
+\newcommand\shufflef{\varindex{shuffle}}
 \newcommand\Univalent{\varindex{Univalent}}
 \newcommand\refl{\varindex{refl}}
 \newcommand\isoToId{\varindex{isoToId}}
 \newcommand\Isomorphism{\varindex{Isomorphism}}
 \newcommand\rrr{\ggg}
-\newcommand\fish{\mathrel{\wideoverbar{\rrr}}}
+%% \newcommand\fish{\mathbin{↣}}
+%% \newcommand\fish{\mathbin{⤅}}
+\newcommand\fish{\mathbin{⤇}}
+%% \newcommand\fish{\mathbin{⤜}}
+%% \newcommand\fish{\mathrel{\wideoverbar{\rrr}}}
 \newcommand\fst{\varindex{fst}}
 \newcommand\snd{\varindex{snd}}
 \newcommand\Path{\varindex{Path}}
@@ -87,12 +91,29 @@
 \newcommand*{\QED}{\hfill\ensuremath{\square}}%
 \newcommand\uexists{\exists!}
 \newcommand\Arrow{\varindex{Arrow}}
+\newcommand\embellish[1]{\widehat{#1}}
+\newcommand\nattrans[1]{\embellish{#1}}
+\newcommand\functor[1]{\embellish{#1}}
 \newcommand\NTsym{\varindex{NT}}
 \newcommand\NT[2]{\NTsym\ #1\ #2}
 \newcommand\Endo[1]{\varindex{Endo}\ #1}
-\newcommand\EndoR{\mathcal{R}}
+\newcommand\EndoR{\functor{\mathcal{R}}}
+\newcommand\omapR{\mathcal{R}}
 \newcommand\funExt{\varindex{funExt}}
 \newcommand{\suc}[1]{\varindex{suc}\ #1}
 \newcommand{\trans}{\varindex{trans}}
 \newcommand{\toKleisli}{\varindex{toKleisli}}
 \newcommand{\toMonoidal}{\varindex{toMonoidal}}
+\newcommand\pairA{\mathcal{A}}
+\newcommand\pairB{\mathcal{B}}
+\newcommand{\joinNT}{\functor{\varindex{join}}}
+\newcommand{\pureNT}{\functor{\varindex{pure}}}
+\newcommand{\hrefsymb}[2]{\href{#1}{#2 \ExternalLink}}
+\newcommand{\sourcebasepath}{http://web.student.chalmers.se/\textasciitilde hanghj/cat/doc/html/}
+\newcommand{\docbasepath}{https://github.com/fredefox/cat/}
+\newcommand{\sourcelink}[1]{\hrefsymb
+    {\sourcebasepath#1.html}
+    {\texttt{#1}}
+  }
+\newcommand{\gitlink}{\hrefsymb{\docbasepath}{\texttt{\docbasepath}}}
+\newcommand{\doclink}{\hrefsymb{\sourcebasepath}{\texttt{\sourcebasepath}}}

doc/main.tex

@@ -62,12 +62,12 @@
 \nocite{coquand-2013}
 
 \bibliography{refs}
-\begin{appendices}
+%% \begin{appendices}
-\setcounter{page}{1}
+%% \setcounter{page}{1}
-\pagenumbering{roman}
+%% \pagenumbering{roman}
-\input{sources.tex}
+%% \input{sources.tex}
 %% \input{planning.tex}
 %% \input{halftime.tex}
-\end{appendices}
+%% \end{appendices}
 \printindex
 \end{document}

doc/packages.tex

@@ -4,14 +4,17 @@
 \bibliographystyle{plain}
 
 \usepackage{xcolor}
+%% \mode<report>{
 \usepackage[
   %% hidelinks,
   pdfusetitle,
   pdfsubject={category theory},
   pdfkeywords={type theory, homotopy theory, category theory, agda}]
   {hyperref}
-\definecolor{darkorange}{HTML}{ff8c00}
+%% }
-\hypersetup{allbordercolors={darkorange}}
+%% \definecolor{darkorange}{HTML}{ff8c00}
+%% \hypersetup{allbordercolors={darkorange}}
+\hypersetup{hidelinks}
 \usepackage{graphicx}
 
 \usepackage{parskip}
@@ -116,3 +119,24 @@
 
 \makeatother
 \usepackage{xspace}
+\usepackage{tikz}
+\newcommand{\ExternalLink}{%
+    \tikz[x=1.2ex, y=1.2ex, baseline=-0.05ex]{% 
+        \begin{scope}[x=1ex, y=1ex]
+            \clip (-0.1,-0.1) 
+                --++ (-0, 1.2) 
+                --++ (0.6, 0) 
+                --++ (0, -0.6) 
+                --++ (0.6, 0) 
+                --++ (0, -1);
+            \path[draw, 
+                line width = 0.5, 
+                rounded corners=0.5] 
+                (0,0) rectangle (1,1);
+        \end{scope}
+        \path[draw, line width = 0.5] (0.5, 0.5) 
+            -- (1, 1);
+        \path[draw, line width = 0.5] (0.6, 1) 
+            -- (1, 1) -- (1, 0.6);
+        }
+    }

doc/presentation.tex

@@ -1,9 +1,18 @@
 \documentclass[a4paper,handout]{beamer}
+\beamertemplatenavigationsymbolsempty
+%% \usecolortheme[named=seagull]{structure}
+
 \input{packages.tex}
 \input{macros.tex}
-\title{Univalent Categories}
+\title[Univalent Categories]{Univalent Categories\\ \footnotesize A formalization of category theory in Cubical Agda}
-\author{Frederik Hangh{\o}j Iversen}
+\newcommand{\myname}{Frederik Hangh{\o}j Iversen}
+\author[\myname]{
+  \myname\\
+  \footnotesize Supervisors: Thierry Coquand, Andrea Vezzosi\\
+  Examiner: Andreas Abel
+}
 \institute{Chalmers University of Technology}
+
 \begin{document}
 \frame{\titlepage}
 
@@ -12,14 +21,14 @@
   \framesubtitle{Functional extensionality}
   Consider the functions
   \begin{align*}
-  \var{zeroLeft} & \defeq (n \tp \bN) \mto (0 + n \tp \bN) \\
+    \var{zeroLeft}  & \defeq \lambda (n \tp \bN) \mto (0 + n \tp \bN) \\
-  \var{zeroRight} & \defeq (n \tp \bN) \mto (n + 0 \tp \bN)
+    \var{zeroRight} & \defeq \lambda (n \tp \bN) \mto (n + 0 \tp \bN)
   \end{align*}
   \pause
   We have
   %
   $$
-\prod_{n \tp \bN} n + 0 \equiv 0 + n
+  \prod_{n \tp \bN} \var{zeroLeft}\ n \equiv \var{zeroRight}\ n
   $$
   %
   \pause
@@ -35,7 +44,6 @@ We need
   $$
   \funExt \tp \prod_{a \tp A} f\ a \equiv g\ a \to f \equiv g
   $$
-
 \end{frame}
 \begin{frame}
   \frametitle{Motivating example}
@@ -53,7 +61,7 @@ $$
   $$(A \simeq B) \simeq (A \equiv B)$$
   \pause
   %
-  We will return to $\simeq$, but for not, think of it as an
+  We will return to $\simeq$, but for now think of it as an
   isomorphism, so it induces maps:
   \begin{align*}
     \var{toPath}  & \tp (A \simeq B) \to (A \equiv B) \\
@@ -117,7 +125,10 @@ $$
     & \isSet    && \tp \MCU \to \MCU \\
     & \isSet\ A && \defeq \prod_{a_0, a_1 \tp A} \isProp\ (a_0 \equiv a_1)
   \end{align*}
-\pause
+  \begin{align*}
+    & \isGroupoid    && \tp \MCU \to \MCU \\
+    & \isGroupoid\ A && \defeq \prod_{a_0, a_1 \tp A} \isSet\ (a_0 \equiv a_1)
+  \end{align*}
 \end{frame}
 \begin{frame}
   \frametitle{Paths}
@@ -137,9 +148,9 @@ $$
   \pause
   We then have the function:
   %
-\begin{equation}
+  $$
-\pathJ\ D\ d \tp \prod_{b \tp A} \prod_{p \tp a ≡ b} D\ a\ p
+    \pathJ\ D\ d \tp \prod_{b \tp A} \prod_{p \tp a ≡ b} D\ b\ p
-\end{equation}
+  $$
 \end{frame}
 \begin{frame}
   \frametitle{Paths}
@@ -179,7 +190,7 @@ $$
   $$
 \end{frame}
 \begin{frame}
-\frametitle{Categories}
+  \frametitle{Pre categories}
   \framesubtitle{Definition}
   Data:
   \begin{align*}
@@ -189,25 +200,48 @@ Data:
     \lll      & \tp \Arrow\ B\ C \to \Arrow\ A\ B \to \Arrow\ A\ C
   \end{align*}
   %
+  \pause
   Laws:
   %
   $$
   h \lll (g \lll f) ≡ (h \lll g) \lll f
   $$
   $$
-\identity \lll f ≡ f \x
+  (\identity \lll f ≡ f)
-f \lll \identity ≡ f
+  \x
+  (f \lll \identity ≡ f)
   $$
   \pause
   1-categories:
   $$
   \isSet\ (\Arrow\ A\ B)
   $$
+\end{frame}
+\begin{frame}
+  \frametitle{Pre categories}
+  \framesubtitle{Propositionality}
+  $$
+  \isProp\ \left( (\identity \comp f \equiv f) \x (f \comp \identity \equiv f) \right)
+  $$
   \pause
-Univalent categories:
+  \begin{align*}
-$$
+    \isProp\ \IsPreCategory
-\isEquiv\ (A \equiv B)\ (A \approxeq B)\ \idToIso
+  \end{align*}
-$$
+  \pause
+  \begin{align*}
+    \var{isAssociative} & \tp \var{IsAssociative}\\
+    \isIdentity    & \tp \var{IsIdentity}\\
+    \var{arrowsAreSets} & \tp \var{ArrowsAreSets}
+  \end{align*}
+  \pause
+  \begin{align*}
+    & \var{propIsAssociative} && a.\var{isAssociative}\
+    && b.\var{isAssociative} && i  \\
+    & \propIsIdentity    && a.\isIdentity\
+    && b.\isIdentity    && i  \\
+    & \var{propArrowsAreSets} && a.\var{arrowsAreSets}\
+    && b.\var{arrowsAreSets} && i
+  \end{align*}
 \end{frame}
 \begin{frame}
   \frametitle{Categories}
@@ -222,15 +256,394 @@ where
   $$
   \phi\ f \defeq \identity \lll f \equiv f \x f \lll \identity \equiv f
   $$
+  \pause
   Let $\approxeq$ denote ismorphism of objects. We can then construct
   the identity isomorphism in any category:
   $$
   \identity , \identity , \var{isIdentity} \tp A \approxeq A
   $$
+  \pause
   Likewise since paths are substitutive we can promote a path to an isomorphism:
   $$
   \idToIso \tp A ≡ B → A ≊ B
   $$
+  \pause
   For a category to be univalent we require this to be an equivalence:
+  %
+  $$
+  \isEquiv\ (A \equiv B)\ (A \approxeq B)\ \idToIso
+  $$
+  %
+\end{frame}
+\begin{frame}
+  \frametitle{Categories}
+  \framesubtitle{Univalence, cont'd}
+  $$\isEquiv\ (A \equiv B)\ (A \approxeq B)\ \idToIso$$
+  \pause%
+  $$(A \equiv B) \simeq (A \approxeq B)$$
+  \pause%
+  $$(A \equiv B) \cong (A \approxeq B)$$
+  \pause%
+  Name the above maps:
+  $$\idToIso \tp A ≡ B → A ≊ B$$
+  %
+  $$\isoToId \tp (A \approxeq B) \to (A \equiv B)$$
+\end{frame}
+\begin{frame}
+  \frametitle{Categories}
+  \framesubtitle{Propositionality}
+  $$
+  \isProp\ \IsCategory = \prod_{a, b \tp \IsCategory} a \equiv b
+  $$
+  \pause
+  So, for
+  $$
+  a\ b \tp \IsCategory
+  $$
+  the proof obligation is the pair:
+  %
+  \begin{align*}
+    p & \tp a.\isPreCategory \equiv b.\isPreCategory \\
+    & \mathrel{\ } \Path\ (\lambda\; i \to (p\ i).Univalent)\ a.\isPreCategory\ b.\isPreCategory
+  \end{align*}
+\end{frame}
+\begin{frame}
+  \frametitle{Categories}
+  \framesubtitle{Propositionality, cont'd}
+  First path given by:
+  $$
+  p
+  \defeq
+  \var{propIsPreCategory}\ a\ b
+  \tp
+  a.\isPreCategory \equiv b.\isPreCategory
+  $$
+  \pause
+  Use $\lemPropF$ for the latter.
+  \pause
+  %
+  Univalence is indexed by an identity proof. So $A \defeq
+  IsIdentity\ identity$ and $B \defeq \var{Univalent}$.
+  \pause
+  %
+  $$
+  \lemPropF\ \var{propUnivalent}\ p
+  $$
+\end{frame}
+
+\begin{frame}
+  \frametitle{Categories}
+  \framesubtitle{A theorem}
+  %
+  Let the isomorphism $(ι, \inv{ι}) \tp A \approxeq B$.
+  %
+  \pause
+  %
+  The isomorphism induces the path
+  %
+  $$
+  p \defeq \idToIso\ (\iota, \inv{\iota}) \tp A \equiv B
+  $$
+  %
+  \pause
+  and consequently an arrow:
+  %
+  $$
+  p_{\var{dom}} \defeq \congruence\ (λ x → \Arrow\ x\ X)\ p
+  \tp
+  \Arrow\ A\ X \equiv \Arrow\ B\ X
+  $$
+  %
+  \pause
+  The proposition is:
+  %
+  \begin{align}
+    \label{eq:coeDom}
+    \tag{$\var{coeDom}$}
+    \prod_{f \tp A \to X}
+    \var{coe}\ p_{\var{dom}}\ f \equiv f \lll \inv{\iota}
+  \end{align}
+\end{frame}
+\begin{frame}
+  \frametitle{Categories}
+  \framesubtitle{A theorem, proof}
+  \begin{align*}
+    \var{coe}\ p_{\var{dom}}\ f
+    & \equiv f \lll \inv{(\idToIso\ p)} && \text{By path-induction} \\
+    & \equiv f \lll \inv{\iota}
+    && \text{$\idToIso$ and $\isoToId$ are inverses}\\
+  \end{align*}
+  \pause
+  %
+  Induction will be based at $A$. Let $\widetilde{B}$ and $\widetilde{p}
+  \tp A \equiv \widetilde{B}$ be given.
+  %
+  \pause
+  %
+  Define the family:
+  %
+  $$
+  D\ \widetilde{B}\ \widetilde{p} \defeq
+  \var{coe}\ \widetilde{p}_{\var{dom}}\ f
+  \equiv
+  f \lll \inv{(\idToIso\ \widetilde{p})}
+  $$
+  \pause
+  %
+  The base-case becomes:
+  $$
+  d \tp D\ A\ \refl =
+  \var{coe}\ \refl_{\var{dom}}\ f \equiv f \lll \inv{(\idToIso\ \refl)}
+  $$
+\end{frame}
+\begin{frame}
+  \frametitle{Categories}
+  \framesubtitle{A theorem, proof, cont'd}
+  $$
+  d \tp
+  \var{coe}\ \refl_{\var{dom}}\ f \equiv f \lll \inv{(\idToIso\ \refl)}
+  $$
+  \pause
+  \begin{align*}
+    \var{coe}\ \refl^*\ f
+    & \equiv f
+    && \text{$\refl$ is a neutral element for $\var{coe}$}\\
+    & \equiv f \lll \identity \\
+    & \equiv f \lll \var{subst}\ \refl\ \identity
+    && \text{$\refl$ is a neutral element for $\var{subst}$}\\
+    & \equiv f \lll \inv{(\idToIso\ \refl)}
+    && \text{By definition of $\idToIso$}\\
+  \end{align*}
+  \pause
+  In conclusion, the theorem is inhabited by:
+  $$
+  \label{eq:pathJ-example}
+  \pathJ\ D\ d\ B\ p
+  $$
+\end{frame}
+\begin{frame}
+  \frametitle{Span category} \framesubtitle{Definition} Given a base
+  category $\bC$ and two objects in this category $\pairA$ and $\pairB$
+  we can construct the \nomenindex{span category}:
+  %
+  \pause
+  Objects:
+  $$
+  \sum_{X \tp Object} \Arrow\ X\ \pairA × \Arrow\ X\ \pairB
+  $$
+  \pause
+  %
+  Arrows between objects $A ,\ a_{\pairA} ,\ a_{\pairB}$ and
+  $B ,\ b_{\pairA} ,\ b_{\pairB}$:
+  %
+  $$
+  \sum_{f \tp \Arrow\ A\ B}
+  b_{\pairA} \lll f \equiv a_{\pairA} \x
+  b_{\pairB} \lll f \equiv a_{\pairB}
+  $$
+\end{frame}
+\begin{frame}
+  \frametitle{Span category}
+  \framesubtitle{Univalence}
+  \begin{align*}
+    \label{eq:univ-0}
+    (X , x_{\mathcal{A}} , x_{\mathcal{B}}) ≡ (Y , y_{\mathcal{A}} , y_{\mathcal{B}})
+  \end{align*}
+  \begin{align*}
+    \label{eq:univ-1}
+    \begin{split}
+      p \tp & X \equiv Y \\
+      & \Path\ (λ i → \Arrow\ (p\ i)\ \mathcal{A})\ x_{\mathcal{A}}\ y_{\mathcal{A}} \\
+      & \Path\ (λ i → \Arrow\ (p\ i)\ \mathcal{B})\ x_{\mathcal{B}}\ y_{\mathcal{B}}
+    \end{split}
+  \end{align*}
+  \begin{align*}
+    \begin{split}
+      \var{iso} \tp & X \approxeq Y \\
+      & \Path\ (λ i → \Arrow\ (\widetilde{p}\ i)\ \mathcal{A})\ x_{\mathcal{A}}\ y_{\mathcal{A}} \\
+      & \Path\ (λ i → \Arrow\ (\widetilde{p}\ i)\ \mathcal{B})\ x_{\mathcal{B}}\ y_{\mathcal{B}}
+    \end{split}
+  \end{align*}
+  \begin{align*}
+    (X , x_{\mathcal{A}} , x_{\mathcal{B}}) ≊ (Y , y_{\mathcal{A}} , y_{\mathcal{B}})
+  \end{align*}
+\end{frame}
+\begin{frame}
+  \frametitle{Span category}
+  \framesubtitle{Univalence, proof}
+  %
+  \begin{align*}
+    %% (f, \inv{f}, \var{inv}_f, \var{inv}_{\inv{f}})
+    %% \tp
+    (X, x_{\mathcal{A}}, x_{\mathcal{B}}) \approxeq (Y, y_{\mathcal{A}}, y_{\mathcal{B}})
+    \to
+    \begin{split}
+      \var{iso} \tp & X \approxeq Y \\
+      & \Path\ (λ i → \Arrow\ (\widetilde{p}\ i)\ \mathcal{A})\ x_{\mathcal{A}}\ y_{\mathcal{A}} \\
+      & \Path\ (λ i → \Arrow\ (\widetilde{p}\ i)\ \mathcal{B})\ x_{\mathcal{B}}\ y_{\mathcal{B}}
+    \end{split}
+  \end{align*}
+  \pause
+  %
+  Let $(f, \inv{f}, \var{inv}_f, \var{inv}_{\inv{f}})$ be an inhabitant
+  of the antecedent.\pause
+
+  Projecting out the first component gives us the isomorphism
+  %
+  $$
+  (\fst\ f, \fst\ \inv{f}
+  , \congruence\ \fst\ \var{inv}_f
+  , \congruence\ \fst\ \var{inv}_{\inv{f}}
+  )
+  \tp X \approxeq Y
+  $$
+  \pause
+  %
+  This gives rise to the following paths:
+  %
+  \begin{align*}
+    \begin{split}
+      \widetilde{p} & \tp X \equiv Y \\
+      \widetilde{p}_{\mathcal{A}} & \tp \Arrow\ X\ \mathcal{A} \equiv \Arrow\ Y\ \mathcal{A} \\
+    \end{split}
+  \end{align*}
+  %
+\end{frame}
+\begin{frame}
+  \frametitle{Span category}
+  \framesubtitle{Univalence, proof, cont'd}
+  It remains to construct:
+  %
+  \begin{align*}
+    \begin{split}
+      \label{eq:product-paths}
+      & \Path\ (λ i → \widetilde{p}_{\mathcal{A}}\ i)\ x_{\mathcal{A}}\ y_{\mathcal{A}}
+    \end{split}
+  \end{align*}
+  \pause
+  %
+  This is achieved with the following lemma:
+  %
+  \begin{align*}
+    \prod_{q \tp A \equiv B} \var{coe}\ q\ x_{\mathcal{A}} ≡ y_{\mathcal{A}}
+    →
+    \Path\ (λ i → q\ i)\ x_{\mathcal{A}}\ y_{\mathcal{A}}
+  \end{align*}
+  %
+  Which is used without proof.\pause
+
+  So the construction reduces to:
+  %
+  \begin{align*}
+    \var{coe}\ \widetilde{p}_{\mathcal{A}}\ x_{\mathcal{A}} ≡ y_{\mathcal{A}}
+  \end{align*}%
+  \pause%
+  This is proven with:
+  %
+  \begin{align*}
+    \var{coe}\ \widetilde{p}_{\mathcal{A}}\ x_{\mathcal{A}}
+    & ≡ x_{\mathcal{A}} \lll \fst\ \inv{f} && \text{\ref{eq:coeDom}} \\
+    & ≡ y_{\mathcal{A}} && \text{Property of span category}
+  \end{align*}
+\end{frame}
+\begin{frame}
+  \frametitle{Propositionality of products}
+  We have
+  %
+  $$
+  \isProp\ \var{Terminal}
+  $$\pause
+  %
+  We can show:
+  \begin{align*}
+    \var{Terminal} ≃ \var{Product}\ ℂ\ \mathcal{A}\ \mathcal{B}
+  \end{align*}
+  \pause
+  And since equivalences preserve homotopy levels we get:
+  %
+  $$
+  \isProp\ \left(\var{Product}\ \bC\ \mathcal{A}\ \mathcal{B}\right)
+  $$
+\end{frame}
+\begin{frame}
+  \frametitle{Monads}
+  \framesubtitle{Monoidal form}
+  %
+  \begin{align*}
+    \EndoR  & \tp \Endo ℂ \\
+    \pureNT
+    & \tp \NT{\EndoR^0}{\EndoR} \\
+    \joinNT
+    & \tp \NT{\EndoR^2}{\EndoR}
+  \end{align*}
+  \pause
+  %
+  Let $\fmap$ be the map on arrows of $\EndoR$. Likewise
+  $\pure$ and $\join$ are the maps of the natural transformations
+  $\pureNT$ and $\joinNT$ respectively.
+  %
+  \begin{align*}
+    \join \lll \fmap\ \join
+    & ≡ \join \lll \join \\
+    \join \lll \pure\           & ≡ \identity \\
+    \join \lll \fmap\     \pure & ≡ \identity
+  \end{align*}
+\end{frame}
+\begin{frame}
+  \frametitle{Monads}
+  \framesubtitle{Kleisli form}
+  %
+  \begin{align*}
+    \omapR & \tp \Object → \Object \\
+    \pure  & \tp % \prod_{X \tp Object}
+    \Arrow\ X\ (\omapR\ X) \\
+    \bind  & \tp
+    \Arrow\ X\ (\omapR\ Y)
+    \to
+    \Arrow\ (\omapR\ X)\ (\omapR\ Y)
+  \end{align*}\pause
+  %
+  \begin{align*}
+    \fish & \tp
+    \Arrow\ A\ (\omapR\ B)
+    →
+    \Arrow\ B\ (\omapR\ C)
+    →
+    \Arrow\ A\ (\omapR\ C) \\
+    f \fish g & \defeq f \rrr (\bind\ g)
+  \end{align*}
+  \pause
+  %
+  \begin{align*}
+    \label{eq:monad-kleisli-laws-0}
+    \bind\ \pure & ≡ \identity_{\omapR\ X} \\
+    \label{eq:monad-kleisli-laws-1}
+    \pure \fish f & ≡ f \\
+    \label{eq:monad-kleisli-laws-2}
+    (\bind\ f) \rrr (\bind\ g) & ≡ \bind\ (f \fish g)
+  \end{align*}
+\end{frame}
+\begin{frame}
+  \frametitle{Monads}
+  \framesubtitle{Equivalence}
+  In the monoidal formulation we can define $\bind$:
+  %
+  $$
+  \bind\ f \defeq \join \lll \fmap\ f
+  $$
+  \pause
+  %
+  And likewise in the Kleisli formulation we can define $\join$:
+  %
+  $$
+  \join \defeq \bind\ \identity
+  $$
+  \pause
+  The laws are logically equivalent. So we get:
+  %
+  $$
+  \var{Monoidal} \simeq \var{Kleisli}
+  $$
+  %
 \end{frame}
 \end{document}

src/Cat/Category.agda

@@ -55,14 +55,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   -- infixl 8 _>>>_
   infixl 10 _<<<_ _>>>_
 
-  -- | Operations on data
+  -- | Reverse arrow composition
-
-  domain : {a b : Object} → Arrow a b → Object
-  domain {a} _ = a
-
-  codomain : {a b : Object} → Arrow a b → Object
-  codomain {b = b} _ = b
-
   _>>>_ : {A B C : Object} → (Arrow A B) → (Arrow B C) → Arrow A C
   f >>> g = g <<< f
 

src/Cat/Category/Product.agda

@@ -1,7 +1,6 @@
 {-# OPTIONS --cubical --caching #-}
 module Cat.Category.Product where
 
-
 open import Cat.Prelude as P hiding (_×_ ; fst ; snd)
 open import Cat.Equivalence