diff --git a/README.md b/README.md index 2869967..a865e23 100644 --- a/README.md +++ b/README.md @@ -2,11 +2,17 @@ Description =========== This project aims to formalize some parts of category theory using cubical agda — an extension to agda permitting univalence. To learn more about this -[readthedocs](https://agda.readthedocs.io/en/latest/language/cubical.html). +[read the docs](https://agda.readthedocs.io/en/latest/language/cubical.html). This project draws a lot of inspiration from [the HoTT-book](https://homotopytypetheory.org/book/). +If you want more information about this project, then you're in luck. This is my +masters thesis. Go ahead and read it: + + cd doc/ + make read + Installation ============ @@ -18,7 +24,8 @@ To succesfully compile the following is needed: * [Agda Standard Library](https://github.com/agda/agda-stdlib) * [Cubical](https://github.com/Saizan/cubical-demo/) -[^1]: At least version >= [`707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43`](https://github.com/agda/agda/commit/707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43) +[^1]: At least version >= + [`707ce6042`](https://github.com/agda/agda/commit/707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43) The version of the libraries that this depends on can be shown by executing the following command in the root directory of the project: @@ -31,13 +38,6 @@ versions of these libraries that are compatible with this project. Since this information is only provided as documentation it may also noot be up-to-date so beware. -It's important to have the right version of these - but which one is the right -is in constant flux. It's most likely the newest one. - -I've used git submodules to manage dependencies. Unfortunately Agda does not -allow specifying libraries to be used only as local dependencies. So the -submodules are mostly used for documentation. - You can let Agda know about these libraries by appending them to your global libraries file like so: (NB!: There is a good reason this is not in a makefile. So please verify that you know what you are doing, you probably diff --git a/doc/.gitignore b/doc/.gitignore index bc1675b..dc361bb 100644 --- a/doc/.gitignore +++ b/doc/.gitignore @@ -7,3 +7,6 @@ *.bbl *.blg *.toc +*.idx +*.ilg +*.ind diff --git a/doc/Makefile b/doc/Makefile index ff8e36c..399475b 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -48,3 +48,6 @@ cleanall: clean: latexmk -c + +read: all + xdg-open $(PROJNAME).pdf diff --git a/doc/abstract.tex b/doc/abstract.tex new file mode 100644 index 0000000..04e47d7 --- /dev/null +++ b/doc/abstract.tex @@ -0,0 +1,21 @@ +\chapter*{Abstract} +The usual notion of propositional equality in intensional type-theory is +restrictive. For instance it does not admit functional extensionality or +univalence. This poses a severe limitation on both what is \emph{provable} and +the \emph{re-usability} of proofs. Recent developments have, however, resulted +in cubical type theory which permits a constructive proof of these two important +notions. The programming language Agda has been extended with capabilities for +working in such a cubical setting. This thesis will explore the usefulness of +this extension in the context of category theory. + +The thesis will motivate and explain why propositional equality in cubical Agda +is more expressive than in standard Agda. Alternative approaches to Cubical Agda +will be presented and their pros and cons will be explained. It will emphasize +why it is useful to have a constructive interpretation of univalence. As an +example of this two formulations of monads will be presented: Namely monaeds in +the monoidal form an monads in the Kleisli form. + +Finally the thesis will explain the challenges that a developer will face when +working with cubical Agda and give some techniques to overcome these +difficulties. It will also try to suggest how furhter work can help allievate +some of these challenges. diff --git a/doc/chalmerstitle.sty b/doc/chalmerstitle.sty index a31e8a2..90cd06c 100644 --- a/doc/chalmerstitle.sty +++ b/doc/chalmerstitle.sty @@ -40,11 +40,11 @@ \newcommand*{\subtitle}[1]{\gdef\@subtitle{#1}} %% FRONTMATTER \newcommand*{\myfrontmatter}{% -\newgeometry{top=3cm, bottom=3cm,left=2.25 cm, right=2.25cm} +%% \newgeometry{top=3cm, bottom=3cm,left=2.25 cm, right=2.25cm} \begingroup \thispagestyle{empty} {\Huge\@title}\\[.5cm] -{\Large A formalization of category theory in Cubical Agda}\\[2.5cm] +{\Large A formalization of category theory in Cubical Agda}\\[6cm] \begin{center} \includegraphics[width=\linewidth,keepaspectratio]{isomorphism.png} \end{center} @@ -66,7 +66,7 @@ Master's thesis in Computer Science } \renewcommand*{\maketitle}{% -\begin{titlepage} +%% \begin{titlepage} % TITLE PAGE \newpage @@ -131,5 +131,6 @@ Telephone +46 31 772 1000 \setlength{\parskip}{0.5cm}\\ %Printed by [Name of printing company]\\ Gothenburg, Sweden \the\year -\restoregeometry -\end{titlepage}} +%% \restoregeometry +%% \end{titlepage} +} diff --git a/doc/conclusion.tex b/doc/conclusion.tex index 834e579..d2cfd0b 100644 --- a/doc/conclusion.tex +++ b/doc/conclusion.tex @@ -1,3 +1,55 @@ \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}. 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 +these difficulties, such as based path-induction. -\TODO{\ldots} +This thesis formalized 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 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 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 to demonstrate that any two product objects +in a category are isomorphic. Furthermore the thesis showed two formulations of +monads 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. 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 +%% the path type +%% homotopy levels +%% depdendent paths +%% +%% category theory +%% algebra of functions ~ funExt +%% identify isomorphic types ~ univalence +%% using categories to prove properties +%% computational properties +%% reusability, compositional diff --git a/doc/cubical.tex b/doc/cubical.tex index 8ccd666..43446cd 100644 --- a/doc/cubical.tex +++ b/doc/cubical.tex @@ -1,17 +1,18 @@ \chapter{Cubical Agda} \section{Propositional equality} -In Agda judgmental equality is a feature of the type-system. It's a property of -types that can be checked by computational means. In the example from the +Judgmental equality in Agda is a feature of the type-system. Its something that +can be checked automatically by the type-checker: In the example from the introduction $n + 0$ can be judged to be equal to $n$ simply by expanding the definition of $+$. -Propositional equality on the other hand is defined within the language itself. -Cubical Agda extends the underlying type system (\TODO{Cite someone smarter than -me with a good resource on this}) but introduces a data-type within the -languages. +On the other hand, propositional equality is something defined within the +language itself. Propositional equality cannot be derived automatically. The +normal definition of judgmental equality is an inductive data-type. Cubical Agda +discards this type in favor of a new primitives that has certain computational +properties exclusive to it. Exceprts of the source code relevant to this section can be found in appendix -\ref{sec:app-cubical}. +\S\ref{sec:app-cubical}. \subsection{The equality type} The usual notion of judgmental equality says that given a type $A \tp \MCU$ and @@ -21,7 +22,8 @@ two points of $A$; $a_0, a_1 \tp A$ we can form the type: a_0 \equiv a_1 \tp \MCU \end{align} % -In Agda this is defined as an inductive data-type with the single constructor: +In Agda this is defined as an inductive data-type with the single constructor +for any $a \tp A$: % \begin{align} \refl \tp a \equiv a @@ -29,7 +31,7 @@ In Agda this is defined as an inductive data-type with the single constructor: % For any $a \tp A$. -There also exist a related notion of \emph{heterogeneous} equality where allows +There also exist a related notion of \emph{heterogeneous} equality which allows for equating points of different types. In this case given two types $A, B \tp \MCU$ and two points $a \tp A$, $b \tp B$ we can construct the type: % @@ -37,7 +39,8 @@ for equating points of different types. In this case given two types $A, B \tp a \cong b \tp \MCU \end{align} % -This is likewise defined as an inductive data-type with a single constructors: +This is likewise defined as an inductive data-type with a single constructors +for any $a \tp A$: % \begin{align} \refl \tp a \cong a @@ -47,11 +50,11 @@ In Cubical Agda these two notions are paralleled with homogeneous- and heterogeneous paths respectively. % \subsection{The path type} -In Cubical Agda judgmental equality is encapsulated with the type: +Judgmental equality in Cubical Agda is encapsulated with the type: % -$$ +\begin{equation} \Path \tp (P \tp I → \MCU) → P\ 0 → P\ 1 → \MCU -$$ +\end{equation} % $I$ is a special data-type (\TODO{that also has special computational properties AFAIK}) called the index set. $I$ can be thought of simply as the interval on @@ -62,11 +65,11 @@ left-endpoint and $P\ 1$ as the type at the right-endpoint. The type is called $\Path$ because it is connected with paths in homotopy theory. The intuition behind this is that $\Path$ describes paths in $\MCU$ -- i.e. between types. For a path $p$ for the point $p\ i$ the index $i$ describes how far along the path -one has moved. An inhabitant of $\Path\ P\ a_0\ a_1$ is a (dependent-) -function, $p$, from the index-space to the path-space: +one has moved. An inhabitant of $\Path\ P\ a_0\ a_1$ is a (dependent-) function, +$p$, from the index-space to the path-space: % $$ -p \tp I \to P\ i +p \tp \prod_{i \tp I} P\ i $$ % Which must satisfy being judgmentally equal to $a_0$ (respectively $a_1$) at the @@ -77,16 +80,16 @@ endpoints. I.e.: p\ 1 & = a_1 \end{align*} % -The notion of ``homogeneous equalities'' can be recovered by not letting the -path-space $P$ depend on it's argument: +The notion of ``homogeneous equalities'' is recovered when $P$ does not depend +on its argument: % $$ a_0 \equiv a_1 \defeq \Path\ (\lambda i \to A)\ a_0\ a_1 $$ % For $A \tp \MCU$, $a_0, a_1 \tp A$. I will generally prefer to use the notation -$a_0 \equiv a_1$ when talking about non-dependent paths and use the notation -$\Path\ (\lambda i \to A)\ a_0\ a_1$ when the path-space is of particular +$a \equiv b$ when talking about non-dependent paths and use the notation +$\Path\ (\lambda i \to P\ i)\ a\ b$ when the path-space is of particular interest. With this definition we can also recover reflexivity. That is, for any $A \tp @@ -99,28 +102,63 @@ With this definition we can also recover reflexivity. That is, for any $A \tp \end{aligned} \end{equation} % -Or, in other terms; reflexivity is the path in $A$ that is $a$ at the left -endpoint as well as at the right endpoint. It is inhabited by the path which -stays constantly at $a$ at any index $i$. +Here the path-space is $P \defeq \lambda i \to A$ and it satsifies $P\ i = A$ +definitionally. So to inhabit it, is to give a path $I \to A$ which is +judgmentally $a$ at either endpoint. This is satisfied by the constant path; +i.e. the path that stays at $a$ at any index $i$. -Paths have some other important properties, but they are not the focus of this -thesis. \TODO{Refer the reader somewhere for more info.} +It is also surpisingly easy to show functional extensionality with which we can +construct a path between $f$ and $g$ -- the function defined in the introduction +(section \S\ref{sec:functional-extensionality}). +%% module _ {ℓa ℓb} {A : Set ℓa} {B : A → Set ℓb} where +%% funExt : {f g : (x : A) → B x} → ((x : A) → f x ≡ g x) → f ≡ g +Functional extensionality is the proposition, given a type $A \tp \MCU$, a +family of types $B \tp A \to \MCU$ and functions $f, g \tp \prod_{a \tp A} +B\ a$: % +\begin{equation} +\label{eq:funExt} +\funExt \tp \prod_{a \tp A} f\ a \equiv g\ a \to f \equiv g +\end{equation} +% +%% p = λ i a → p a i +So given $p \tp \prod_{a \tp A} f\ a \equiv g\ a$ we must give a path $f \equiv +g$. That is a function $I \to \prod_{a \tp A} B\ a$. So let $i \tp I$ be given. +We must now give an expression $\phi \tp \prod_{a \tp A} B\ a$ satisfying +$\phi\ 0 \equiv f\ a$ and $\phi\ 1 \equiv g\ a$. This neccesitates that the +expression must be a lambda-abstraction, so let $a \tp A$ be given. Now we can +apply $a$ to $p$ and get the path $p\ a \tp f\ a \equiv g\ a$. And this exactly +satisfied the conditions for $\phi$. In conclustion \ref{eq:funExt} is inhabited +by the term: +% +\begin{equation} +\label{eq:funExt} +\funExt\ p \defeq λ i\ a → p\ a\ i +\end{equation} +% +With this we can now prove the desired equality $f \equiv g$ from section +\S\ref{sec:functional-extensionality}: +% +\begin{align*} + p & \tp f \equiv g \\ + p & \defeq \funExt\ \lambda n \to \refl +\end{align*} +% +Paths have some other important properties, but they are not the focus of +this thesis. \TODO{Refer the reader somewhere for more info.} \section{Homotopy levels} In ITT all equality proofs are identical (in a closed context). This means that, in some sense, any two inhabitants of $a \equiv b$ are ``equally good'' -- they -don't have any interesting structure. This is referred to as uniqueness of -identity proofs. Unfortunately this is orthogonal to univalence that only makes -sense in the absence of UIP. - -In homotopy type theory we have a hierarchy of types based on their ``internal -structure''. At the bottom of this hierarchy we have the set of contractible -types: +do not have any interesting structure. This is referred to as Uniqueness of +Identity Proofs (UIP). Unfortunately it is not possible to have a type-theory +with both univalence and UIP. In stead we have a hierarchy of types with an +increasing amount of homotopic structure. At the bottom of this hierarchy we +have the set of contractible types: % \begin{equation} \begin{aligned} %% \begin{split} -& \isContr && \tp \MCU \to \MCU \\ +& \isContr && \tp \MCU \to \MCU \\ & \isContr\ A && \defeq \sum_{c \tp A} \prod_{a \tp A} a \equiv c %% \end{split} \end{aligned} @@ -128,8 +166,14 @@ types: % The first component of $\isContr\ A$ is called ``the center of contraction''. Under the propositions-as-types interpretation of type-theory $\isContr\ A$ can -be thought of as ``the true proposition $A$''. It is a theorem that if a type is -contractible, then it is isomorphic to the unit-type $\top$. +be thought of as ``the true proposition $A$''. And indeed $\top$ is +contractible: +\begin{equation*} +\var{tt} , \lambda x \to \refl \tp \isContr\ \top +\end{equation*} +% +It is a theorem that if a type is contractible, then it is isomorphic to the +unit-type. The next step in the hierarchy is the set of mere propositions: % @@ -140,10 +184,18 @@ The next step in the hierarchy is the set of mere propositions: \end{aligned} \end{equation} % -$\isProp\ A$ can be thought of as the set of true and false propositions. It is -a result that if a mere proposition $A$ is inhabited, then so is it -contractible. If it is not inhabited it is equivalent to the empty-type (or -false proposition).\TODO{Cite!!} +$\isProp\ A$ can be thought of as the set of true and false propositions. And +indeed both $\top$ and $\bot$ are propositions: +% +\begin{align*} +λ \var{tt}\ \var{tt} → refl & \tp \isProp\ ⊤ \\ +λ\varnothing\ \varnothing & \tp \isProp\ ⊥ +\end{align*} +% +$\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!!} I will refer to a type $A \tp \MCU$ as a \emph{mere} proposition if I want to stress that we have $\isProp\ A$. @@ -157,12 +209,15 @@ Then comes the set of homotopical sets: \end{aligned} \end{equation} % -At this point it should be noted that the term ``set'' is somewhat conflated; -there is the notion of sets from set-theory, in Agda types are denoted -\texttt{Set}. I will use it consistently to refer to a type $A$ as a set exactly -if $\isSet\ A$ is inhabited. +I will not give an example of a set at this point. It turns out that proving +e.g. $\isProp\ \bN$ is not so straight-forward (see \cite[\S3.1.4]{hott-2013}). +There will be examples of sets later in this report. At this point it should be +noted that the term ``set'' is somewhat conflated; there is the notion of sets +from set-theory, in Agda types are denoted \texttt{Set}. I will use it +consistently to refer to a type $A$ as a set exactly if $\isSet\ A$ is a +proposition. -The next step in the hierarchy is, as the reader might've guessed, the type: +As the reader may have guessed the next step in the hierarchy is the type: % \begin{equation} \begin{aligned} @@ -219,10 +274,13 @@ $$ % We have the function: % -$$ +\begin{equation} \pathJ\ P\ p \tp \prod_{a' \tp A} \prod_{p \tp a ≡ a'} P\ a\ p -$$ +\end{equation} % +I will not give an example of using $\pathJ$ here. An application can be found +later in \ref{eq:pathJ-example}. + \subsection{Paths over propositions} \label{sec:lemPropF} Another very useful combinator is $\lemPropF$: @@ -277,8 +335,8 @@ $$ \subsection{Pairs over propositions} \label{sec:propSig} % -$\sum$-types preserve propositionality whenever it's first component is a -proposition, and it's second component is a proposition for all points of in the +$\sum$-types preserve propositionality whenever its first component is a +proposition, and its second component is a proposition for all points of in the left type. % $$ diff --git a/doc/discussion.tex b/doc/discussion.tex index 62564e6..771d4ef 100644 --- a/doc/discussion.tex +++ b/doc/discussion.tex @@ -7,9 +7,9 @@ to very complicated goals. One technique for alleviating this was to prove that certain types are mere propositions. \subsection{Computational properties} -Another aspect (\TODO{That I actually didn't highlight very well in the previous - chapter}) is the computational nature of paths. Say we have formalized this -common result about monads: +Another aspect (\TODO{That I actually did not highlight very well in the + previous chapter}) is the computational nature of paths. Say we have +formalized this common result about monads: \TODO{Some equation\ldots} @@ -26,7 +26,7 @@ disparate areas: The category-theoretic study of monads; and monads as in functional programming. Univalence thus allows one to reuse proofs. You could say that univalence gives the developer two proofs for the price of one. -The introduction (section \ref{sec:context}) mentioned an often +The introduction (section \S\ref{sec:context}) mentioned an often employed-technique for enabling extensional equalities is to use the setoid-interpretation. Nowhere in this formalization has this been necessary, $\Path$ has been used globally in the project as propositional equality. One diff --git a/doc/implementation.tex b/doc/implementation.tex index 2ce0d4e..93c404e 100644 --- a/doc/implementation.tex +++ b/doc/implementation.tex @@ -53,9 +53,15 @@ given type. For the rest of this chapter I will present some of these results. For didactic reasons no source-code has been included in this chapter. To see the formal definitions excerpts of the implementation have been included in appendix -\ref{ch:app-sources}. +\S\ref{ch:app-sources}: +Appendix +\S\ref{sec:app-categories} corresponds to section \S\ref{sec:categories}, +appendix \S\ref{sec:app-products} to section \S\ref{sec:products} +and appendix \S\ref{sec:app-monads} to section \S\ref{sec:monads}. + \section{Categories} +\label{sec:categories} The data for a category consist of a type for the sort of objects; a type for the sort of arrows; an identity arrow and a composition operation for arrows. Another record encapsulates some laws about this data: associativity of @@ -64,7 +70,7 @@ constituents of a category and can be found in typical mathematical expositions on the topic. We, however, impose one further requirement on what it means to be a category, namely that the type of arrows form a set. -Such categories are called \nomen{1-categories}. It's possible to relax this +Such categories are called \nomen{1-categories}. It is possible to relax this requirement. This would lead to the notion of higher categories (\cite[p. 307]{hott-2013}). For the purpose of this project, however, this report will restrict itself to 1-categories. Making based on higher categories would be a @@ -82,15 +88,15 @@ definitions: If we let $p$ be a witness to the identity law, which formally is: \id \comp f \equiv f \x f \comp \id \equiv f \end{equation} % -Then we can construct the identity isomorphism $\var{idIso} \tp \identity, +Then we can construct the identity isomorphism $\idIso \tp \identity, \identity, p \tp A \approxeq A$ for any object $A$. Here $\approxeq$ denotes isomorphism on objects (whereas $\cong$ denotes isomorphism of types). This will -be elaborated further on in sections \ref{sec:equiv} and \ref{sec:univalence}. -Moreover, due to substitution for paths we can construct an isomorphism from -\emph{any} path: +be elaborated further on in sections \S\ref{sec:equiv} and +\S\ref{sec:univalence}. Moreover, due to substitution for paths we can construct +an isomorphism from \emph{any} path: % \begin{equation} -\var{idToIso} \tp A ≡ B → A ≊ B +\idToIso \tp A ≡ B → A ≊ B \end{equation} % The univalence criterion for categories states that this map must be an @@ -106,14 +112,14 @@ Note that \ref{eq:cat-univ} is \emph{not} the same as: % \begin{equation} \label{eq:cat-univalence} -\tag{Univalence, category} +%% \tag{Univalence, category} (A \equiv B) \simeq (A \approxeq B) \end{equation} % However the two are logically equivalent: One can construct the latter from the former simply by ``forgetting'' that $\idToIso$ plays the role of the equivalence. The other direction is more involved and will be discussed in -section \ref{sec:univalence}. +section \S\ref{sec:univalence}. In summary, the definition of a category is the following collection of data: % @@ -127,14 +133,14 @@ In summary, the definition of a category is the following collection of data: And laws: % \begin{align} -\tag{associativity} +%% \tag{associativity} h \lll (g \lll f) ≡ (h \lll g) \lll f \\ -\tag{identity} +%% \tag{identity} \identity \lll f ≡ f \x f \lll \identity ≡ f \\ \label{eq:arrows-are-sets} -\tag{arrows are sets} +%% \tag{arrows are sets} \isSet\ (\Arrow\ A\ B)\\ \tag{\ref{eq:cat-univ}} \isEquiv\ (A \equiv B)\ (A \approxeq B)\ \idToIso @@ -159,12 +165,12 @@ Proving that \ref{eq:identity} is a mere proposition: % There are multiple ways to prove this. Perhaps one of the more intuitive proofs is by way of the `combinators' $\propPi$ and $\propSig$ presented in sections -\ref{sec:propPi} and \ref{sec:propSig}: +\S\ref{sec:propPi} and \S\ref{sec:propSig}: % \begin{align*} -\var{propPi} & \tp \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\prod_{a \tp A} P\ a\right) +\propPi & \tp \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\prod_{a \tp A} P\ a\right) \\ -\var{propSig} & \tp \isProp\ A \to \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\sum_{a \tp A} P\ a\right) +\propSig & \tp \isProp\ A \to \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\sum_{a \tp A} P\ a\right) \end{align*} % So the proof goes like this: We `eliminate' the 3 function abstractions by @@ -180,11 +186,11 @@ us the two obligations: $\isProp\ (\id \comp f \equiv f)$ and $\isProp\ (f \comp set. This example illustrates nicely how we can use these combinators to reason about -`canonical' types like $\sum$ and $\prod$. Similar combinators can be defined -at the other homotopic levels. These combinators are however not applicable in -situations where we want to reason about other types - e.g. types we've defined -ourselves. For instance, after we've proven that all the projections of -pre-categories are propositions, then we would like to bundle this up to show +`canonical' types like $\sum$ and $\prod$. Similar combinators can be defined at +the other homotopic levels. These combinators are however not applicable in +situations where we want to reason about other types - e.g. types we have +defined ourselves. For instance, after we have proven that all the projections +of pre-categories are propositions, then we would like to bundle this up to show that the type of pre-categories is also a proposition. Formally: % \begin{equation} @@ -196,14 +202,13 @@ Where The definition of $\IsPreCategory$ is the triple: % \begin{align*} \var{isAssociative} & \tp \var{IsAssociative}\\ -\var{isIdentity} & \tp \var{IsIdentity}\\ +\isIdentity & \tp \var{IsIdentity}\\ \var{arrowsAreSets} & \tp \var{ArrowsAreSets} \end{align*} % 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 we'll have to use the path-type -directly. +combinators available to help us here. In stead the paths must be used directly. \ref{eq:propIsPreCategory} is judgmentally the same as % @@ -239,21 +244,21 @@ $i$ becomes the triple: \begin{aligned} & \var{propIsAssociative} && a.\var{isAssociative}\ && b.\var{isAssociative} && i \\ - & \var{propIsIdentity} && a.\var{isIdentity}\ - && b.\var{isIdentity} && i \\ + & \propIsIdentity && a.\isIdentity\ + && b.\isIdentity && i \\ & \var{propArrowsAreSets} && a.\var{arrowsAreSets}\ && b.\var{arrowsAreSets} && i \end{aligned} \end{equation} % -I've found this to be a general pattern when proving things in homotopy type +I have found this to be a general pattern when proving things in homotopy type theory, namely that you have to wrap and unwrap equalities at different levels. 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 reverse?) to retrieve the equalities in $a$ and $b$, pattern-match on them to -see that they are both $\var{refl}$ and then close the proof with $\var{refl}$. +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. @@ -279,16 +284,16 @@ we have shown, $\IsPreCategory$ is a proposition. However, even though $\Univalent$ is also a proposition, we cannot use this directly to show the latter. This is because $\isProp$ talks about non-dependent paths. So we need to 'promote' the result that univalence is a proposition to a heterogeneous path. -To this end we can use $\lemPropF$, which was introduced in \ref{sec:lemPropF}. +To this end we can use $\lemPropF$, which was introduced in \S\ref{sec:lemPropF}. -In this case $A = \var{IsIdentity}\ \identity$ and $B = \var{Univalent}$. We've +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: % $$ -\congruence\ \var{isIdentity}\ p +\congruence\ \isIdentity\ p $$ % And this finishes the proof that being-a-category is a mere proposition @@ -361,7 +366,7 @@ $$ \fiber\ f\ b \defeq \sum_{a \tp A} \left( b \equiv f\ a \right) $$ % -I give it's definition here mainly for completeness, because as I stated we can +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. @@ -414,7 +419,7 @@ $$ $$ % That is, we must demonstrate that there is an isomorphism (on types) between -equalities and isomorphisms (on arrows). It's worthwhile to dwell on this for a +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 @@ -441,8 +446,8 @@ an isomorphism $A \approxeq B$ in some category $\bC$ be given. Name the isomorphism $\iota \tp A \to B$ and its inverse $\inv{\iota} \tp B \to A$. Since $\bC$ is a category (and therefore univalent) the isomorphism induces a path $p \tp A \equiv B$. From this equality we can get two further paths: -$p_{\var{dom}} \tp \var{Arrow}\ A\ X \equiv \var{Arrow}\ B\ X$ and -$p_{\var{cod}} \tp \var{Arrow}\ X\ A \equiv \var{Arrow}\ X\ B$. We +$p_{\var{dom}} \tp \Arrow\ A\ X \equiv \Arrow\ B\ X$ and +$p_{\var{cod}} \tp \Arrow\ X\ A \equiv \Arrow\ X\ B$. We then have the following two theorems: % \begin{align} @@ -459,58 +464,68 @@ I will give the proof of the first theorem here, the second one is analogous. % \begin{align*} \var{coe}\ p_{\var{dom}}\ f - & \equiv f \lll \inv{(\var{idToIso}\ p)} && \text{lemma} \\ + & \equiv f \lll \inv{(\idToIso\ p)} && \text{lemma} \\ & \equiv f \lll \inv{\iota} - && \text{$\var{idToIso}$ and $\var{isoToId}$ are inverses}\\ + && \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{(\var{idToIso}\ p)}$ denotes the map $B \to A$ induced by the -isomorphism $\var{idToIso}\ p \tp A \cong B$. The helper-lemma is similar to -what we're trying to prove but talks about paths rather than isomorphisms: +$\iota$ -- $\inv{(\idToIso\ p)}$ denotes the map $B \to A$ induced by the +isomorphism $\idToIso\ p \tp A \cong B$. The helper-lemma is similar to +what we are trying to prove but talks about paths rather than isomorphisms: % \begin{equation} \label{eq:coeDomIso} -\prod_{f \tp \var{Arrow}\ A\ B} \prod_{p \tp A \equiv B} -\var{coe}\ p_{\var{dom}}\ f \equiv f \lll \inv{(\var{idToIso}\ p)} +\prod_{f \tp \Arrow\ A\ B} \prod_{p \tp A \equiv B} +\var{coe}\ p_{\var{dom}}\ f \equiv f \lll \inv{(\idToIso\ p)} \end{equation} % -Again $p_{\var{dom}}$ denotes the path $\var{Arrow}\ A\ X \equiv -\var{Arrow}\ B\ X$ induced by $p$. To prove this statement I let $f$ and $p$ -be given and then invoke based-path-induction. The induction will be based at $A -\tp \var{Object}$, so let $\widetilde{B} \tp \Object$ and $\widetilde{p} \tp -A \equiv \widetilde{B}$ be given. The family that we perform induction over will +Again $p_{\var{dom}}$ denotes the path $\Arrow\ A\ X \equiv +\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 +\equiv \widetilde{B}$ be given. The family that we perform induction over will be: % -$$ -\var{coe}\ {\widetilde{p}}^*\ f +\begin{align} +D\ \widetilde{B}\ \widetilde{p} \defeq + %% \prod_{\widetilde{B} \tp \Object} + %% \prod_{\widetilde{p} \tp A \equiv \widetilde{B}} + \var{coe}\ {\widetilde{p}}^*\ f \equiv -f \lll \inv{(\var{idToIso}\ \widetilde{p})} -$$ -The base-case therefore becomes: +f \lll \inv{(\idToIso\ \widetilde{p})} +\end{align} +The base-case therefore becomes +$d \tp \var{coe}\ \refl^*\ f \equiv f \lll \inv{(\idToIso\ \refl)}$ +and is inhabited by: \begin{align*} -\var{coe}\ {\widetilde{\refl}}^*\ f -& \equiv f \\ -& \equiv f \lll \var{identity} \\ -& \equiv f \lll \inv{(\var{idToIso}\ \widetilde{\refl})} +\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*} % -The first step follows because reflexivity is a neutral element for coercion. -The second step is the identity law in the category. The last step has to do -with the fact that $\var{idToIso}$ is constructed by substituting according to -the supplied path and since reflexivity is also the neutral element for -substitutions we arrive at the desired expression. To close the -based-path-induction we must supply the value ``at the other''. In this case -this is simply $B \tp \Object$ and $p \tp A \equiv B$ which we have. - +To close the based-path-induction we must supply the value ``at the other''. In +this case this is simply $B \tp \Object$ and $p \tp A \equiv B$ which we have. +In summary the proof of \ref{eq:coeDomIso} is the term: +% +\begin{equation} +\label{eq:pathJ-example} +\pathJ\ D\ d\ B\ p +\end{equation} +% And this finishes the proof of \ref{eq:coeDomIso} and thus \ref{eq:coeDom}. % \section{Categories} \subsection{Opposite category} \label{op-cat} -The first category I'll present is a pure construction on categories. Given some -category we can construct it's dual, called the opposite category. Starting with -a simple example allows us to focus on how we work with equivalences and +The first category I will present is a pure construction on categories. Given +some category we can construct its dual, called the opposite category. Starting +with a simple example allows us to focus on how we work with equivalences and univalence in a very simple category where the structure of the category is rather simple. @@ -521,7 +536,7 @@ an arrow from $B$ to $A$ in the underlying category. The identity arrow is the same as the one in the underlying category (they have the same type). Function composition will be reverse function composition from the underlying category. -I'll refer to things in terms of the underlying category, unless they have an +I will refer to things in terms of the underlying category, unless they have an over-bar. So e.g. $\idToIso$ is a function in the underlying category and the corresponding thing is denoted $\wideoverbar{\idToIso}$ in the opposite category. @@ -536,7 +551,7 @@ Since $\rrr$ is reverse function composition this is just the symmetric version of associativity. % $$ -\var{identity} \rrr f \equiv f \x f \rrr identity \equiv f +\identity \rrr f \equiv f \x f \rrr identity \equiv f $$ % This is just the swapped version of identity. @@ -546,38 +561,38 @@ arguments. Or in other words; since $\Arrow\ A\ B$ is a set for all $A\;B \tp \Object$ then so is $Arrow\ B\ A$. Now, to show that this category is univalent is not as straight-forward. Luckily -section \ref{sec:equiv} gave us some tools to work with equivalences. We saw +section \S\ref{sec:equiv} gave us some tools to work with equivalences. We saw that we can prove this category univalent by giving an inverse to $\wideoverbar{\idToIso} \tp (A \equiv B) \to (A \wideoverbar{\approxeq} B)$. From the original category we have that $\idToIso \tp (A \equiv B) \to (A \cong -B)$ is an isomorphism. Let us denote it's inverse with $\isoToId \tp (A +B)$ is an isomorphism. Let us denote its inverse with $\isoToId \tp (A \approxeq B) \to (A \equiv B)$. If we squint we can see what we need is a way to go between $\wideoverbar{\approxeq}$ and $\approxeq$. -An inhabitant of $A \approxeq B$ is simply an arrow $f \tp \var{Arrow}\ A\ B$ -and it's inverse $g \tp \var{Arrow}\ B\ A$. In the opposite category $g$ will +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 $\var{shuffle} \tp (A \approxeq -B) \to (A \wideoverbar{\approxeq} B)$ and $\var{shuffle}^{-1} \tp (A +go in the opposite direction. I name these maps $\shuffle \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 \var{shuffle}$. The proof that they are inverses go as +\defeq \isoToId \comp \shuffle$. The proof that they are inverses go as follows: % \begin{align*} \wideoverbar{\isoToId} \comp \wideoverbar{\idToIso} & = -\isoToId \comp \var{shuffle} \comp \wideoverbar{\idToIso} +\isoToId \comp \shuffle \comp \wideoverbar{\idToIso} \\ %% ≡⟨ cong (λ φ → φ x) (cong (λ φ → η ⊙ shuffle ⊙ φ) (funExt lem)) ⟩ \\ % & \equiv -\isoToId \comp \var{shuffle} \comp \inv{\var{shuffle}} \comp \idToIso +\isoToId \comp \shuffle \comp \inv{\shuffle} \comp \idToIso && \text{lemma} \\ %% ≡⟨⟩ \\ & \equiv \isoToId \comp \idToIso -&& \text{$\var{shuffle}$ is an isomorphism} \\ +&& \text{$\shuffle$ is an isomorphism} \\ & \equiv \identity && \text{$\isoToId$ is an isomorphism} @@ -586,7 +601,7 @@ follows: The other direction is analogous. The lemma used in step 2 of this proof states that $\wideoverbar{idToIso} \equiv -\inv{\var{shuffle}} \comp \idToIso$. This is a rather straight-forward proof +\inv{\shuffle} \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. @@ -594,12 +609,12 @@ 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: % $$ -\prod_{\bC \tp \var{Category}} \left(\bC^{\var{Op}}\right)^{\var{Op}} \equiv \bC +\prod_{\bC \tp \Category} \left(\bC^{\var{Op}}\right)^{\var{Op}} \equiv \bC $$ % -As we've seen the laws in $\left(\bC^{\var{Op}}\right)^{\var{Op}}$ get quite -involved.\footnote{We haven't even seen the full story because we've used this - `interface' for equivalences.} Luckily since being-a-category is a mere +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 @@ -635,7 +650,7 @@ $$ (\var{hA} \equiv \var{hB}) \simeq (\var{hA} \approxeq \var{hB}) $$ % -Which, as we saw in section \ref{sec:univalence}, is sufficient to show that the +Which, as we saw in section \S\ref{sec:univalence}, is sufficient to show that the category is univalent. The way that I have shown this is with a three-step process. For objects $(A, s_A)\; (B, s_B) \tp \Set$ I show the following chain of equivalences: @@ -669,11 +684,11 @@ lemma: Which says that if two type-families are equivalent at all points, then pairs with identical first components and these families as second components will also be equivalent. For our purposes $P \defeq \isEquiv\ A\ B$ and $Q \defeq -\var{Isomorphism}$. So we must finally prove: +\Isomorphism$. So we must finally prove: % \begin{align} \label{eq:equivIso} -\prod_{f \tp A \to B} \left( \isEquiv\ A\ B\ f \simeq \var{Isomorphism}\ f \right) +\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 @@ -716,12 +731,12 @@ choose: % \begin{align*} \var{toIso} - & \tp \isEquiv\ f \to \var{Isomorphism}\ f \\ + & \tp \isEquiv\ f \to \Isomorphism\ f \\ \var{fromIso} - & \tp \var{Isomorphism}\ f \to \isEquiv\ f + & \tp \Isomorphism\ f \to \isEquiv\ f \end{align*} % -As mentioned in section \ref{sec:equiv}. These maps are not in general inverses +As mentioned in section \S\ref{sec:equiv}. These maps are not in general inverses of each other. In stead, we will use the fact that $A$ and $B$ are sets. The first thing we must prove is: % \begin{align*} @@ -732,11 +747,11 @@ For this we can use the fact that being-an-equivalence is a mere proposition. For the other direction: % \begin{align*} - \var{toIso} \comp \var{fromIso} \equiv \identity_{\var{Isomorphism}\ f} + \var{toIso} \comp \var{fromIso} \equiv \identity_{\Isomorphism\ f} \end{align*} % -We will show that $\var{Isomorphism}\ f$ is also a mere proposition. To this -end, let $X\;Y \tp \var{Isomorphism}\ f$ be given. Name the maps $x\;y \tp B +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 \to A$ respectively. Now, the proof that $X$ and $Y$ are the same is a pair of paths: $p \tp x \equiv y$ and $\Path\ (\lambda\; i \to \var{AreInverses}\ f\ (p\ i))\ \mathcal{X}\ \mathcal{Y}$ where $\mathcal{X}$ @@ -777,8 +792,10 @@ where we have a witness to this being a category. This is useful if this library is later extended to talk about higher categories. \section{Products} -In the following I'll demonstrate a technique for using categories to prove -properties. The goal in this section is to show that products are propositions: +\label{sec:products} +In the following a technique for using categories to prove properties will be +demonstrated. The goal in this section is to show that products are +propositions: % $$ \prod_{\bC \tp \Category} \prod_{A\;B \tp \Object} \isProp\ (\var{Product}\ \bC\ A\ B) @@ -789,7 +806,7 @@ and $B$ in the category $\bC$. I do this by constructing a category whose terminal objects are equivalent to products in $\bC$, and since terminal objects 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, -let's recall the definition of products. +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 @@ -815,7 +832,7 @@ $\pi$ is called the product (arrow) of $f$ and $g$. \newcommand\pairB{\mathcal{B}} Given a base category $\bC$ and two objects in this category $\pairA$ and $\pairB$ we can construct the ``pair category'': \TODO{This is a working title, - it's nice to have a name for this thing to refer back to} + it is nice to have a name for this thing to refer back to} The type of objects in this category will be an object in the underlying category, $X$, and two arrows (also from the underlying category) @@ -991,7 +1008,7 @@ isomorphism, and create a path from this: \end{split} \end{align} % -Where $\widetilde{p} \defeq \var{isoToId}\ \var{iso} \tp X \equiv Y$. +Where $\widetilde{p} \defeq \isoToId\ \var{iso} \tp X \equiv Y$. Finally we have the type: % @@ -1063,8 +1080,8 @@ equality principle for arrows in this category (\ref{eq:productEqPrinc}) gives us that it suffices to show that $f$ and $\inv{f}$, this is exactly $\var{inv}_f$. -This concludes the first direction of the isomorphism that we're constructing. -For the other direction we're given just given the isomorphism +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) @@ -1134,7 +1151,7 @@ gory details. % \subsection{Propositionality of products} % -Now that we've constructed the ``pair category'' I'll demonstrate how to use +Now that we have constructed the ``pair category'' I will demonstrate how to use this to prove that products are propositional. I will do this by showing that terminal objects in this category are equivalent to products: % @@ -1145,7 +1162,7 @@ terminal objects in this category are equivalent to products: And as always we do this by constructing an isomorphism: % In the direction $\var{Terminal} → \var{Product}\ ℂ\ \mathcal{A}\ \mathcal{B}$ -we're given a terminal object $X, x_𝒜, x_ℬ$. $X$ Will be the product-object and +we are given a terminal object $X, x_𝒜, x_ℬ$. $X$ Will be the product-object and $x_𝒜, x_ℬ$ will be the product arrows, so it just remains to verify that this is 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 @@ -1214,6 +1231,7 @@ That in any category: \end{align} % \section{Monads} +\label{sec:monads} In this section I present two formulations of monads. The two representations are referred to as the monoidal- and Kleisli- representation respectively or simply monoidal monads and Kleisli monads for short. We then show that the two @@ -1230,8 +1248,8 @@ The monoidal formulation of monads consists of the following data: \label{eq:monad-monoidal-data} \begin{split} \EndoR & \tp \Endo ℂ \\ - \var{pure} & \tp \NT{\EndoR^0}{\EndoR} \\ - \var{join} & \tp \NT{\EndoR^2}{\EndoR} + \pure & \tp \NT{\EndoR^0}{\EndoR} \\ + \join & \tp \NT{\EndoR^2}{\EndoR} \end{split} \end{align} % @@ -1246,10 +1264,10 @@ following laws: \begin{align} \label{eq:monad-monoidal-laws} \begin{split} - \var{join} \lll \fmap\ \var{join} - & ≡ \var{join} \lll \var{join}\ \fmap \\ - \var{join} \lll \var{pure}\ \fmap & ≡ \identity \\ - \var{join} \lll \fmap\ \var{pure} & ≡ \identity + \join \lll \fmap\ \join + & ≡ \join \lll \join\ \fmap \\ + \join \lll \pure\ \fmap & ≡ \identity \\ + \join \lll \fmap\ \pure & ≡ \identity \end{split} \end{align} % @@ -1273,7 +1291,7 @@ The Kleisli-formulation consists of the following data: % The objects $X$ and $Y$ are implicitly universally quantified. -It's interesting to note here that this formulation does not talk about natural +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. % diff --git a/doc/introduction.tex b/doc/introduction.tex index 12ad3b3..a3b5567 100644 --- a/doc/introduction.tex +++ b/doc/introduction.tex @@ -1,30 +1,20 @@ \chapter{Introduction} -Functional extensionality and univalence is not expressible in -\nomen{Intensional Martin Löf Type Theory} (ITT). This poses a severe limitation -on both i. what is \emph{provable} and ii. the \emph{re-usability} of proofs. -Recent developments have, however, resulted in \nomen{Cubical Type Theory} (CTT) -which permits a constructive proof of these two important notions. - -Furthermore an extension has been implemented for the proof assistant Agda -(\cite{agda}, \cite{cubical-agda}) that allows us to work in such a ``cubical -setting''. This thesis will explore the usefulness of this extension in the -context of category theory. -% \section{Motivating examples} % In the following two sections I present two examples that illustrate some limitations inherent in ITT and -- by extension -- Agda. % \subsection{Functional extensionality} +\label{sec:functional-extensionality}% Consider the functions: % \begin{multicols}{2} \noindent \begin{equation*} - f \defeq (n \tp \bN) \mapsto (0 + n \tp \bN) + f \defeq (n \tp \bN) \mto (0 + n \tp \bN) \end{equation*} \begin{equation*} - g \defeq (n \tp \bN) \mapsto (n + 0 \tp \bN) + g \defeq (n \tp \bN) \mto (n + 0 \tp \bN) \end{equation*} \end{multicols} % @@ -33,7 +23,6 @@ This is also called \nomen{judgmental} equality. We call it definitional equality because the \emph{equality} arises from the \emph{definition} of $+$ which is: % -\newcommand{\suc}[1]{\mathit{suc}\ #1} \begin{align*} + & \tp \bN \to \bN \to \bN \\ n + 0 & \defeq n \\ @@ -55,21 +44,21 @@ equivalence of $f$ and $g$ -- even though we can prove them equal for all points. This is exactly the notion of equality of functions that we are interested in; that they are equal for all inputs. We call this \nomen{point-wise equality}, where the \emph{points} of a function refers -to it's arguments. +to its arguments. In the context of category theory functional extensionality is e.g. needed to show that representable functors are indeed functors. The representable functor for a category $\bC$ and a fixed object in $A \in \bC$ is defined to be: % \begin{align*} -\fmap \defeq X \mapsto \Hom_{\bC}(A, X) +\fmap \defeq X \mto \Hom_{\bC}(A, X) \end{align*} % The proof obligation that this satisfies the identity law of functors ($\fmap\ \idFun \equiv \idFun$) thus becomes: % \begin{align*} -\Hom(A, \idFun_{\bX}) = (g \mapsto \idFun \comp g) \equiv \idFun_{\Sets} +\Hom(A, \idFun_{\bX}) = (g \mto \idFun \comp g) \equiv \idFun_{\Sets} \end{align*} % One needs functional extensionality to ``go under'' the function arrow and apply @@ -92,7 +81,7 @@ be performed in ITT. More specifically what we are interested in is a way of identifying \nomen{equivalent} types. I will return to the definition of equivalence later -in section \ref{sec:equiv}, but for now it is sufficient to think of an +in section \S\ref{sec:equiv}, but for now it is sufficient to think of an equivalence as a one-to-one correspondence. We write $A \simeq B$ to assert that $A$ and $B$ are equivalent types. The principle of univalence says that: % diff --git a/doc/isomorphism.png b/doc/isomorphism.png index 03c5a8b..7338c01 100644 Binary files a/doc/isomorphism.png and b/doc/isomorphism.png differ diff --git a/doc/macros.tex b/doc/macros.tex index a5e03db..1733db4 100644 --- a/doc/macros.tex +++ b/doc/macros.tex @@ -12,7 +12,8 @@ \newcommand{\bC}{\mathbb{C}} \newcommand{\bX}{\mathbb{X}} % \newcommand{\to}{\rightarrow} -\newcommand{\mto}{\mapsto} +%% \newcommand{\mto}{\mapsto} +\newcommand{\mto}{\rightarrow} \newcommand{\UU}{\ensuremath{\mathcal{U}}\xspace} \let\type\UU \newcommand{\MCU}{\UU} @@ -32,57 +33,62 @@ } \makeatother \newcommand{\var}[1]{\ensuremath{\mathit{#1}}} -\newcommand{\Hom}{\var{Hom}} -\newcommand{\fmap}{\var{fmap}} -\newcommand{\bind}{\var{bind}} -\newcommand{\join}{\var{join}} -\newcommand{\omap}{\var{omap}} -\newcommand{\pure}{\var{pure}} -\newcommand{\idFun}{\var{id}} -\newcommand{\Sets}{\var{Sets}} -\newcommand{\Set}{\var{Set}} -\newcommand{\hSet}{\var{hSet}} -\newcommand{\id}{\var{id}} -\newcommand{\isEquiv}{\var{isEquiv}} -\newcommand{\idToIso}{\var{idToIso}} -\newcommand{\isSet}{\var{isSet}} -\newcommand{\isContr}{\var{isContr}} -\newcommand{\isGroupoid}{\var{isGroupoid}} -\newcommand{\pathJ}{\var{pathJ}} -\newcommand\Object{\var{Object}} -\newcommand\Functor{\var{Functor}} -\newcommand\isProp{\var{isProp}} -\newcommand\propPi{\var{propPi}} -\newcommand\propSig{\var{propSig}} -\newcommand\PreCategory{\var{PreCategory}} -\newcommand\IsPreCategory{\var{IsPreCategory}} -\newcommand\isIdentity{\var{isIdentity}} -\newcommand\propIsIdentity{\var{propIsIdentity}} -\newcommand\IsCategory{\var{IsCategory}} -\newcommand\Gl{\var{\lambda}} -\newcommand\lemPropF{\var{lemPropF}} -\newcommand\isPreCategory{\var{isPreCategory}} -\newcommand\congruence{\var{cong}} -\newcommand\identity{\var{identity}} -\newcommand\isequiv{\var{isequiv}} -\newcommand\qinv{\var{qinv}} -\newcommand\fiber{\var{fiber}} -\newcommand\shuffle{\var{shuffle}} -\newcommand\Univalent{\var{Univalent}} -\newcommand\refl{\var{refl}} -\newcommand\isoToId{\var{isoToId}} -\newcommand\Isomorphism{\var{Isomorphism}} +\newcommand{\varindex}[1]{\ensuremath{\mathit{#1}}\index{#1}} + +\newcommand{\Hom}{\varindex{Hom}} +\newcommand{\fmap}{\varindex{fmap}} +\newcommand{\bind}{\varindex{bind}} +\newcommand{\join}{\varindex{join}} +\newcommand{\omap}{\varindex{omap}} +\newcommand{\pure}{\varindex{pure}} +\newcommand{\idFun}{\varindex{id}} +\newcommand{\Sets}{\varindex{Sets}} +\newcommand{\Set}{\varindex{Set}} +\newcommand{\hSet}{\varindex{hSet}} +\newcommand{\id}{\varindex{id}} +\newcommand{\isEquiv}{\varindex{isEquiv}} +\newcommand{\idToIso}{\varindex{idToIso}} +\newcommand{\idIso}{\varindex{idIso}} +\newcommand{\isSet}{\varindex{isSet}} +\newcommand{\isContr}{\varindex{isContr}} +\newcommand{\isGroupoid}{\varindex{isGroupoid}} +\newcommand{\pathJ}{\varindex{pathJ}} +\newcommand\Object{\varindex{Object}} +\newcommand\Functor{\varindex{Functor}} +\newcommand\isProp{\varindex{isProp}} +\newcommand\propPi{\varindex{propPi}} +\newcommand\propSig{\varindex{propSig}} +\newcommand\PreCategory{\varindex{PreCategory}} +\newcommand\IsPreCategory{\varindex{IsPreCategory}} +\newcommand\isIdentity{\varindex{isIdentity}} +\newcommand\propIsIdentity{\varindex{propIsIdentity}} +\newcommand\IsCategory{\varindex{IsCategory}} +\newcommand\Gl{\varindex{\lambda}} +\newcommand\lemPropF{\varindex{lemPropF}} +\newcommand\isPreCategory{\varindex{isPreCategory}} +\newcommand\congruence{\varindex{cong}} +\newcommand\identity{\varindex{identity}} +\newcommand\isequiv{\varindex{isequiv}} +\newcommand\qinv{\varindex{qinv}} +\newcommand\fiber{\varindex{fiber}} +\newcommand\shuffle{\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\fst{\var{fst}} -\newcommand\snd{\var{snd}} -\newcommand\Path{\var{Path}} -\newcommand\Category{\var{Category}} +\newcommand\fst{\varindex{fst}} +\newcommand\snd{\varindex{snd}} +\newcommand\Path{\varindex{Path}} +\newcommand\Category{\varindex{Category}} \newcommand\TODO[1]{TODO: \emph{#1}} \newcommand*{\QED}{\hfill\ensuremath{\square}}% \newcommand\uexists{\exists!} -\newcommand\Arrow{\var{Arrow}} -\newcommand\NTsym{\var{NT}} +\newcommand\Arrow{\varindex{Arrow}} +\newcommand\NTsym{\varindex{NT}} \newcommand\NT[2]{\NTsym\ #1\ #2} -\newcommand\Endo[1]{\var{Endo}\ #1} +\newcommand\Endo[1]{\varindex{Endo}\ #1} \newcommand\EndoR{\mathcal{R}} +\newcommand\funExt{\varindex{funExt}} +\newcommand{\suc}[1]{\mathit{suc}\ #1} diff --git a/doc/main.tex b/doc/main.tex index 917f74d..4d01c3a 100644 --- a/doc/main.tex +++ b/doc/main.tex @@ -42,19 +42,15 @@ \institution{\chalmers} \department{Department of Computer Science and Engineering} \researchgroup{Programming Logic Group} -\bibliographystyle{plain} -%% \newtheorem{prop}{Proposition} -\makeatletter -\newcommand*{\rom}[1]{\expandafter\@slowroman\romannumeral #1@} -\makeatother \begin{document} + +\frontmatter \myfrontmatter -\pagenumbering{roman} \maketitle -\addtocontents{toc}{\protect\thispagestyle{empty}} +\input{abstract.tex} \tableofcontents -\pagenumbering{arabic} +\mainmatter % \input{introduction.tex} \input{cubical.tex} @@ -73,4 +69,5 @@ %% \input{planning.tex} %% \input{halftime.tex} \end{appendices} +\printindex \end{document} diff --git a/doc/packages.tex b/doc/packages.tex index 19837af..c203951 100644 --- a/doc/packages.tex +++ b/doc/packages.tex @@ -1,6 +1,8 @@ \usepackage[utf8]{inputenc} \usepackage{natbib} +\bibliographystyle{plain} + \usepackage[ hidelinks, pdfusetitle, @@ -15,8 +17,9 @@ \usepackage{amssymb,amsmath,amsthm,stmaryrd,mathrsfs,wasysym} \usepackage[toc,page]{appendix} \usepackage{xspace} -\usepackage[a4paper]{geometry} - +\usepackage[a4paper,top=3cm,bottom=3cm]{geometry} +\usepackage{makeidx} +\makeindex % \setlength{\parskip}{10pt} % \usepackage{tikz} @@ -85,3 +88,28 @@ \newunicodechar{𝒜}{\textfallback{?}} \newunicodechar{ℬ}{\textfallback{?}} %% \newunicodechar{≊}{\textfallback{≊}} +\makeatletter +\newcommand*{\rom}[1]{\expandafter\@slowroman\romannumeral #1@} +\makeatother +\makeatletter + +\newcommand\frontmatter{% + \cleardoublepage + %\@mainmatterfalse + \pagenumbering{roman}} + +\newcommand\mainmatter{% + \cleardoublepage + % \@mainmattertrue + \pagenumbering{arabic}} + +\newcommand\backmatter{% + \if@openright + \cleardoublepage + \else + \clearpage + \fi + % \@mainmatterfalse + } + +\makeatother diff --git a/doc/sources.tex b/doc/sources.tex index d270c1f..772a037 100644 --- a/doc/sources.tex +++ b/doc/sources.tex @@ -1,15 +1,15 @@ -\chapter{Source code} +\chapter{Source code excerpts} \label{ch:app-sources} In the following a few of the definitions mentioned in the report are included. The following is \emph{not} a verbatim copy of individual modules from the implementation. Rather, this is a redacted and pre-formatted designed for -presentation purposes. It's provided here as a convenience. The actual sources +presentation purposes. Its provided here as a convenience. The actual sources are the only authoritative source. Is something is not clear, please refer to those. -\clearpage \section{Cubical} \label{sec:app-cubical} \begin{figure}[h] +\label{fig:path} \begin{Verbatim} postulate PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ @@ -23,6 +23,7 @@ module _ {ℓ} {A : Set ℓ} where \end{Verbatim} \caption{Excerpt from the cubical library. Definition of the path-type.} \end{figure} +\clearpage % \begin{figure}[h] \begin{Verbatim}