From 2d0dfab12afb9ae0d24a77dcd8e3087592b48c03 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 23 May 2018 18:28:27 +0200 Subject: [PATCH] Remove some TODO-notes, add section on motifs --- doc/conclusion.tex | 38 +++++++++++++------------ doc/cubical.tex | 40 +++++++++++++++----------- doc/discussion.tex | 20 +++++++++++++ doc/implementation.tex | 64 ++++++++++++++++++++++++++---------------- doc/introduction.tex | 22 +++++++-------- 5 files changed, 114 insertions(+), 70 deletions(-) diff --git a/doc/conclusion.tex b/doc/conclusion.tex index 101a94f..a47ca3b 100644 --- a/doc/conclusion.tex +++ b/doc/conclusion.tex @@ -1,22 +1,24 @@ \chapter{Conclusion} -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 -admissible. Cubical Agda is more expressive, but there are certain issues that -arise that are not present in standard Agda. For one thing ITT and standard Agda -enjoys Uniqueness of Identity Proofs (UIP). This is not the case in Cubical -Agda. In stead there exists 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 \TODO{Not mentioned anywhere in the report}. 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 +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 +admissible. Cubical Agda is more expressive, but there are certain +issues that arise that are not present in standard Agda. For one thing +ITT and standard Agda enjoys Uniqueness of Identity Proofs (UIP). This +is not the case in Cubical Agda. In stead there exists 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. This thesis formalized some of the core concepts from category theory including; diff --git a/doc/cubical.tex b/doc/cubical.tex index a4a4c5f..e539d30 100644 --- a/doc/cubical.tex +++ b/doc/cubical.tex @@ -54,17 +54,18 @@ Judgmental equality in Cubical Agda is encapsulated with the type: \Path \tp (P \tp I → \MCU) → P\ 0 → P\ 1 → \MCU \end{equation} % -$I$ is a special data type (\TODO{that also has special computational properties - AFAIK}) called the index set. $I$ can be thought of simply as the interval on -the real numbers from $0$ to $1$. $P$ is a family of types over the index set -$I$. I will sometimes refer to $P$ as the \nomenindex{path space} of some path $p \tp -\Path\ P\ a\ b$. By this token $P\ 0$ then corresponds to the type at the -left-endpoint and $P\ 1$ as the type at the right-endpoint. The type is called -$\Path$ because it is connected with paths in homotopy theory. The intuition -behind this is that $\Path$ describes paths in $\MCU$ -- i.e.\ between types. For -a path $p$ for the point $p\ i$ the index $i$ describes how far along the path -one has moved. An inhabitant of $\Path\ P\ a_0\ a_1$ is a (dependent-) function, -$p$, from the index-space to the path space: +$I$ is a special data type called the index set. $I$ can be thought of +simply as the interval on the real numbers from $0$ to $1$. $P$ is a +family of types over the index set $I$. I will sometimes refer to $P$ +as the \nomenindex{path space} of some path $p \tp \Path\ P\ a\ b$. By +this token $P\ 0$ then corresponds to the type at the left-endpoint +and $P\ 1$ as the type at the right-endpoint. The type is called +$\Path$ because it is connected with paths in homotopy theory. The +intuition behind this is that $\Path$ describes paths in $\MCU$ -- +i.e.\ between types. For a path $p$ for the point $p\ i$ the index $i$ +describes how far along the path one has moved. An inhabitant of +$\Path\ P\ a_0\ a_1$ is a (dependent-) function, $p$, from the +index-space to the path space: % $$ p \tp \prod_{i \tp I} P\ i @@ -194,7 +195,7 @@ indeed both $\top$ and $\bot$ are propositions: The term $\varnothing$ is used here to denote an impossible pattern. It is a theorem that if a mere proposition $A$ is inhabited, then so is it contractible. If it is not inhabited it is equivalent to the empty-type (or false -proposition).\TODO{Cite!!} +proposition).\TODO{Cite} I will refer to a type $A \tp \MCU$ as a \emph{mere} proposition if I want to stress that we have $\isProp\ A$. @@ -242,11 +243,16 @@ Let $\left\Vert A \right\Vert = n$ denote that the level of $A$ is $n$. Proposition: For any homotopic level $n$ this is a mere proposition. % \section{A few lemmas} -Rather than getting into the nitty-gritty details of Agda I venture to take a -more ``combinator-based'' approach. That is, I will use theorems about paths -already that have already been formalized. Specifically the results come from -the Agda library \texttt{cubical} (\TODO{Cite}). I have used a handful of -results from this library as well as contributed a few lemmas myself.\footnote{The module \texttt{Cat.Prelude} lists the upstream dependencies. As well my contribution to \texttt{cubical} can be found in the git logs \TODO{Cite}.} +Rather than getting into the nitty-gritty details of Agda I venture to +take a more ``combinator-based'' approach. That is, I will use +theorems about paths already that have already been formalized. +Specifically the results come from the Agda library \texttt{cubical} +(\cite{cubical-demo}). I have used a handful of results from this +library as well as contributed a few lemmas myself.\footnote{The + module \texttt{Cat.Prelude} lists the upstream dependencies. As well + my contribution to \texttt{cubical} can be found in the git logs + which are available at + \hrefsymb{https://github.com/Saizan/cubical-demo}{\texttt{https://github.com/Saizan/cubical-demo}}.} These theorems are all purely related to homotopy theory and cubical Agda and as such not specific to the formalization of Category Theory. I will present a few diff --git a/doc/discussion.tex b/doc/discussion.tex index e021ff5..3dc101a 100644 --- a/doc/discussion.tex +++ b/doc/discussion.tex @@ -97,10 +97,25 @@ 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 +arises when doing so is that Agda is not able to automatically infer +the family that one wants to do induction over. For instance in the +proof $\var{sym}\ (\var{sym}\ p) ≡ p$ from \ref{eq:sym-invol} the +family that we chose to do induction over was $D\ b'\ p' \defeq +\var{sym}\ (\var{sym}\ p') ≡ p'$. However, if one interactively tries +to give this hole, all the information that Agda can provide is that +one must provide an element of $𝒰$. Agda could be more helpful in this +context, perhaps even infer this family in some situations. In this +very simple example this is of course not a big problem, but there are +examples in the source code where this gets more involved. + \section{Future work} \subsection{Agda \texttt{Prop}} Jesper Cockx' work extending the universe-level-laws for Agda and the \texttt{Prop}-type. +\TODO{Do I want to include this?} \subsection{Compiling Cubical Agda} \label{sec:compiling-cubical-agda} @@ -117,3 +132,8 @@ 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. diff --git a/doc/implementation.tex b/doc/implementation.tex index 0a26bd0..c7604e3 100644 --- a/doc/implementation.tex +++ b/doc/implementation.tex @@ -277,16 +277,19 @@ $i$ becomes the triple: \end{aligned} \end{equation} % -I have found this to be a general pattern when proving things in homotopy type -theory, namely that you have to wrap and unwrap equalities at different levels. -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 \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. +I have found this to be a general pattern when proving things in +homotopy type theory, namely that you have to wrap and unwrap +equalities at different levels. 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 $\prod$-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. 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 @@ -326,8 +329,8 @@ $$ And this finishes the proof that being-a-category is a mere proposition (\ref{eq:propIsPreCategory}). -When we have a proper category we can make precise the notion of ``identifying -isomorphic types'' \TODO{cite Awodey here}. That is, we can construct the +When we have a proper category we can make precise the notion of +``identifying isomorphic types''. That is, we can construct the function: % $$ @@ -345,7 +348,11 @@ terminal objects are propositional: It follows from the usual observation that any two terminal objects are isomorphic - and since categories are univalent, so are they equal. The proof is omitted here, but the curious reader can check the implementation for the -details. \TODO{The proof is a bit fun, should I include it?} +details. It is in the module: +% +\begin{center} +\sourcelink{Cat.Category} +\end{center} \section{Equivalences} \label{sec:equiv} @@ -733,7 +740,7 @@ $x \equiv y$ and $\fst\ x \equiv \fst\ y$: \end{aligned} \end{equation*} % -\TODO{Is it confusing that I use point-free style here?} Here $\var{lemSig}$ is +\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: @@ -744,15 +751,18 @@ the two pairs: \left( \fst\ u \equiv \fst\ v \right) \to u \equiv v \end{align*} % -The proof that these are indeed inverses has been omitted. \TODO{Do I really - want to omit it?}\QED +The proof that these are indeed inverses 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 \prod_{a \tp A} \left( P\ a \simeq -Q\ a \right)$ be given. To prove the equivalence, it suffices to give an -isomorphism between $\sum_{a \tp A} P\ a$ and $\sum_{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$. This is exactly what we can get from -the equivalence $e$.\QED +Now to prove \ref{eq:equivSig}: Let $e \tp \prod_{a \tp A} \left( P\ a +\simeq Q\ a \right)$ be given. To prove the equivalence, it suffices +to give an isomorphism between $\sum_{a \tp A} P\ a$ and $\sum_{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$. +This is exactly what we can get from the equivalence $e$.\QED Lastly we prove \ref{eq:equivIso}. Let $f \tp A \to B$ be given. For the maps we choose: @@ -1050,7 +1060,10 @@ $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). \emph{Proposition} \ref{eq:univ-1} is isomorphic to \ref{eq:univ-2}: -\TODO{Super complicated} +This proof of this has been omitted but can be found in the module: +\begin{center} +\sourcelink{Cat.Categories.Span} +\end{center} \emph{Proposition} \ref{eq:univ-2} is isomorphic to \ref{eq:univ-3}: For this I will show two corollaries of \ref{eq:coeCod}: For an isomorphism $(\iota, @@ -1067,7 +1080,10 @@ f & \equiv g \lll \iota \\ g & \equiv f \lll \inv{\iota} \end{align} % -Proof: \TODO{\ldots} +The proof is omitted but can be found in the module: +\begin{center} +\sourcelink{Cat.Category} +\end{center} Now we can prove the equivalence in the following way: Given $(f, \inv{f}, \var{inv}_f) \tp X \cong Y$ and two heterogeneous paths diff --git a/doc/introduction.tex b/doc/introduction.tex index 853da02..59c1037 100644 --- a/doc/introduction.tex +++ b/doc/introduction.tex @@ -207,14 +207,13 @@ implementations of category theory in Agda: % The contribution of this thesis is to explore how working in a cubical setting will make it possible to prove more things and to reuse proofs and to try and -compare some aspects of this formalization with the existing ones.\TODO{How can - I live up to this?} +compare some aspects of this formalization with the existing ones. There are alternative approaches to working in a cubical setting where one can still have univalence and functional extensionality. One option is to postulate these as axioms. This approach, however, has other shortcomings, e.g. you lose \nomenindex{canonicity} -(\TODO{Pageno!} \cite{huber-2016}). +(\cite[p. 3]{huber-2016}). Another approach is to use the \emph{setoid interpretation} of type theory (\cite{hofmann-1995,huber-2016}). With this approach one works @@ -227,16 +226,17 @@ relation a priori. 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 (\TODO{Citation needed}), is -cumbersome to work with in practice (\cite[p. 4]{huber-2016}) and makes -equational proofs less reusable since equational proofs $a \sim_{X} b$ are -inherently `local' to the extensional set $(X , \sim)$. +This approach has other drawbacks; it does not satisfy all +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 ∼ +f\ y$ for some function $f \tp A → B$ between two extensional sets $A$ +and $B$ it must be shown that $f$ is a groupoid homomorphism. This +makes it very cumbersome to work with in practice (\cite[p. + 4]{huber-2016}). \section{Conventions} -\TODO{Talk a bit about terminology. Find a good place to stuff this little - section.} - In the remainder of this paper I will use the term \nomenindex{Type} to describe -- well, types. Thereby diverging from the notation in Agda where the keyword