diff --git a/doc/abstract.tex b/doc/abstract.tex index e2bb834..17b3853 100644 --- a/doc/abstract.tex +++ b/doc/abstract.tex @@ -1,21 +1,22 @@ \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 +extensionality nor 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 +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 monads in the -monoidal form and monads in the Kleisli form. +The thesis will motivate the need for univalence 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. As an example of +the application of univalence two formulations of monads will be +presented: Namely monads in the monoidal form and monads in the +Kleisli form and under the univalent interpretation it will be shown +how these are equal. Finally the thesis will explain the challenges that a developer will face when working with cubical Agda and give some techniques to diff --git a/doc/acknowledgements.tex b/doc/acknowledgements.tex new file mode 100644 index 0000000..e4c45e3 --- /dev/null +++ b/doc/acknowledgements.tex @@ -0,0 +1,13 @@ +\chapter*{Acknowledgements} +I would like to thank my supervisor Thierry Coquand for giving me a +chance to work on this interesting topic. I would also like to thank +Andrea Vezzosi for some very long and very insightful meetings during +the project. It is fascinating and almost uncanny how quickly Andrea +can conjure up various proofs. I also want to recognize the support +of Knud Højgaards Fond who graciously sponsored me with a 20.000 DKK +scholarship which helped toward sponsoring the two years I have spent +studying abroad. I would also like to give a warm thanks to my fellow +students Pierre Kraft and Nachiappan Villiappan who have made the time +spent working on the thesis way more enjoyable. Lastly I would like to +give a special thanks to Valentina Méndez who have been a great moral +support throughout the whole process. diff --git a/doc/appendix/abstract-funext.tex b/doc/appendix/abstract-funext.tex index dafb81f..918990c 100644 --- a/doc/appendix/abstract-funext.tex +++ b/doc/appendix/abstract-funext.tex @@ -1,4 +1,4 @@ -\chapter{Abstract functional extensionality} +\chapter{Non-reducing functional extensionality} \label{app:abstract-funext} In two places in my formalization was the computational behaviours of functional extensionality used. The reduction behaviour can be diff --git a/doc/chalmerstitle.sty b/doc/chalmerstitle.sty index 90cd06c..908e13d 100644 --- a/doc/chalmerstitle.sty +++ b/doc/chalmerstitle.sty @@ -46,7 +46,8 @@ {\Huge\@title}\\[.5cm] {\Large A formalization of category theory in Cubical Agda}\\[6cm] \begin{center} -\includegraphics[width=\linewidth,keepaspectratio]{isomorphism.png} +\includegraphics[width=\linewidth,keepaspectratio]{isomorphism.pdf} +%% \includepdf{isomorphism.pdf} \end{center} % Cover text \vfill diff --git a/doc/conclusion.tex b/doc/conclusion.tex index a47ca3b..c4d0d10 100644 --- a/doc/conclusion.tex +++ b/doc/conclusion.tex @@ -8,40 +8,46 @@ 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. +Agda enjoys Uniqueness of Identity Proofs (UIP) though a flag exists +to turn this off, which is the case in Cubical Agda. In stead +there exists a hierarchy of types with increasing \nomen{homotopical + 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; -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. +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. It would have been very +difficult to make a similar proof with setoids. In the formulation we +also saw how paths can be used to extract functions. A path between +two types induce an isomorphism between the two types. This +e.g. permits developers to write a monad instance for a given type +using the Kleisli formulation. By transporting along the path between +the monoidal- and Kleisli- formulation one can reuse all the +operations and results shown for monoidal- monads in the context of +kleisli monads. %% %% problem with inductive type %% overcome with cubical diff --git a/doc/cubical.tex b/doc/cubical.tex index e539d30..40d2beb 100644 --- a/doc/cubical.tex +++ b/doc/cubical.tex @@ -1,29 +1,31 @@ \chapter{Cubical Agda} \section{Propositional equality} -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 $+$. +Judgmental equality in Agda is a feature of the type system. It is +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 $+$. -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. +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 some +new primitives. -The source code can be browsed online and is linked in the beginning -of \S\ref{ch:implementation}. +Most of the source code related with this section is implemented in +\cite{cubical-demo} it can be browsed in hyperlinked and syntax +highlighted HTML online. The links can be found in the beginning of +section \S\ref{ch:implementation}. \subsection{The equality type} -The usual notion of judgmental equality says that given a type $A \tp \MCU$ and -two points of $A$; $a_0, a_1 \tp A$ we can form the type: +The usual notion of judgmental equality says that given a type $A \tp +\MCU$ and two points hereof $a_0, a_1 \tp A$ we can form the type: % \begin{align} a_0 \equiv a_1 \tp \MCU \end{align} % -In Agda this is defined as an inductive data type with the single constructor -for any $a \tp A$: +In Agda this is defined as an inductive data type with the single +constructor $\refl$ that for any $a \tp A$ gives: % \begin{align} \refl \tp a \equiv a @@ -37,8 +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 -for any $a \tp A$: +This likewise has the single constructor $\refl$ that for any $a \tp +A$ gives: % \begin{align} \refl \tp a \cong a @@ -51,28 +53,28 @@ heterogeneous paths respectively. Judgmental equality in Cubical Agda is encapsulated with the type: % \begin{equation} -\Path \tp (P \tp I → \MCU) → P\ 0 → P\ 1 → \MCU +\Path \tp (P \tp \I → \MCU) → P\ 0 → P\ 1 → \MCU \end{equation} % -$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: +The special type $\I$ is called the index set. The index set can be +thought of simply as the interval on the real numbers from $0$ to $1$ +(both inclusive). The family $P$ over $\I$ will be referred to as the +\nomenindex{path space} given some path $p \tp \Path\ P\ a\ b$. By +that token $P\ 0$ corresponds to the type at the left endpoint of $p$. +Likewise $P\ 1$ is the type at the right endpoint. The type is called +$\Path$ because the idea has roots in homotopy theory. The intuition +is that $\Path$ describes\linebreak[1] paths in $\MCU$. I.e.\ paths +between types. For a path $p$ the expression $p\ i$ can be thought of +as a \emph{point} on this path. 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 from the index set to the path space: % $$ -p \tp \prod_{i \tp I} P\ i +p \tp \prod_{i \tp \I} P\ i $$ % -Which must satisfy being judgmentally equal to $a_0$ (respectively $a_1$) at the -endpoints. I.e.: +Which must satisfy being judgmentally equal to $a_0$ at the +left endpoint and equal to $a_1$ at the other end. I.e.: % \begin{align*} p\ 0 & = a_0 \\ @@ -80,80 +82,77 @@ endpoints. I.e.: \end{align*} % The notion of \nomenindex{homogeneous equalities} is recovered when $P$ does not -depend on its argument. That is for $A \tp \MCU$, $a_0, a_1 \tp A$ the +depend on its argument. That is for $A \tp \MCU$ and $a_0, a_1 \tp A$ the homogenous equality between $a_0$ and $a_1$ is the type: % $$ -a_0 \equiv a_1 \defeq \Path\ (\lambda i \to A)\ a_0\ a_1 +a_0 \equiv a_1 \defeq \Path\ (\lambda\;i \to A)\ a_0\ a_1 $$ % -I will generally prefer to use the notation -$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. +I will generally prefer to use the notation $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 \MCU$ and $a \tp A$: % \begin{equation} \begin{aligned} -\refl & \tp \Path (\lambda i \to A)\ a\ a \\ -\refl & \defeq \lambda i \to a +\refl & \tp a \equiv a \\ +\refl & \defeq \lambda\; i \to a \end{aligned} \end{equation} % -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$. +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 is constantly $a$ at any index +$i \tp \I$. -It is also surpisingly easy to show functional extensionality with which we can -construct a path between $f$ and $g$ -- the functions defined in the -introduction (section \S\ref{sec:functional-extensionality}). 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$: +It is also surprisingly easy to show functional extensionality. +Functional extensionality is the proposition that 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$ gives: % \begin{equation} \label{eq:funExt} -\funExt \tp \prod_{a \tp A} f\ a \equiv g\ a \to f \equiv g +\funExt \tp \left(\prod_{a \tp A} f\ a \equiv g\ a \right) \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. +%% p = λ\; i a → p a i +So given $η \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 +apply $a$ to $η$ and get the path $η\ a \tp f\ a \equiv g\ a$. And this exactly +satisfies 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} +\begin{equation*} +\funExt\ η \defeq λ\; i\ a → η\ a\ i +\end{equation*} % -With this we can now prove the desired equality $f \equiv g$ from section -\S\ref{sec:functional-extensionality}: +With $\funExt$ in place we can now construct a path between +$\var{zeroLeft}$ and $\var{zeroRight}$ -- the functions defined in the +introduction \S\ref{sec:functional-extensionality}: % \begin{align*} - p & \tp f \equiv g \\ - p & \defeq \funExt\ \phi + p & \tp \var{zeroLeft} \equiv \var{zeroRight} \\ + p & \defeq \funExt\ \var{zrn} \end{align*} % -Here $\phi \tp \prod_{n \tp \bN} \var{zeroLeft}\ n \equiv -\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.} +Here $\var{zrn}$ is the proof from \ref{eq:zrn}. % \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 -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: +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 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 in cubical Agda we have a hierarchy of types with an increasing +amount of homotopic structure. At the bottom of this hierarchy is the +set of contractible types: % \begin{equation} \begin{aligned} @@ -168,8 +167,9 @@ 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$''. And indeed $\top$ is contractible: +% \begin{equation*} -\var{tt} , \lambda x \to \refl \tp \isContr\ \top +(\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 @@ -188,19 +188,19 @@ One can think of $\isProp\ A$ 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\ ⊥ +(λ\; \var{tt}, \var{tt} → refl) & \tp \isProp\ ⊤ \\ +λ\;\varnothing\ \varnothing & \tp \isProp\ ⊥ \end{align*} % 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). -I will refer to a type $A \tp \MCU$ as a \emph{mere} proposition if I want to +I will refer to a type $A \tp \MCU$ as a \emph{mere proposition} if I want to stress that we have $\isProp\ A$. -Then comes the set of homotopical sets: +The next step in the hierarchy is the set of homotopical sets: % \begin{equation} \begin{aligned} @@ -209,13 +209,14 @@ Then comes the set of homotopical sets: \end{aligned} \end{equation} % -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. +I will not give an example of a set at this point. It turns out that +proving e.g.\ $\isProp\ \bN$ directly is not so straightforward (see +\cite[\S3.1.4]{hott-2013}). Hedberg's theorem states that any type +with decidable equality is a set. 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. As the reader may have guessed the next step in the hierarchy is the type: % @@ -239,34 +240,40 @@ exposition: Proposition: Homotopy levels are cumulative. That is, if $A \tp \MCU$ has homotopy level $n$ then so does it have $n + 1$. -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. +For any level $n$ it is the case that to be of level $n$ 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. +take a more ``combinator-based'' approach. That is I will use +theorems about paths 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}}.} +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 -of these theorems here, as they will be used later in chapter -\ref{ch:implementation} throughout. +These theorems are all purely related to homotopy type theory and as +such not specific to the formalization of Category Theory. I will +present a few of these theorems here as they will be used throughout +chapter \ref{ch:implementation}. They should also give the reader some +intuition about the path type. \subsection{Path induction} \label{sec:pathJ} -The induction principle for paths intuitively gives us a way to reason about a -type family indexed by a path by only considering if said path is $\refl$ (the -\nomen{base case}{path induction}). For \emph{based path induction}, that equality is \emph{based} -at some element $a \tp A$. +The induction principle for paths intuitively gives us a way to reason +about a type family indexed by a path by only considering if said path +is $\refl$ (the \nomen{base case}{path induction}). For \emph{based + path induction}, that equality is \emph{based} at some element $a +\tp A$. -Let a type $A \tp \MCU$ and an element of the type $a \tp A$ be given. $a$ is said to be the base of the induction. Given a family of types: +\pagebreak[3] +\begin{samepage} +Let a type $A \tp \MCU$ and an element of the type $a \tp A$ be +given. $a$ is said to be the base of the induction.\linebreak[3] Given +a family of types: % $$ D \tp \prod_{b \tp A} \prod_{p \tp a ≡ b} \MCU @@ -283,7 +290,8 @@ We have the function: \begin{equation} \pathJ\ D\ d \tp \prod_{b \tp A} \prod_{p \tp a ≡ b} D\ b\ p \end{equation} -% +\end{samepage}% + A simple application of $\pathJ$ is for proving that $\var{sym}$ is an involution. Namely for any set $A \tp \MCU$, points $a, b \tp A$ and a path between them $p \tp a \equiv b$: @@ -293,8 +301,8 @@ between them $p \tp a \equiv b$: \var{sym}\ (\var{sym}\ p) ≡ p \end{equation} % -The proof will be by induction on $p$ and will be based at $a$. That is, $D$ -will be the family: +The proof will be by induction on $p$ and will be based at $a$. That +is $D$ will be the family: % \begin{align*} D & \tp \prod_{b' \tp A} \prod_{p \tp a ≡ b'} \MCU \\ @@ -319,7 +327,7 @@ definitionally. In summary \ref{eq:sym-invol} is inhabited by the term: % Another application of $\pathJ$ is for proving associativity of $\trans$. That is, given a type $A \tp \MCU$, elements of $A$, $a, b, c, d \tp A$ and paths -between them, $p \tp a \equiv b$, $q \tp b \equiv c$ and $r \tp c \equiv d$ we +between them $p \tp a \equiv b$, $q \tp b \equiv c$ and $r \tp c \equiv d$ we have the following: % \begin{equation} @@ -351,49 +359,52 @@ conclusion \ref{eq:cum-trans} is inhabited by the term: \pathJ\ T\ t\ d\ r \end{align*} % -We shall see another application on path induction in \ref{eq:pathJ-example}. +We shall see another application of path induction in \ref{eq:pathJ-example}. \subsection{Paths over propositions} \label{sec:lemPropF} -Another very useful combinator is $\lemPropF$: - -To `promote' this to a dependent path we can use another useful combinator; -$\lemPropF$. Given a type $A \tp \MCU$ and a type family on $A$; $P \tp A \to -\MCU$. Let $\var{propP} \tp \prod_{x \tp A} \isProp\ (P\ x)$ be the proof that -$P$ is a mere proposition for all elements of $A$. Furthermore say we have a -path between some two elements in $A$; $p \tp a_0 \equiv a_1$ then we can built -a heterogeneous path between any two elements of $p_0 \tp P\ a_0$ and $p_1 \tp -P\ a_1$: +Another very useful combinator is $\lemPropF$: Given a type $A \tp +\MCU$ and a type family on $A$; $D \tp A \to \MCU$. Let $\var{propD} +\tp \prod_{x \tp A} \isProp\ (D\ x)$ be the proof that $D$ is a mere +proposition for all elements of $A$. Furthermore say we have a path +between some two elements in $A$; $p \tp a_0 \equiv a_1$ then we can +built a heterogeneous path between any two elements of $d_0 \tp +D\ a_0$ and $d_1 \tp D\ a_1$. % $$ -\lemPropF\ \var{propP}\ p \tp \Path\ (\lambda\; i \mto P\ (p\ i))\ p_0\ p_1 +\lemPropF\ \var{propD}\ p \tp \Path\ (\lambda\; i \mto D\ (p\ i))\ d_0\ d_1 $$ % -This is quite a mouthful. So let me try to show how this is a very general and -useful result. +Note that $d_0$ and $d_1$, though points of the same family, have +different types. This is quite a mouthful. So let me try to show how +this is a very general and useful result. Often when proving equalities between elements of some dependent types -$\lemPropF$ can be used to boil this complexity down to showing that the -dependent parts of the type are mere propositions. For instance, saw we have a type: +$\lemPropF$ can be used to boil this complexity down to showing that +the dependent parts of the type are mere propositions. For instance +say we have a type: % $$ -T \defeq \sum_{a \tp A} P\ a +T \defeq \sum_{a \tp A} D\ a $$ % -For some proposition $P \tp A \to \MCU$. If we want to prove $t_0 \equiv t_1$ -for two elements $t_0, t_1 \tp T$ then this will be a pair of paths: +For some proposition $D \tp A \to \MCU$. That is we have $\var{propD} +\tp \prod_{a \tp A} \isProp\ (D\ a)$. If we want to prove $t_0 \equiv +t_1$ for two elements $t_0, t_1 \tp T$ then this will be a pair of +paths: % % \begin{align*} p \tp & \fst\ t_0 \equiv \fst\ t_1 \\ - & \Path\ (\lambda i \to P\ (p\ i))\ \snd\ t_0 \equiv \snd\ t_1 + & \Path\ (\lambda\; i \to D\ (p\ i))\ (\snd\ t_0)\ (\snd\ t_1) \end{align*} % -Here $\lemPropF$ directly allow us to prove the latter of these: +Here $\lemPropF$ directly allow us to prove the latter of these given +that we have already provided $p$. % $$ -\lemPropF\ \var{propP}\ p - \tp \Path\ (\lambda i \to P\ (p\ i))\ \snd\ t_0 \equiv \snd\ t_1 +\lemPropF\ \var{propD}\ p + \tp \Path\ (\lambda\; i \to D\ (p\ i))\ (\snd\ t_0)\ (\snd\ t_1) $$ % \subsection{Functions over propositions} @@ -407,9 +418,9 @@ $$ \subsection{Pairs over propositions} \label{sec:propSig} % -$\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. +$\sum$-types preserve propositionality whenever its first component is +a proposition, and its second component is a proposition for all +points of the left type. % $$ \mathit{propSig} \tp \isProp\ A \to \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\sum_{a \tp A} P\ a\right) diff --git a/doc/discussion.tex b/doc/discussion.tex index 3dc101a..56177ef 100644 --- a/doc/discussion.tex +++ b/doc/discussion.tex @@ -90,7 +90,7 @@ been put towards proving things that would not have been needed in classical Agda. The proofs that some given type is a proposition were provided as a strategy to simplify some otherwise very complicated proofs (e.g. \ref{eq:proof-prop-IsPreCategory} -and \label{eq:productPath}). Often these proofs would not be this +and \ref{eq:productPath}). Often these proofs would not be this complicated. If the J-rule holds definitionally the proof-assistant can help simplify these goals considerably. The lack of the J-rule has a significant impact on the complexity of these kinds of proofs. @@ -112,11 +112,6 @@ 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} Compilation of program written in Cubical Agda is currently not @@ -137,3 +132,9 @@ in the context of Category Theory. 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. + +\subsection{Proving laws of programs} +Another interesting thing would be to use the Kleisli formulation of +monads to prove properties of functional programs. The existence of +univalence will make it possible to re-use proofs stated in terms of +the monoidal formulation in this setting. diff --git a/doc/implementation.tex b/doc/implementation.tex index 69cba0c..ad2ed63 100644 --- a/doc/implementation.tex +++ b/doc/implementation.tex @@ -1,7 +1,7 @@ \chapter{Category Theory} \label{ch:implementation} -This implementaiton, including this report, is available as open -source software at: +The source code for this formalization, including this report, is +available as open source software at: % \begin{center} \gitlink @@ -17,7 +17,7 @@ link\footnote{% \begin{center} \doclink \end{center} -This implementation formalizes the following concepts: +The concepts formalized in this development are: % \begin{center} \begin{tabular}{ l l } @@ -41,6 +41,7 @@ Span category & \sourcelink{Cat.Categories.Span} \\ \end{tabular} \end{center} % +\begin{samepage} Furthermore the following items have been partly formalized: % \begin{center} @@ -54,70 +55,75 @@ Free category & \sourcelink{Cat.Categories.Free} \\ Monoids & \sourcelink{Cat.Category.Monoid} \\ \end{tabular} \end{center} +\end{samepage}% % 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 -formalized. In stead, I have selected parts of this formalization that +formalized. In stead I have selected parts of this formalization that highlight some interesting proof techniques relevant to doing proofs in Cubical Agda. This chapter will focus on the definition of \emph{categories}, \emph{equivalences}, the \emph{opposite category}, the \emph{category of sets}, \emph{products}, the \emph{span category} and the two formulations of \emph{monads}. -One such technique that is pervasive to this formalization is the idea of -distinguishing types with more or less homotopical structure. To do this I have -followed the following design-principle: I have split concepts up into things -that represent ``data'' and ``laws'' about this data. The idea is that we can -provide a proof that the laws are mere propositions. As an example a category is -defined to have two members: `raw` which is a collection of the data and -`isCategory` which asserts some laws about that data. +One technique employed throughout this formalization is the idea of +distinguishing types with more or less homotopical structure. To do +this I have followed the following design-principle: I have split +concepts up into things that represent \emph{data} and \emph{laws} +about this data. The idea is that we can provide a proof that the laws +are mere propositions. As an example a category is defined to have two +members: $\var{raw}$ which is a collection of the data and +$\var{isCategory}$ which asserts some laws about that data. -This allows me to reason about things in a more ``standard mathematical way'', -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. +This allows me to reason about things in a more ``standard +mathematical way'', 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 reasons no source-code has been included in this chapter. To see the formal definitions the reader is referred to the -implementation which is linked in \S\ref{ch:implementation}. +implementation which is linked in the tables above. \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 -composition, identity law for the identity morphism. These are standard -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. +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 composition, identity law for the identity +morphism. These are standard constituents of a category and can be +found in typical mathematical expositions on the topic. We shall +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}{1-category}. 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\index{1-category}. Generalizing this work to -higher categories would be a very natural possible extension of this work. +Such categories are called \nomen{1-categories}{1-category}. 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 +thesis however, this report will restrict itself to +1-categories\index{1-category}. Generalizing this work to higher +categories would be a very natural extension of this work. Raw categories satisfying all of the above requirements are called a -\nomenindex{pre categories}. As a further requirement to be a proper category we +\nomenindex{pre-categories}. As a further requirement to be a proper category we require it to be univalent. Before we can define this, I must introduce two more definitions: If we let $p$ be a witness to the identity law, which formally is: % \begin{equation} \label{eq:identity} \var{IsIdentity} \defeq - \prod_{A\ B \tp \Object} \prod_{f \tp \Arrow\ A\ B} + \prod_{A, B \tp \Object} \prod_{f \tp \Arrow\ A\ B} \left(\id \lll f \equiv f\right) \x \left(f \lll \id \equiv f\right) \end{equation} % -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 \S\ref{sec:equiv} and -\S\ref{sec:univalence}. Moreover, due to substitution for paths we can construct -an isomorphism from \emph{any} path: +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 on +types). This will 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} \idToIso \tp A ≡ B → A ≊ B @@ -140,12 +146,13 @@ Note that \ref{eq:cat-univ} is \emph{not} the same as: (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 \S\ref{sec:univalence}. +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 \S\ref{sec:univalence}. -In summary, the definition of a category is the following collection of data: +In summary the definition of a category is the following collection of +data: % \begin{align} \Object & \tp \Type \\ @@ -180,19 +187,20 @@ composition (left-to-right, diagrammatic order) is denoted $\rrr$. The objects ($A$, $B$ and $C$) and arrow ($f$, $g$, $h$) are implicitly universally quantified. -With all this in place it is now possible to prove that all the laws are indeed -mere propositions. Most of the proofs simply use the fact that the type of -arrows are sets. This is because most of the laws are a collection of equations -between arrows in the category. And since such a proof does not have any content -exactly because the type of arrows form a set, two witnesses must be the same. -All the proofs are really quite mechanical. Lets have a look at one of them. -Proving that \ref{eq:identity} is a mere proposition: +With all this in place it is now possible to prove that all the laws +are indeed mere propositions. Most of the proofs simply use the fact +that the type of arrows are sets. This is because most of the laws are +a collection of equations between arrows in the category. And since +such a proof does not have any content exactly because the type of +arrows form a set, two witnesses must be the same. All the proofs are +really quite mechanical. Let us have a look at one of them: Proving +that \ref{eq:identity} is a mere proposition: % \begin{equation} \isProp\ \var{IsIdentity} \end{equation} % -There are multiple ways to prove this. Perhaps one of the more intuitive proofs +There are multiple ways to do this. Perhaps one of the more intuitive proofs is by way of the `combinators' $\propPi$ and $\propSig$ presented in sections \S\ref{sec:propPi} and \S\ref{sec:propSig}: % @@ -202,25 +210,26 @@ is by way of the `combinators' $\propPi$ and $\propSig$ presented in sections \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 -applying $\propPi$ three times. So our proof obligation becomes: +The proof goes like this: We `eliminate' the 3 function abstractions +by applying $\propPi$ three times. So our proof obligation becomes: % $$ \isProp\ \left( \left( \id \comp f \equiv f \right) \x \left( f \comp \id \equiv f \right) \right) $$ % Then we eliminate the (non-dependent) sigma-type by applying $\propSig$ giving -us the two obligations: $\isProp\ (\id \comp f \equiv f)$ and $\isProp\ (f \comp +us the two obligations $\isProp\ (\id \comp f \equiv f)$ and $\isProp\ (f \comp \id \equiv f)$ which follows from the type of arrows being a 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 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: +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 have defined ourselves. For +instance, after we have proven that all the projections of +pre-categories are propositions, we would like to bundle this up to +show that the type of pre-categories is also a proposition. Formally: % \begin{equation} \label{eq:propIsPreCategory} @@ -235,19 +244,20 @@ Where The definition of $\IsPreCategory$ is the triple: \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 the paths must be used directly. +Each corresponding to the first three laws for categories. Note that +since $\IsPreCategory$ is not formulated with a chain of sigma-types +we will not have any combinators available to help us here. In stead +the path type must be used directly. -\ref{eq:propIsPreCategory} is judgmentally the same as: +The type \ref{eq:propIsPreCategory} is judgmentally the same as: % $$ -\prod_{a\ b \tp \IsPreCategory} a \equiv b +\prod_{a, b \tp \IsPreCategory} a \equiv b $$ % -So to prove the proposition let $a\ b \tp \IsPreCategory$ be given. To +So to prove the proposition let $a, b \tp \IsPreCategory$ be given. To prove the equality $a \equiv b$ is to give a continuous path from the -index-type into the path-space. I.e.\ a function $I \to +index-type into the path-space. I.e.\ a function $\I \to \IsPreCategory$. This path must satisfy being being judgmentally the same as $a$ at the left endpoint and $b$ at the right endpoint. We know we can form a continuous path between all projections of $a$ and @@ -261,8 +271,8 @@ $$ a.\isIdentity \equiv b.\isIdentity $$ % -So to give the continuous function $I \to \IsPreCategory$, which is our goal, we -introduce $i \tp I$ and proceed by constructing an element of $\IsPreCategory$ +So to give the continuous function $\I \to \IsPreCategory$, which is our goal, we +introduce $i \tp \I$ and proceed by constructing an element of $\IsPreCategory$ by using the fact that all the projections are propositions to generate paths between all projections. Once we have such a path e.g.\ $p \tp a.\isIdentity \equiv b.\isIdentity$ we can eliminate it with $i$ and thus obtain $p\ i \tp @@ -299,9 +309,9 @@ 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 proposition. The type $\IsCategory$ is a record with two fields, a -witness to being a pre category and the univalence condition. Recall +witness to being a pre-category and the univalence condition. Recall that the univalence condition is indexed by the identity-proof. So to -follow the same recipe as above, let $a\ b \tp \IsCategory$ be given, +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: % $$ @@ -463,7 +473,7 @@ equalities and isomorphisms (on arrows). It is worthwhile to dwell on this for a few seconds. This type looks very similar to univalence for types and is therefore perhaps a bit more intuitive to grasp the implications of. Of course univalence for types (which is a proposition -- i.e.\ provable) does not imply -univalence of all pre category since morphisms in a category are not regular +univalence of all pre-category since morphisms in a category are not regular functions -- in stead they can be thought of as a generalization hereof. The univalence criterion therefore is simply a way of restricting arrows to behave similarly to maps. @@ -581,7 +591,7 @@ 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. -Showing that this forms a pre category is rather straightforward. +Showing that this forms a pre-category is rather straightforward. % $$ h \rrr (g \rrr f) \equiv h \rrr g \rrr f @@ -600,7 +610,7 @@ Finally, that the arrows form sets just follows by flipping the order of the 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 +Now, to show that this category is univalent is not as straightforward. Luckily 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)$. @@ -624,7 +634,7 @@ follows: \wideoverbar{\isoToId} \comp \wideoverbar{\idToIso} & = \isoToId \comp \shufflef \comp \wideoverbar{\idToIso} \\ -%% ≡⟨ cong (λ φ → φ x) (cong (λ φ → η ⊙ shuffle ⊙ φ) (funExt lem)) ⟩ \\ +%% ≡⟨ cong (λ \; φ → φ x) (cong (λ \; φ → η ⊙ shuffle ⊙ φ) (funExt lem)) ⟩ \\ % & \equiv \isoToId \comp \shufflef \comp \inv{\shufflef} \comp \idToIso @@ -641,7 +651,7 @@ follows: The other direction is analogous. The lemma used in step 2 of this proof states that $\wideoverbar{idToIso} \equiv -\inv{\shufflef} \comp \idToIso$. This is a rather straight-forward proof +\inv{\shufflef} \comp \idToIso$. This is a rather straightforward proof since being-an-inverse-of is a proposition, so it suffices to show that their first components are equal, but this holds judgmentally. @@ -673,7 +683,7 @@ homotopic sets. This is encapsulated in Agda with the following type: % $$\Set \defeq \sum_{A \tp \MCU} \isSet\ A$$ % -The more straight-forward notion of a category where the objects are types is +The more straightforward notion of a category where the objects are types is not a valid \mbox{(1-)category}. This stems from the fact that types in cubical Agda types can have higher homotopic structure. @@ -681,7 +691,7 @@ Univalence does not follow immediately from univalence for types: % $$(A \equiv B) \simeq (A \simeq B)$$ % -Because here $A\ B \tp \Type$ whereas the objects in this category have the type +Because here $A, B \tp \Type$ whereas the objects in this category have the type $\Set$ so we cannot form the type $\var{hA} \simeq \var{hB}$ for objects $\var{hA}\;\var{hB} \tp \Set$. In stead I show that this category satisfies: @@ -956,7 +966,7 @@ underlying category. Given that $p$ is the chosen proof of % \begin{align} \label{eq:productPath} -λ\ i → d_{\pairA} \lll p\ i ≡ 2 a_{\pairA} × d_{\pairB} \lll p\ i ≡ a_{\pairB} +λ \; i → d_{\pairA} \lll p\ i ≡ 2 a_{\pairA} × d_{\pairB} \lll p\ i ≡ a_{\pairB} \end{align} % And these paths are in the type of the hom-set of the underlying category, so @@ -1006,7 +1016,7 @@ $$ This we get from \ref{eq:productEqPrinc} and the fact that homotopical structure is cumulative. -This finishes the proof that this is a valid pre category. +This finishes the proof that this is a valid pre-category. \subsubsection{Univalence} To prove that this is a proper category it must be shown that it is univalent. @@ -1032,8 +1042,8 @@ The next types will be the triple: \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}} +& \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{split} \end{align} @@ -1045,8 +1055,8 @@ isomorphism, and create a path from this: \label{eq:univ-2} \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}} +& \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} % @@ -1074,7 +1084,7 @@ This proof of this has been omitted but can be found in the module: \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, \inv{\iota}, \var{inv}) \tp A \cong B$, arrows $f \tp \Arrow\ A\ X$, $g \tp -\Arrow\ B\ X$ and a heterogeneous path between them, $q \tp \Path\ (\lambda i +\Arrow\ B\ X$ and a heterogeneous path between them, $q \tp \Path\ (\lambda\; i \to p_{\var{dom}}\ i)\ f\ g$, where $p_{\var{dom}} \tp \Arrow\ A\ X \equiv \Arrow\ B\ X$ is a path induced by $\var{iso}$, we have the following two results @@ -1095,9 +1105,9 @@ 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 % \begin{align*} -p_{\mathcal{A}} & \tp \Path\ (\lambda i \to p_{\var{dom}}\ i)\ x_{\mathcal{A}}\ y_{\mathcal{A}}\\ +p_{\mathcal{A}} & \tp \Path\ (\lambda\; i \to p_{\var{dom}}\ i)\ x_{\mathcal{A}}\ y_{\mathcal{A}}\\ % -q_{\mathcal{B}} & \tp \Path\ (\lambda i \to p_{\var{dom}}\ i)\ x_{\mathcal{B}}\ y_{\mathcal{B}} +q_{\mathcal{B}} & \tp \Path\ (\lambda\; i \to p_{\var{dom}}\ i)\ x_{\mathcal{B}}\ y_{\mathcal{B}} \end{align*} % all as in \ref{eq:univ-2}. I use $p_{\var{dom}}$ here again to mean the path @@ -1163,8 +1173,8 @@ It then remains to construct the two paths: \begin{align} \begin{split} \label{eq:product-paths} -& \Path\ (λ i → \widetilde{p}_{\mathcal{A}}\ i)\ x_{\mathcal{A}}\ y_{\mathcal{A}}\\ -& \Path\ (λ i → \widetilde{p}_{\mathcal{B}}\ i)\ x_{\mathcal{B}}\ y_{\mathcal{B}} +& \Path\ (λ \; i → \widetilde{p}_{\mathcal{A}}\ i)\ x_{\mathcal{A}}\ y_{\mathcal{A}}\\ +& \Path\ (λ \; i → \widetilde{p}_{\mathcal{B}}\ i)\ x_{\mathcal{B}}\ y_{\mathcal{B}} \end{split} \end{align} % @@ -1172,7 +1182,7 @@ This is achieved with the following lemma: % \begin{align} \prod_{a \tp A} \prod_{b \tp B} \prod_{q \tp A \equiv B} \var{coe}\ q\ a ≡ b → -\Path\ (λ i → q\ i)\ a\ b +\Path\ (λ \; i → q\ i)\ a\ b \end{align} % Which is used without proof. See the implementation for the details. @@ -1201,12 +1211,17 @@ the proof uses the fact that isomorphism-of is propositional and that arrows (in both categories) are sets. The reader is referred to the implementation for the gory details. % -\subsection{Propositionality of products} +\subsection{Products are propositions} % Now that we have constructed the span category\index{span 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: +propositions. On the face of it this may seem surprising. Products +look like they are a structure on categories. After all it consist of +a select element and two arrows given some two objects. If formulated +in set theory this would be the case but in the present setting +univalence of categories give us that products are properties. I will +show this by showing that terminal objects in the span category are +equivalent to products: % \begin{align} \var{Terminal} ≃ \var{Product}\ ℂ\ \mathcal{A}\ \mathcal{B} @@ -1248,9 +1263,9 @@ is the proof that $f$ satisfies \ref{eq:pairCondRev}). The proof will be a pair of proofs: % \begin{alignat}{3} - p \tp & \Path\ (\lambda i \to \Arrow\ X\ Y)\quad + p \tp & \Path\ (\lambda\; i \to \Arrow\ X\ Y)\quad && f\quad && y_𝒜 \x y_ℬ \\ - & \Path\ (\lambda i \to \Phi\ (p\ i))\quad + & \Path\ (\lambda\; i \to \Phi\ (p\ i))\quad && \phi_f\quad && \phi_{y_𝒜 \x y_ℬ} \end{alignat} % @@ -1283,7 +1298,7 @@ preserve homotopic levels along with \ref{eq:termProp} we get our final result. That in any category: % \begin{align} -\prod_{A\ B \tp \Object} \isProp\ (\var{Product}\ \bC\ A\ B) +\prod_{A, B \tp \Object} \isProp\ (\var{Product}\ \bC\ A\ B) \end{align} % \section{Functors and natural transformations} diff --git a/doc/introduction.tex b/doc/introduction.tex index 59c1037..d4effb8 100644 --- a/doc/introduction.tex +++ b/doc/introduction.tex @@ -6,22 +6,27 @@ of equality: \nomenindex{judgmental equality} and \nomenindex{propositional equality}. Judgmental equality is a property of the type system. Judgmental equality on the other hand is usually defined \emph{within} the system. When introducing definitions this -report will use the notation $\defeq$. Judgmental equalities written -$=$. For propositional equalities the notation $\equiv$ is used. +report will use the symbol $\defeq$. Judgmental equalities will be +denoted with $=$ and for propositional equalities the notation +$\equiv$ is used. -For judgmental equality there are some properties that it must -satisfy. \nomenindex{sound}, enjoy \nomenindex{canonicity} and be a -\nomen{congruence relation}. Soundness means that things judged to be -equal are equal with respects to the model of the theory (the meta -theory). It must be a congruence relation because otherwise the -relation certainly does not adhere to our notion of equality. One -would be able to conclude things like: $x \equiv y \rightarrow f\ x -\nequiv f\ y$. Canonicity means that any well typed term evaluates to -a \emph{canonical} form. For example for a closed term $e \tp \bN$ it -will be the case that $e$ reduces to $n$ applications of -$\mathit{suc}$ to $0$ for some $n$; $e = \mathit{suc}^n\ 0$. Without -canonicity terms in the language can get ``stuck'' -- meaning that -they do not reduce to a canonical form. +The rules of judgmental equality are related with $β$- and +$η$-reduction which gives a notion of computation in a given type +theory. +% +There are some properties that one usually want judgmental equality to +satisfy. It must be \nomenindex{sound}, enjoy \nomenindex{canonicity} +and be a \nomenindex{congruence relation}. Soundness means that things +judged to be equal are equal with respects to the \nomenindex{model} +of the theory or the \emph{meta theory}. It must be a congruence +relation because otherwise the relation certainly does not adhere to +our notion of equality. One would be able to conclude things like: $x +\equiv y \rightarrow f\ x \nequiv f\ y$. Canonicity means that any +well typed term evaluates to a \emph{canonical} form. For example for +a closed term $e \tp \bN$ it will be the case that $e$ reduces to $n$ +applications of $\mathit{suc}$ to $0$ for some $n$; $e = +\mathit{suc}^n\ 0$. Without canonicity terms in the language can get +``stuck'' meaning that they do not reduce to a canonical form. To work as a programming languages it is necessary for judgmental equality to be \nomenindex{decidable}. Being decidable simply means @@ -34,27 +39,27 @@ is not in general possible to decide the correctness of logical propositions (cf.\ Hilbert's \emph{entscheidigungsproblem}). There are two flavors of type-theory. \emph{Intensional-} and -\emph{extensional-} type theory. Identity types in extensional type -theory are required to be \nomen{propositions}{proposition}. That is, -a type with at most one inhabitant. In extensional type thoery the -principle of reflection +\emph{extensional-} type theory (ITT and ETT respectively). Identity +types in extensional type theory are required to be +\nomen{propositions}{proposition}. That is, a type with at most one +inhabitant. In extensional type theory the principle of reflection % $$a ≡ b → a = b$$ % is enough to make type checking undecidable. This report focuses on -Agda which at a glance can be thought of a version of intensional type -theory. Pattern-matching in regular Agda let's one prove -\nomenindex{axiom K}. Axiom K states that any two identity proofs are -propositionally identical. +Agda which at a glance can be thought of as a version of intensional +type theory. Pattern-matching in regular Agda lets one prove +\nomenindex{Uniqueness of Identity Proofs} (UIP). UIP states that any +two identity proofs are propositionally identical. -The usual notion of propositional equality in \nomenindex{Intensional - Type Theory} (ITT) is quite restrictive. In the next section a few -motivating examples will highlight this. There exist techniques to -circumvent these problems, as we shall see. This thesis will explore -an extension to Agda that redefines the notion of propositional -equality and as such is an alternative to these other techniques. The -extension is called cubical Agda. Cubical Agda drops Axiom K as this -does not permit \nomenindex{functional extensionality} and +The usual notion of propositional equality in ITT is quite +restrictive. In the next section a few motivating examples will +highlight this. There exist techniques to circumvent these problems, +as we shall see. This thesis will explore an extension to Agda that +redefines the notion of propositional equality and as such is an +alternative to these other techniques. The extension is called cubical +Agda. Cubical Agda drops UIP as this does not permit +\nomenindex{functional extensionality} and \nomenindex{univalence}. What makes this extension particularly interesting is that it gives a \emph{constructive} interpretation of univalence. What all this means will be elaborated in the following @@ -69,74 +74,53 @@ some limitations inherent in ITT and -- by extension -- Agda. \label{sec:functional-extensionality}% Consider the functions: % -\begin{multicols}{2} - \noindent% - \begin{equation*}% - f \defeq \lambda\ (n \tp \bN) \to (0 + n \tp \bN) - \end{equation*}% - \begin{equation*}% - g \defeq \lambda\ (n \tp \bN) \to (n + 0 \tp \bN) - \end{equation*}% -\end{multicols}% +\begin{align*}% +\var{zeroLeft} & \defeq \lambda\; (n \tp \bN) \to (0 + n \tp \bN) \\ +\var{zeroRight} & \defeq \lambda\; (n \tp \bN) \to (n + 0 \tp \bN) +\end{align*}% % -The term $n + 0$ is -\nomenindex{definitionally} equal to $n$, which we -write as $n + 0 = n$. This is also called -\nomenindex{judgmental equality}. -We call it definitional equality because the \emph{equality} arises -from the \emph{definition} of $+$ which is: +The term $n + 0$ is \nomenindex{definitionally} equal to $n$, which we +write as $n + 0 = n$. This is also called \nomenindex{judgmental + equality}. We call it definitional equality because the +\emph{equality} arises from the \emph{definition} of $+$ which is: % \begin{align*} - + & \tp \bN \to \bN \to \bN \\ - n + 0 & \defeq n \\ + + & \tp \bN \to \bN \to \bN \\ + n + 0 & \defeq n \\ n + (\suc{m}) & \defeq \suc{(n + m)} \end{align*} % -Note that $0 + n$ is \emph{not} definitionally equal to $n$. $0 + n$ -is in normal form. I.e.; there is no rule for $+$ whose left hand side -matches this expression. We \emph{do}, however, have that they are -\nomen{propositionally}{propositional equality} equal, which we write -as $n + 0 \equiv n$. Propositional equality means that there is a -proof that exhibits this relation. Since equality is a transitive -relation we have that $n + 0 \equiv 0 + n$. - -Unfortunately we don't have $f \equiv g$. There is no way to construct -a proof asserting the obvious equivalence of $f$ and $g$. Actually -showing this is outside the scope of this text. Essentially it would -involve giving a model for our type theory that validates all our -axioms but where $f \equiv g$ is not true. We cannot show that they -are equal, even though we can prove them equal for all points. For -functions this is exactly the notion of equality that we are -interested in: Functions are considered equal when they are equal for -all inputs. This is called \nomenindex{point wise equality}, where the -\emph{points} of a function refer 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 is defined for a fixed category $\bC$ and an -%% object $X \in \bC$. It's map on objects is defined thus: -%% % -%% \begin{align*} -%% \lambda\ A \to \Arrow\ X\ A -%% \end{align*} -%% % -%% That is, it maps objects to arrows. So, it's map on arrows must map an arrow $\Arrow\ A\ B$ to an -%% The map on objects is defined thus: -%% % -%% \begin{align*} -%% \lambda f \to -%% \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}) = (\lambda\ g \to \idFun \comp g) \equiv \idFun_{\Sets} -%% \end{align*} -%% % -%% One needs functional extensionality to ``go under'' the function arrow and apply -%% the (left) identity law of the underlying category to prove $\idFun \comp g -%% \equiv g$ and thus close the goal. +Note that $0 + n$ is \emph{not} definitionally equal to $n$. This is +because $0 + n$ is in normal form. I.e.\ there is no rule for $+$ +whose left hand side matches this expression. We do however have that +they are \nomen{propositionally}{propositional equality} equal, which +we write as $n \equiv n + 0$. Propositional equality means that there +is a proof that exhibits this relation. We can do induction over $n$ +to prove this: +% +\begin{align} +\label{eq:zrn} +\begin{split} +\var{zrn}\ & \tp ∀ n → n ≡ \var{zeroRight}\ n \\ +\var{zrn}\ \var{zero} & \defeq \var{refl} \\ +\var{zrn}\ (\var{suc}\ n) & \defeq \var{cong}\ \var{suc}\ (\var{zrn}\ n) +\end{split} +\end{align} +% +This show that zero is a right neutral element hence the name $\var{zrn}$. +Since equality is a transitive relation we have that $\forall n \to +\var{zeroLeft}\ n \equiv \var{zeroRight}\ n$. Unfortunately we don't +have $\var{zeroLeft} \equiv \var{zeroRight}$. There is no way to +construct a proof asserting the obvious equivalence of +$\var{zeroLeft}$ and $\var{zeroRight}$. Actually showing this is +outside the scope of this text. Essentially it would involve giving a +model for our type theory that validates all our axioms but where +$\var{zeroLeft} \equiv \var{zeroRight}$ is not true. We cannot show +that they are equal even though we can prove them equal for all +points. For functions this is exactly the notion of equality that we +are interested in: Functions are considered equal when they are equal +for all inputs. This is called \nomenindex{pointwise equality}, where +the \emph{points} of a function refer to its arguments. % \subsection{Equality of isomorphic types} % @@ -155,7 +139,6 @@ without thinking twice. Unfortunately such an identification can not be performed in ITT. More specifically what we are interested in is a way of identifying - \nomenindex{equivalent} types. I will return to the definition of equivalence later in section \S\ref{sec:equiv}, but for now it is sufficient to think of an equivalence as a one-to-one correspondence. @@ -165,27 +148,30 @@ The principle of univalence says that: $$\mathit{univalence} \tp (A \simeq B) \simeq (A \equiv B)$$ % In particular this allows us to construct an equality from an equivalence -($\mathit{ua} \tp (A \simeq B) \to (A \equiv B)$) and vice versa. +% +$$\mathit{ua} \tp (A \simeq B) \to (A \equiv B)$$ +% +and vice versa. \section{Formalizing Category Theory} % -The above examples serve to illustrate a limitation of ITT. One case where these -limitations are particularly prohibitive is in the study of Category Theory. At -a glance category theory can be described as ``the mathematical study of -(abstract) algebras of functions'' (\cite{awodey-2006}). By that token -functional extensionality is particularly useful for formulating Category -Theory. In Category theory it is also common to identify isomorphic structures -and univalence gives us a way to make this notion precise. In fact we can -formulate this requirement within our formulation of categories by requiring the -\emph{categories} themselves to be univalent as we shall see. +The above examples serve to illustrate a limitation of ITT. One case +where these limitations are particularly prohibitive is in the study +of Category Theory. At a glance category theory can be described as +``the mathematical study of (abstract) algebras of functions'' +(\cite{awodey-2006}). By that token functional extensionality is +particularly useful for formulating Category Theory. In Category +theory it is also commonplace to identify isomorphic structures and +univalence gives us a way to make this notion precise. In fact we can +formulate this requirement within our formulation of categories by +requiring the \emph{categories} themselves to be univalent as we shall +see in \S\ref{sec:univalence}. \section{Context} \label{sec:context} % The idea of formalizing Category Theory in proof assistants is not new. There -are a multitude of these available online. Just as a first reference see this -question on Math Overflow: \cite{mo-formalizations}. Notably these -implementations of category theory in Agda: +are a multitude of these available online. Notably: % \begin{itemize} \item @@ -217,12 +203,12 @@ other shortcomings, e.g. you lose \nomenindex{canonicity} Another approach is to use the \emph{setoid interpretation} of type theory (\cite{hofmann-1995,huber-2016}). With this approach one works -with \nomenindex{extensional sets} $(X, \sim)$, that is a type $X \tp +with \nomenindex{extensional sets} $(X, \sim)$. That is a type $X \tp \MCU$ and an equivalence relation $\sim\ \tp X \to X \to \MCU$ on that type. Under the setoid interpretation the equivalence relation serve as a sort of ``local'' propositional equality. Since the developer -gets to pick this relation it is not guaranteed to be a congruence -relation a priori. So this must be verified manually by the developer. +gets to pick this relation it is not a\~priori a congruence +relation. So this must be verified manually by the developer. Furthermore, functions between different setoids must be shown to be setoid homomorphism, that is; they preserve the relation. @@ -237,12 +223,14 @@ makes it very cumbersome to work with in practice (\cite[p. 4]{huber-2016}). \section{Conventions} -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 -\texttt{Set} refers to types. -\nomenindex{Set} on the other hand shall refer to the -homotopical notion of a set. I will also leave all universe levels implicit. +In the remainder of this paper I will use the term \nomenindex{Type} +to describe -- well -- types. Thereby departing from the notation in +Agda where the keyword \texttt{Set} refers to types. \nomenindex{Set} +on the other hand shall refer to the homotopical notion of a set. I +will also leave all universe levels implicit. This of course does not +mean that a statement such as $\MCU \tp \MCU$ means that we have +type-in-type but rather that the arguments to the universes are +implicit. And I use the term \nomenindex{arrow} to refer to morphisms in a category, @@ -253,11 +241,13 @@ whereas the terms shall be reserved for talking about type theoretic functions; i.e. functions in Agda. -$\defeq$ will be used for introducing definitions. $=$ will be used to for -judgmental equality and $\equiv$ will be used for propositional equality. +As already noted $\defeq$ will be used for introducing definitions $=$ +will be used to for judgmental equality and $\equiv$ will be used for +propositional equality. All this is summarized in the following table: - +% +\begin{samepage} \begin{center} \begin{tabular}{ c c c } Name & Agda & Notation \\ @@ -277,3 +267,4 @@ Judgmental equality & \null & $̱=$ \\ Propositional equality & \null & $̱\equiv$ \end{tabular} \end{center} +\end{samepage} diff --git a/doc/macros.tex b/doc/macros.tex index 4d872b0..da71215 100644 --- a/doc/macros.tex +++ b/doc/macros.tex @@ -127,3 +127,4 @@ \newcommand\coe{\varindex{coe}} \newcommand\Monoidal{\varindex{Monoidal}} \newcommand\Kleisli{\varindex{Kleisli}} +\newcommand\I{\mathds{I}} diff --git a/doc/main.tex b/doc/main.tex index 2d5ad96..74d37b7 100644 --- a/doc/main.tex +++ b/doc/main.tex @@ -1,4 +1,5 @@ \documentclass[a4paper]{report} +%% \documentclass[tightpage]{preview} %% \documentclass[compact,a4paper]{article} \input{packages.tex} @@ -49,6 +50,7 @@ \myfrontmatter \maketitle \input{abstract.tex} +\input{acknowledgements.tex} \tableofcontents \mainmatter % diff --git a/doc/packages.tex b/doc/packages.tex index ba2ccba..738bf95 100644 --- a/doc/packages.tex +++ b/doc/packages.tex @@ -16,13 +16,14 @@ %% \hypersetup{allbordercolors={darkorange}} \hypersetup{hidelinks} \usepackage{graphicx} +%% \usepackage[active,tightpage]{preview} \usepackage{parskip} \usepackage{multicol} \usepackage{amssymb,amsmath,amsthm,stmaryrd,mathrsfs,wasysym} \usepackage[toc,page]{appendix} \usepackage{xspace} -\usepackage[a4paper,top=3cm,bottom=3cm]{geometry} +\usepackage[paper=a4paper,top=3cm,bottom=3cm]{geometry} \usepackage{makeidx} \makeindex % \setlength{\parskip}{10pt} @@ -83,7 +84,7 @@ \newunicodechar{∨}{\textfallback{∨}} \newunicodechar{∧}{\textfallback{∧}} \newunicodechar{⊔}{\textfallback{⊔}} -\newunicodechar{≊}{\textfallback{≊}} +%% \newunicodechar{≊}{\textfallback{≊}} \newunicodechar{∈}{\textfallback{∈}} \newunicodechar{ℂ}{\textfallback{ℂ}} \newunicodechar{∘}{\textfallback{∘}} diff --git a/doc/presentation.tex b/doc/presentation.tex index 95f73fd..85014b6 100644 --- a/doc/presentation.tex +++ b/doc/presentation.tex @@ -1,4 +1,5 @@ \documentclass[a4paper,handout]{beamer} +\usetheme{metropolis} \beamertemplatenavigationsymbolsempty %% \usecolortheme[named=seagull]{structure} @@ -21,28 +22,28 @@ \framesubtitle{Functional extensionality} Consider the functions \begin{align*} - \var{zeroLeft} & \defeq \lambda (n \tp \bN) \mto (0 + n \tp \bN) \\ - \var{zeroRight} & \defeq \lambda (n \tp \bN) \mto (n + 0 \tp \bN) + \var{zeroLeft} & ≜ \lambda (n \tp \bN) \mto (0 + n \tp \bN) \\ + \var{zeroRight} & ≜ \lambda (n \tp \bN) \mto (n + 0 \tp \bN) \end{align*} \pause We have % $$ - \prod_{n \tp \bN} \var{zeroLeft}\ n \equiv \var{zeroRight}\ n + ∏_{n \tp \bN} \var{zeroLeft}\ n ≡ \var{zeroRight}\ n $$ % \pause But not % $$ - \var{zeroLeft} \equiv \var{zeroRight} + \var{zeroLeft} ≡ \var{zeroRight} $$ % \pause We need % $$ - \funExt \tp \prod_{a \tp A} f\ a \equiv g\ a \to f \equiv g + \funExt \tp ∏_{a \tp A} f\ a ≡ g\ a → f ≡ g $$ \end{frame} \begin{frame} @@ -52,20 +53,20 @@ $\{x \mid \phi\ x \land \psi\ x\}$ \pause - If we show $\forall x . \psi\ x \equiv \top$ + If we show $∀ x . \psi\ x ≡ \top$ then we want to conclude - $\{x \mid \phi\ x \land \psi\ x\} \equiv \{x \mid \phi\ x\}$ + $\{x \mid \phi\ x \land \psi\ x\} ≡ \{x \mid \phi\ x\}$ \pause We need univalence: - $$(A \simeq B) \simeq (A \equiv B)$$ + $$(A ≃ B) ≃ (A ≡ B)$$ \pause % - We will return to $\simeq$, but for now think of it as an + We will return to $≃$, 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) \\ - \var{toEquiv} & \tp (A \equiv B) \to (A \simeq B) + \var{toPath} & \tp (A ≃ B) → (A ≡ B) \\ + \var{toEquiv} & \tp (A ≡ B) → (A ≃ B) \end{align*} \end{frame} \begin{frame} @@ -76,11 +77,11 @@ \Path \tp (P \tp I → \MCU) → P\ 0 → P\ 1 → \MCU \end{equation*} \pause - For $P \tp I \to \MCU$, $A \tp \MCU$ and $a_0, a_1 \tp A$ + For $P \tp I → \MCU$, $A \tp \MCU$ and $a_0, a_1 \tp A$ inhabitants of $\Path\ P\ a_0\ a_1$ are like functions % $$ - p \tp \prod_{i \tp I} P\ i + p \tp ∏_{i \tp I} P\ i $$ % Which satisfy $p\ 0 & = a_0$ and $p\ 1 & = a_1$ @@ -88,46 +89,46 @@ Homogenous paths $$ - a_0 \equiv a_1 \defeq \Path\ (\var{const}\ A)\ a_0\ a_1 + a_0 ≡ a_1 ≜ \Path\ (\var{const}\ A)\ a_0\ a_1 $$ \end{frame} \begin{frame} \frametitle{Paths} \framesubtitle{Functional extenstionality} $$ - \funExt & \tp \prod_{a \tp A} f\ a \equiv g\ a \to f \equiv g + \funExt & \tp ∏_{a \tp A} f\ a ≡ g\ a → f ≡ g $$ \pause $$ - \funExt\ p \defeq λ i\ a → p\ a\ i + \funExt\ p ≜ λ i\ a → p\ a\ i $$ \pause $$ \funExt\ (\var{const}\ \refl) \tp - \var{zeroLeft} \equiv \var{zeroRight} + \var{zeroLeft} ≡ \var{zeroRight} $$ \end{frame} \begin{frame} \frametitle{Paths} \framesubtitle{Homotopy levels} \begin{align*} - & \isContr && \tp \MCU \to \MCU \\ - & \isContr\ A && \defeq \sum_{c \tp A} \prod_{a \tp A} a \equiv c + & \isContr && \tp \MCU → \MCU \\ + & \isContr\ A && ≜ ∑_{c \tp A} ∏_{a \tp A} a ≡ c \end{align*} \pause \begin{align*} - & \isProp && \tp \MCU \to \MCU \\ - & \isProp\ A && \defeq \prod_{a_0, a_1 \tp A} a_0 \equiv a_1 + & \isProp && \tp \MCU → \MCU \\ + & \isProp\ A && ≜ ∏_{a_0, a_1 \tp A} a_0 ≡ a_1 \end{align*} \pause \begin{align*} - & \isSet && \tp \MCU \to \MCU \\ - & \isSet\ A && \defeq \prod_{a_0, a_1 \tp A} \isProp\ (a_0 \equiv a_1) + & \isSet && \tp \MCU → \MCU \\ + & \isSet\ A && ≜ ∏_{a_0, a_1 \tp A} \isProp\ (a_0 ≡ a_1) \end{align*} \begin{align*} - & \isGroupoid && \tp \MCU \to \MCU \\ - & \isGroupoid\ A && \defeq \prod_{a_0, a_1 \tp A} \isSet\ (a_0 \equiv a_1) + & \isGroupoid && \tp \MCU → \MCU \\ + & \isGroupoid\ A && ≜ ∏_{a_0, a_1 \tp A} \isSet\ (a_0 ≡ a_1) \end{align*} \end{frame} \begin{frame} @@ -135,7 +136,7 @@ \framesubtitle{A few lemmas} Let $D$ be a type-family: $$ - D \tp \prod_{b \tp A} \prod_{p \tp a ≡ b} \MCU + D \tp ∏_{b \tp A} ∏_{p \tp a ≡ b} \MCU $$ % \pause @@ -149,7 +150,7 @@ We then have the function: % $$ - \pathJ\ D\ d \tp \prod_{b \tp A} \prod_{p \tp a ≡ b} D\ b\ p + \pathJ\ D\ d \tp ∏_{b \tp A} ∏_{p \tp a ≡ b} D\ b\ p $$ \end{frame} \begin{frame} @@ -158,9 +159,9 @@ Given \begin{align*} A & \tp \MCU \\ - P & \tp A \to \MCU \\ - \var{propP} & \tp \prod_{x \tp A} \isProp\ (P\ x) \\ - p & \tp a_0 \equiv a_1 \\ + P & \tp A → \MCU \\ + \var{propP} & \tp ∏_{x \tp A} \isProp\ (P\ x) \\ + p & \tp a_0 ≡ a_1 \\ p_0 & \tp P\ a_0 \\ p_1 & \tp P\ a_1 \end{align*} @@ -176,17 +177,17 @@ \begin{frame} \frametitle{Paths} \framesubtitle{A few lemmas} - $\prod$ preserves $\isProp$: + $∏$ preserves $\isProp$: $$ \mathit{propPi} \tp - \left(\prod_{a \tp A} \isProp\ (P\ a)\right) - \to \isProp\ \left(\prod_{a \tp A} P\ a\right) + \left(∏_{a \tp A} \isProp\ (P\ a)\right) + → \isProp\ \left(∏_{a \tp A} P\ a\right) $$ \pause - $\sum$ preserves $\isProp$: + $∑$ preserves $\isProp$: $$ - \mathit{propSig} \tp \isProp\ A \to \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\sum_{a \tp A} P\ a\right) + \mathit{propSig} \tp \isProp\ A → \left(∏_{a \tp A} \isProp\ (P\ a)\right) → \isProp\ \left(∑_{a \tp A} P\ a\right) $$ \end{frame} \begin{frame} @@ -195,9 +196,9 @@ Data: \begin{align*} \Object & \tp \Type \\ - \Arrow & \tp \Object \to \Object \to \Type \\ + \Arrow & \tp \Object → \Object → \Type \\ \identity & \tp \Arrow\ A\ A \\ - \lll & \tp \Arrow\ B\ C \to \Arrow\ A\ B \to \Arrow\ A\ C + \lll & \tp \Arrow\ B\ C → \Arrow\ A\ B → \Arrow\ A\ C \end{align*} % \pause @@ -208,7 +209,7 @@ $$ $$ (\identity \lll f ≡ f) - \x + × (f \lll \identity ≡ f) $$ \pause @@ -221,7 +222,7 @@ \frametitle{Pre categories} \framesubtitle{Propositionality} $$ - \isProp\ \left( (\identity \comp f \equiv f) \x (f \comp \identity \equiv f) \right) + \isProp\ \left( (\identity \comp f ≡ f) × (f \comp \identity ≡ f) \right) $$ \pause \begin{align*} @@ -247,14 +248,17 @@ \frametitle{Categories} \framesubtitle{Univalence} \begin{align*} - \var{IsIdentity} & \defeq - \prod_{A\ B \tp \Object} \prod_{f \tp \Arrow\ A\ B} \phi\ f + \var{IsIdentity} & ≜ + ∏_{A\ B \tp \Object} ∏_{f \tp \Arrow\ A\ B} \phi\ f %% \\ - %% & \mathrel{\ } \identity \lll f \equiv f \x f \lll \identity \equiv f + %% & \mathrel{\ } \identity \lll f ≡ f × f \lll \identity ≡ f \end{align*} where $$ - \phi\ f \defeq \identity \lll f \equiv f \x f \lll \identity \equiv f + \phi\ f ≜ \identity + ( \lll f ≡ f ) + × + ( f \lll \identity ≡ f) $$ \pause Let $\approxeq$ denote ismorphism of objects. We can then construct @@ -271,29 +275,29 @@ For a category to be univalent we require this to be an equivalence: % $$ - \isEquiv\ (A \equiv B)\ (A \approxeq B)\ \idToIso + \isEquiv\ (A ≡ B)\ (A \approxeq B)\ \idToIso $$ % \end{frame} \begin{frame} \frametitle{Categories} \framesubtitle{Univalence, cont'd} - $$\isEquiv\ (A \equiv B)\ (A \approxeq B)\ \idToIso$$ + $$\isEquiv\ (A ≡ B)\ (A \approxeq B)\ \idToIso$$ \pause% - $$(A \equiv B) \simeq (A \approxeq B)$$ + $$(A ≡ B) ≃ (A \approxeq B)$$ \pause% - $$(A \equiv B) \cong (A \approxeq B)$$ + $$(A ≡ B) ≅ (A \approxeq B)$$ \pause% Name the above maps: $$\idToIso \tp A ≡ B → A ≊ B$$ % - $$\isoToId \tp (A \approxeq B) \to (A \equiv B)$$ + $$\isoToId \tp (A \approxeq B) → (A ≡ B)$$ \end{frame} \begin{frame} \frametitle{Categories} \framesubtitle{Propositionality} $$ - \isProp\ \IsCategory = \prod_{a, b \tp \IsCategory} a \equiv b + \isProp\ \IsCategory = ∏_{a, b \tp \IsCategory} a ≡ b $$ \pause So, for @@ -303,8 +307,8 @@ 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 + p & \tp a.\isPreCategory ≡ b.\isPreCategory \\ + & \mathrel{\ } \Path\ (\lambda\; i → (p\ i).Univalent)\ a.\isPreCategory\ b.\isPreCategory \end{align*} \end{frame} \begin{frame} @@ -313,17 +317,17 @@ First path given by: $$ p - \defeq + ≜ \var{propIsPreCategory}\ a\ b \tp - a.\isPreCategory \equiv b.\isPreCategory + a.\isPreCategory ≡ 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}$. + Univalence is indexed by an identity proof. So $A ≜ + IsIdentity\ identity$ and $B ≜ \var{Univalent}$. \pause % $$ @@ -342,16 +346,16 @@ The isomorphism induces the path % $$ - p \defeq \idToIso\ (\iota, \inv{\iota}) \tp A \equiv B + p ≜ \idToIso\ (\iota, \inv{\iota}) \tp A ≡ B $$ % \pause and consequently an arrow: % $$ - p_{\var{dom}} \defeq \congruence\ (λ x → \Arrow\ x\ X)\ p + p_{\var{dom}} ≜ \congruence\ (λ x → \Arrow\ x\ X)\ p \tp - \Arrow\ A\ X \equiv \Arrow\ B\ X + \Arrow\ A\ X ≡ \Arrow\ B\ X $$ % \pause @@ -360,8 +364,8 @@ \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} + ∏_{f \tp A → X} + \var{coe}\ p_{\var{dom}}\ f ≡ f \lll \inv{\iota} \end{align} \end{frame} \begin{frame} @@ -369,23 +373,23 @@ \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} + & ≡ f \lll \inv{(\idToIso\ p)} && \text{By path-induction} \\ + & ≡ 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. + \tp A ≡ \widetilde{B}$ be given. % \pause % Define the family: % $$ - D\ \widetilde{B}\ \widetilde{p} \defeq + D\ \widetilde{B}\ \widetilde{p} ≜ \var{coe}\ \widetilde{p}_{\var{dom}}\ f - \equiv + ≡ f \lll \inv{(\idToIso\ \widetilde{p})} $$ \pause @@ -393,7 +397,7 @@ The base-case becomes: $$ d \tp D\ A\ \refl = - \var{coe}\ \refl_{\var{dom}}\ f \equiv f \lll \inv{(\idToIso\ \refl)} + \var{coe}\ \refl_{\var{dom}}\ f ≡ f \lll \inv{(\idToIso\ \refl)} $$ \end{frame} \begin{frame} @@ -401,17 +405,17 @@ \framesubtitle{A theorem, proof, cont'd} $$ d \tp - \var{coe}\ \refl_{\var{dom}}\ f \equiv f \lll \inv{(\idToIso\ \refl)} + \var{coe}\ \refl_{\var{dom}}\ f ≡ f \lll \inv{(\idToIso\ \refl)} $$ \pause \begin{align*} \var{coe}\ \refl^*\ f - & \equiv f + & ≡ f && \text{$\refl$ is a neutral element for $\var{coe}$}\\ - & \equiv f \lll \identity \\ - & \equiv f \lll \var{subst}\ \refl\ \identity + & ≡ f \lll \identity \\ + & ≡ f \lll \var{subst}\ \refl\ \identity && \text{$\refl$ is a neutral element for $\var{subst}$}\\ - & \equiv f \lll \inv{(\idToIso\ \refl)} + & ≡ f \lll \inv{(\idToIso\ \refl)} && \text{By definition of $\idToIso$}\\ \end{align*} \pause @@ -429,7 +433,7 @@ \pause Objects: $$ - \sum_{X \tp Object} \Arrow\ X\ \pairA × \Arrow\ X\ \pairB + ∑_{X \tp Object} \Arrow\ X\ \pairA × \Arrow\ X\ \pairB $$ \pause % @@ -437,9 +441,9 @@ $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} + ∑_{f \tp \Arrow\ A\ B} + b_{\pairA} \lll f ≡ a_{\pairA} × + b_{\pairB} \lll f ≡ a_{\pairB} $$ \end{frame} \begin{frame} @@ -447,25 +451,25 @@ \framesubtitle{Univalence} \begin{align*} \label{eq:univ-0} - (X , x_{\mathcal{A}} , x_{\mathcal{B}}) ≡ (Y , y_{\mathcal{A}} , y_{\mathcal{B}}) + (X , x_{𝒜} , x_{ℬ}) ≡ (Y , y_{𝒜} , y_{ℬ}) \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}} + p \tp & X ≡ Y \\ + & \Path\ (λ i → \Arrow\ (p\ i)\ 𝒜)\ x_{𝒜}\ y_{𝒜} \\ + & \Path\ (λ i → \Arrow\ (p\ i)\ ℬ)\ x_{ℬ}\ y_{ℬ} \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}} + & \Path\ (λ i → \Arrow\ (\widetilde{p}\ i)\ 𝒜)\ x_{𝒜}\ y_{𝒜} \\ + & \Path\ (λ i → \Arrow\ (\widetilde{p}\ i)\ ℬ)\ x_{ℬ}\ y_{ℬ} \end{split} \end{align*} \begin{align*} - (X , x_{\mathcal{A}} , x_{\mathcal{B}}) ≊ (Y , y_{\mathcal{A}} , y_{\mathcal{B}}) + (X , x_{𝒜} , x_{ℬ}) ≊ (Y , y_{𝒜} , y_{ℬ}) \end{align*} \end{frame} \begin{frame} @@ -475,12 +479,12 @@ \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}}) + (X, x_{𝒜}, x_{ℬ}) \approxeq (Y, y_{𝒜}, y_{ℬ}) \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}} + & \Path\ (λ i → \Arrow\ (\widetilde{p}\ i)\ 𝒜)\ x_{𝒜}\ y_{𝒜} \\ + & \Path\ (λ i → \Arrow\ (\widetilde{p}\ i)\ ℬ)\ x_{ℬ}\ y_{ℬ} \end{split} \end{align*} \pause @@ -503,8 +507,8 @@ % \begin{align*} \begin{split} - \widetilde{p} & \tp X \equiv Y \\ - \widetilde{p}_{\mathcal{A}} & \tp \Arrow\ X\ \mathcal{A} \equiv \Arrow\ Y\ \mathcal{A} \\ + \widetilde{p} & \tp X ≡ Y \\ + \widetilde{p}_{𝒜} & \tp \Arrow\ X\ 𝒜 ≡ \Arrow\ Y\ 𝒜 \\ \end{split} \end{align*} % @@ -517,7 +521,7 @@ \begin{align*} \begin{split} \label{eq:product-paths} - & \Path\ (λ i → \widetilde{p}_{\mathcal{A}}\ i)\ x_{\mathcal{A}}\ y_{\mathcal{A}} + & \Path\ (λ i → \widetilde{p}_{𝒜}\ i)\ x_{𝒜}\ y_{𝒜} \end{split} \end{align*} \pause @@ -525,9 +529,9 @@ This is achieved with the following lemma: % \begin{align*} - \prod_{q \tp A \equiv B} \var{coe}\ q\ x_{\mathcal{A}} ≡ y_{\mathcal{A}} + ∏_{q \tp A ≡ B} \var{coe}\ q\ x_{𝒜} ≡ y_{𝒜} → - \Path\ (λ i → q\ i)\ x_{\mathcal{A}}\ y_{\mathcal{A}} + \Path\ (λ i → q\ i)\ x_{𝒜}\ y_{𝒜} \end{align*} % Which is used without proof.\pause @@ -535,15 +539,15 @@ So the construction reduces to: % \begin{align*} - \var{coe}\ \widetilde{p}_{\mathcal{A}}\ x_{\mathcal{A}} ≡ y_{\mathcal{A}} + \var{coe}\ \widetilde{p}_{𝒜}\ x_{𝒜} ≡ y_{𝒜} \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} + \var{coe}\ \widetilde{p}_{𝒜}\ x_{𝒜} + & ≡ x_{𝒜} \lll \fst\ \inv{f} && \text{\ref{eq:coeDom}} \\ + & ≡ y_{𝒜} && \text{Property of span category} \end{align*} \end{frame} \begin{frame} @@ -556,13 +560,13 @@ % We can show: \begin{align*} - \var{Terminal} ≃ \var{Product}\ ℂ\ \mathcal{A}\ \mathcal{B} + \var{Terminal} ≃ \var{Product}\ ℂ\ 𝒜\ ℬ \end{align*} \pause And since equivalences preserve homotopy levels we get: % $$ - \isProp\ \left(\var{Product}\ \bC\ \mathcal{A}\ \mathcal{B}\right) + \isProp\ \left(\var{Product}\ \bC\ 𝒜\ ℬ\right) $$ \end{frame} \begin{frame} @@ -595,7 +599,7 @@ % \begin{align*} \omapR & \tp \Object → \Object \\ - \pure & \tp % \prod_{X \tp Object} + \pure & \tp % ∏_{X \tp Object} \Arrow\ X\ (\omapR\ X) \\ \bind & \tp \Arrow\ X\ (\omapR\ Y) @@ -610,7 +614,7 @@ \Arrow\ B\ (\omapR\ C) → \Arrow\ A\ (\omapR\ C) \\ - f \fish g & \defeq f \rrr (\bind\ g) + f \fish g & ≜ f \rrr (\bind\ g) \end{align*} \pause % @@ -629,20 +633,20 @@ In the monoidal formulation we can define $\bind$: % $$ - \bind\ f \defeq \join \lll \fmap\ f + \bind\ f ≜ \join \lll \fmap\ f $$ \pause % And likewise in the Kleisli formulation we can define $\join$: % $$ - \join \defeq \bind\ \identity + \join ≜ \bind\ \identity $$ \pause The laws are logically equivalent. So we get: % $$ - \var{Monoidal} \simeq \var{Kleisli} + \var{Monoidal} ≃ \var{Kleisli} $$ % \end{frame}