diff --git a/doc/acknowledgement.tex b/doc/acknowledgement.tex new file mode 100644 index 0000000..5cd6cc3 --- /dev/null +++ b/doc/acknowledgement.tex @@ -0,0 +1 @@ +\chapter*{Acknowledgements} diff --git a/doc/conclusion.tex b/doc/conclusion.tex index c4d0d10..67f4075 100644 --- a/doc/conclusion.tex +++ b/doc/conclusion.tex @@ -1,53 +1,53 @@ \chapter{Conclusion} This thesis highlighted some issues with the standard inductive -definition of propositional equality used in Agda. Functional +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 -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 +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 Agda enjoys Uniqueness of Identity Proofs (UIP) though a flag +exists to turn this off. This feature is not present in Cubical Agda. +Rather than having unique identity proofs cubical Agda gives rise to a +hierarchy of types with increasing \nomen{homotopical structure}{homotopy levels}. It turns out to be useful to built the formalization with this hierarchy in mind as it can simplify proofs -considerably. Another issue one must overcome in Cubical Agda is when -a type has a field whose type depends on a previous field. In this -case paths between such types will be heterogeneous paths. This -problem is related to Cubical Agda not having the K-rule. In practice -it turns out to be considerably more difficult to work heterogeneous -paths than with homogeneous paths. The thesis demonstrated some -techniques to overcome these difficulties, such as based -path-induction. +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. In +practice it turns out to be considerably more difficult to work with +heterogeneous paths than with homogeneous paths. The thesis +demonstrated the application of some techniques to overcome these +difficulties, such as based path induction. -This thesis formalized some of the core concepts from category theory +This thesis formalizes some of the core concepts from category theory including; categories, functors, products, exponentials, Cartesian closed categories, natural transformations, the yoneda embedding, -monads and more. Category theory is an interesting case-study for the -application of Cubical Agda for two reasons in particular: Because +monads and more. Category theory is an interesting case study for the +application of cubical Agda for two reasons in particular: Because category theory is the study of abstract algebra of functions, meaning that functional extensionality is particularly relevant. Another reason is that in category theory it is commonplace to identify -isomorphic structures and univalence allows for making this notion -precise. This thesis also demonstrated another technique that is +isomorphic structures. Univalence allows for making this notion +precise. This thesis also demonstrated another technique that is common in category theory; namely to define categories to prove properties of other structures. Specifically a category was defined to demonstrate that any two product objects in a category are -isomorphic. Furthermore the thesis showed two formulations of monads +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 +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. +more familiar to functional programmers. It would have been very +difficult to make a similar proof with setoids and the proof would be +very difficult to read. In the formulation we also saw how paths can +be used to extract functions. A path between two types induce an +isomorphism between the two types. This e.g.\ permits developers to +write a monad instance for a given type using the Kleisli formulation. +By transporting along the path between the monoidal- and Kleisli- +formulation one can reuse all the operations and results shown for +monoidal- monads in the context of kleisli monads. %% %% problem with inductive type %% overcome with cubical diff --git a/doc/discussion.tex b/doc/discussion.tex index 56177ef..6d87beb 100644 --- a/doc/discussion.tex +++ b/doc/discussion.tex @@ -1,113 +1,113 @@ \chapter{Perspectives} \section{Discussion} In the previous chapter the practical aspects of proving things in -Cubical Agda were highlighted. I also demonstrated the usefulness of -separating ``laws'' from ``data''. One of the reasons for this is that -dependencies within types can lead to very complicated goals. One +Cubical Agda were highlighted. I also demonstrated the usefulness of +separating ``laws'' from ``data''. One of the reasons for this is that +dependencies within types can lead to very complicated goals. One technique for alleviating this was to prove that certain types are mere propositions. \subsection{Computational properties} The new contribution of cubical Agda is that it has a constructive proof of functional extensionality\index{functional extensionality} -and univalence\index{univalence}. This means that in particular that -the type checker can reduce terms defined with these theorems. So one +and univalence\index{univalence}. This means that in particular that +the type checker can reduce terms defined with these theorems. So one interesting result of this development is how much this influenced the -development. In particular having a functional extensionality that +development. In particular having a functional extensionality that ``computes'' should simplify some proofs. -I have tested this theory by using a feature of Agda where one can -mark certain bindings as being \emph{abstract}. This means that the -type-checker will not try to reduce that term further when -type-checking is performed. I tried making univalence and functional -extensionality abstract. It turns out that the conversion behaviour of -univalence is not used anywhere. For functional extensionality there -are two places in the whole solution where the reduction behaviour is -used to simplify some proofs. This is in showing that the maps between -the two formulations of monads are inverses. See the notes in this +I have tested this by using a feature of Agda where one can mark +certain bindings as being \emph{abstract}. This means that the +type-checker will not try to reduce that term further during type +checking. I tried making univalence and functional extensionality +abstract. It turns out that the conversion behaviour of univalence is +not used anywhere. For functional extensionality there are two places +in the whole solution where the reduction behaviour is used to +simplify some proofs. This is in showing that the maps between the +two formulations of monads are inverses. See the notes in this module: % \begin{center} \sourcelink{Cat.Category.Monad.Voevodsky} \end{center} % -I've also put this in a source listing in \ref{app:abstract-funext}. I -will not reproduce it in full here as the type is quite involved. The -method used to find in what places the computational behaviour of -these proofs are needed has the caveat of only working for places that -directly or transitively uses these two proofs. Fortunately though the -code is structured in such a way that this should be the case. -Nonetheless it is quite surprising that this computational behaviours -is not used more widely in the formalization. -Barring this, however, the computational behaviour of paths can still -be useful. E.g. if a programmer want's to reuse functions that operate -on a monoidal monads to work with a monad in the Kleisli form that -this programmer has specified. To make this idea concrete, say we are +I will not reproduce it in full here as the type is quite involved. In +stead I have put this in a source listing in \ref{app:abstract-funext}. +The method used to find in what places the computational behaviour of +these proofs are needed has the caveat of only working for places that +directly or transitively uses these two proofs. Fortunately though +the code is structured in such a way that this is the case. So in +conclusion the way I have structured these proofs means that the +computational behaviour of functional extensionality and univalence +has not been so relevant. + +Barring this the computational behaviour of paths can still be useful. +E.g.\ if a programmer wants to reuse functions that operate on a +monoidal monads to work with a monad in the Kleisli form that the +programmer has specified. To make this idea concrete, say we are given some function $f \tp \Kleisli \to T$ having a path between $p \tp \Monoidal \equiv \Kleisli$ induces a map $\coe\ p \tp \Monoidal -\to \Kleisli$. We can compose $f$ with this map to get $f \comp -\coe\ p \tp \Monoidal \to T$. Of course, since that map was +\to \Kleisli$. We can compose $f$ with this map to get $f \comp +\coe\ p \tp \Monoidal \to T$. Of course, since that map was constructed with an isomorphism these maps already exist and could be -used directly. So this is arguably only interesting when one wants to -prove properties of such functions. +used directly. So this is arguably only interesting when one also +wants to prove properties of applying such functions. \subsection{Reusability of proofs} The previous example illustrate how univalence unifies two otherwise disparate areas: The category-theoretic study of monads; and monads as -in functional programming. Univalence thus allows one to reuse proofs. +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. As an illustration of this I proved that monads are -groupoids. I initially proved this for the Kleisli +price of one. As an illustration of this I proved that monads are +groupoids. I initially proved this for the Kleisli formulation\footnote{Actually doing this directly turned out to be tricky as well, so I defined an equivalent formulation which was not - formulated with a record, but purely with $\sum$-types.}. Since the + formulated with a record, but purely with $\sum$-types.}. Since the two formulations are equal under univalence, substitution directly -gives us that this also holds for the monoidal formulation. This of +gives us that this also holds for the monoidal formulation. This of course generalizes to any family $P \tp 𝒰 β†’ 𝒰$ where $P$ is inhabited at either formulation (i.e.\ either $P\ \Monoidal$ or $P\ \Kleisli$ holds). -The introduction (section \S\ref{sec:context}) mentioned an often -employed-technique for enabling extensional equalities is to use the -setoid-interpretation. Nowhere in this formalization has this been -necessary, $\Path$ has been used globally in the project as -propositional equality. One interesting place where this becomes -apparent is in interfacing with the Agda standard library. Multiple -definitions in the Agda standard library have been designed with the -setoid-interpretation in mind. E.g. the notion of ``unique -existential'' is indexed by a relation that should play the role of -propositional equality. Likewise for equivalence relations, they are -indexed, not only by the actual equivalence relation, but also by -another relation that serve as propositional equality. +The introduction (section \S\ref{sec:context}) mentioned that a +typical way of getting access to functional extensionality is to work +with setoids. Nowhere in this formalization has this been necessary, +$\Path$ has been used globally in the project for propositional +equality. One interesting place where this becomes apparent is in +interfacing with the Agda standard library. Multiple definitions in +the Agda standard library have been designed with the +setoid-interpretation in mind. E.g.\ the notion of \emph{unique + existential} is indexed by a relation that should play the role of +propositional equality. Equivalence relations are likewise indexed, +not only by the actual equivalence relation but also by another +relation that serve as propositional equality. %% Unfortunately we cannot use the definition of equivalences found in -%% the standard library to do equational reasoning directly. The +%% the standard library to do equational reasoning directly. The %% reason for this is that the equivalence relation defined there must %% be a homogenous relation, but paths are heterogeneous relations. In the formalization at present a significant amount of energy has been put towards proving things that would not have been needed in -classical Agda. The proofs that some given type is a proposition were +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 \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 +proofs (e.g.\ \ref{eq:proof-prop-IsPreCategory} +and \ref{eq:productPath}). Often these proofs would not be this +complicated. If the J-rule holds definitionally the proof-assistant +can help simplify these goals considerably. The lack of the J-rule has a significant impact on the complexity of these kinds of proofs. -\TODO{Universe levels.} - \subsection{Motifs} An oft-used technique in this development is using based path -induction to prove certain properties. One particular challenge that +induction to prove certain properties. One particular challenge that arises when doing so is that Agda is not able to automatically infer -the family that one wants to do induction over. For instance in the +the family that one wants to do induction over. For instance in the proof $\var{sym}\ (\var{sym}\ p) ≑ p$ from \ref{eq:sym-invol} the family that we chose to do induction over was $D\ b'\ p' \defeq -\var{sym}\ (\var{sym}\ p') ≑ p'$. However, if one interactively tries +\var{sym}\ (\var{sym}\ p') ≑ p'$. However, if one interactively tries to give this hole, all the information that Agda can provide is that -one must provide an element of $𝒰$. Agda could be more helpful in this -context, perhaps even infer this family in some situations. In this +one must provide an element of $𝒰$. Agda could be more helpful in this +context, perhaps even infer this family in some situations. In this very simple example this is of course not a big problem, but there are examples in the source code where this gets more involved. @@ -115,26 +115,25 @@ examples in the source code where this gets more involved. \subsection{Compiling Cubical Agda} \label{sec:compiling-cubical-agda} Compilation of program written in Cubical Agda is currently not -supported. One issue here is that the backends does not provide an +supported. One issue here is that the backends does not provide an implementation for the cubical primitives (such as the path-type). This means that even though the path-type gives us a computational interpretation of functional extensionality, univalence, transport, etc., we do not have a way of actually using this to compile our -programs that use these primitives. It would be interesting to see -practical applications of this. The path between monads that this -library exposes could provide one particularly interesting case-study. - -\subsection{Higher inductive types} -This library has not explored the usefulness of higher inductive types -in the context of Category Theory. - -\subsection{Initiality conjecture} -A fellow student here at Chalmers, Andreas KΓ€llberg, is currently -working on proving the initiality conjecture\TODO{Citation}. He will -be using this library to do so. +programs that use these primitives. It would be interesting to see +practical applications of this. \subsection{Proving laws of programs} Another interesting thing would be to use the Kleisli formulation of -monads to prove properties of functional programs. The existence of +monads to prove properties of functional programs. The existence of univalence will make it possible to re-use proofs stated in terms of the monoidal formulation in this setting. + +%% \subsection{Higher inductive types} +%% This library has not explored the usefulness of higher inductive types +%% in the context of Category Theory. + +\subsection{Initiality conjecture} +A fellow student at Chalmers, Andreas KΓ€llberg, is currently working +on proving the initiality conjecture. He will be using this library +to do so. diff --git a/doc/implementation.tex b/doc/implementation.tex index 51f5629..e8574de 100644 --- a/doc/implementation.tex +++ b/doc/implementation.tex @@ -15,75 +15,75 @@ link\footnote{% }: % \begin{center} -\doclink + \doclink \end{center} The concepts formalized in this development are: % \begin{center} -\begin{tabular}{ l l } -Name & Module \\ -\hline -Equivalences & \sourcelink{Cat.Equivalence} \\ -Categories & \sourcelink{Cat.Category} \\ -Functors & \sourcelink{Cat.Category.Functor} \\ -Products & \sourcelink{Cat.Category.Product} \\ -Exponentials & \sourcelink{Cat.Category.Exponential} \\ -Cartesian closed categories & \sourcelink{Cat.Category.CartesianClosed} \\ -Natural transformations & \sourcelink{Cat.Category.NaturalTransformation} \\ -Yoneda embedding & \sourcelink{Cat.Category.Yoneda} \\ -Monads & \sourcelink{Cat.Category.Monad} \\ -Kleisli Monads & \sourcelink{Cat.Category.Monad.Kleisli} \\ -Monoidal Monads & \sourcelink{Cat.Category.Monad.Monoidal} \\ -Voevodsky's construction & \sourcelink{Cat.Category.Monad.Voevodsky} \\ -Opposite category & \sourcelink{Cat.Categories.Opposite} \\ -Category of sets & \sourcelink{Cat.Categories.Sets} \\ -Span category & \sourcelink{Cat.Categories.Span} \\ -\end{tabular} + \begin{tabular}{ l l } + Name & Module \\ + \hline + Equivalences & \sourcelink{Cat.Equivalence} \\ + Categories & \sourcelink{Cat.Category} \\ + Functors & \sourcelink{Cat.Category.Functor} \\ + Products & \sourcelink{Cat.Category.Product} \\ + Exponentials & \sourcelink{Cat.Category.Exponential} \\ + Cartesian closed categories & \sourcelink{Cat.Category.CartesianClosed} \\ + Natural transformations & \sourcelink{Cat.Category.NaturalTransformation} \\ + Yoneda embedding & \sourcelink{Cat.Category.Yoneda} \\ + Monads & \sourcelink{Cat.Category.Monad} \\ + Kleisli Monads & \sourcelink{Cat.Category.Monad.Kleisli} \\ + Monoidal Monads & \sourcelink{Cat.Category.Monad.Monoidal} \\ + Voevodsky's construction & \sourcelink{Cat.Category.Monad.Voevodsky} \\ + Opposite category & \sourcelink{Cat.Categories.Opposite} \\ + Category of sets & \sourcelink{Cat.Categories.Sets} \\ + Span category & \sourcelink{Cat.Categories.Span} \\ + \end{tabular} \end{center} % \begin{samepage} -Furthermore the following items have been partly formalized: -% -\begin{center} -\begin{tabular}{ l l } -Name & Module \\ -\hline -Category of categories & \sourcelink{Cat.Categories.Cat} \\ -Category of relations & \sourcelink{Cat.Categories.Rel} \\ -Category of functors & \sourcelink{Cat.Categories.Fun} \\ -Free category & \sourcelink{Cat.Categories.Free} \\ -Monoids & \sourcelink{Cat.Category.Monoid} \\ -\end{tabular} -\end{center} + Furthermore the following items have been partly formalized: + % + \begin{center} + \begin{tabular}{ l l } + Name & Module \\ + \hline + Category of categories & \sourcelink{Cat.Categories.Cat} \\ + Category of relations & \sourcelink{Cat.Categories.Rel} \\ + Category of functors & \sourcelink{Cat.Categories.Fun} \\ + 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 +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 +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 technique employed throughout this formalization is the idea of -distinguishing types with more or less homotopical structure. To do +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 +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 +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 +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 the tables above. @@ -91,64 +91,64 @@ implementation which is linked in the tables above. \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 +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 +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 +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 +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 -require it to be univalent. Before we can define this, I must introduce two more +\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} β‰œ ∏_{A, B \tp \Object} ∏_{f \tp \Arrow\ A\ B} - \left(\id \lll f ≑ f\right) \x \left(f \lll \id ≑ f\right) + \left(\id \lll f ≑ f\right) \x \left(f \lll \id ≑ f\right) \end{equation} % Then we can construct the identity isomorphism $\idIso \tp (\identity, -\identity, p) \tp A β‰Š A$ for any object $A$. Here $β‰Š$ +\identity, p) \tp A β‰Š A$ for any object $A$. Here $β‰Š$ 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 +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 + \idToIso \tp A ≑ B β†’ A β‰Š B \end{equation} % The univalence criterion for categories states that this map must be an -equivalence. The requirement is similar to univalence for types, but where -isomorphism on objects play the role of equivalence on types. Formally: +equivalence. The requirement is similar to univalence for types, but where +isomorphism on objects play the role of equivalence on types. Formally: % \begin{align} -\label{eq:cat-univ} -\isEquiv\ (A ≑ B)\ (A β‰Š B)\ \idToIso + \label{eq:cat-univ} + \isEquiv\ (A ≑ B)\ (A β‰Š B)\ \idToIso \end{align} % Note that \ref{eq:cat-univ} is \emph{not} the same as: % \begin{equation} -\label{eq:cat-univalence} -%% \tag{Univalence, category} -(A ≑ B) ≃ (A β‰Š B) + \label{eq:cat-univalence} + %% \tag{Univalence, category} + (A ≑ B) ≃ (A β‰Š 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 +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 @@ -164,54 +164,54 @@ data: And laws: % \begin{align} -%% \tag{associativity} -h \lll (g \lll f) ≑ (h \lll g) \lll f \\ -%% \tag{identity} -\left( -\identity \lll f ≑ f -\right) -\x -\left( -f \lll \identity ≑ f -\right) -\\ -\label{eq:arrows-are-sets} -%% \tag{arrows are sets} -\isSet\ (\Arrow\ A\ B)\\ -\tag{\ref{eq:cat-univ}} -\isEquiv\ (A ≑ B)\ (A β‰Š B)\ \idToIso + %% \tag{associativity} + h \lll (g \lll f) ≑ (h \lll g) \lll f \\ + %% \tag{identity} + \left( + \identity \lll f ≑ f + \right) + \x + \left( + f \lll \identity ≑ f + \right) + \\ + \label{eq:arrows-are-sets} + %% \tag{arrows are sets} + \isSet\ (\Arrow\ A\ B)\\ + \tag{\ref{eq:cat-univ}} + \isEquiv\ (A ≑ B)\ (A β‰Š B)\ \idToIso \end{align} % -$\lll$ denotes arrow composition (right-to-left), and reverse function -composition (left-to-right, diagrammatic order) is denoted $\rrr$. The objects -($A$, $B$ and $C$) and arrow ($f$, $g$, $h$) are implicitly universally -quantified. +The function $\lll$ denotes arrow composition (right-to-left), and +reverse function composition (left-to-right, diagrammatic order) is +denoted $\rrr$. The objects ($A$, $B$ and $C$) and arrow ($f$, $g$, +$h$) are implicitly universally quantified. With all this in place it is now possible to prove that all the laws -are indeed mere propositions. Most of the proofs simply use the fact -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 +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 +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 do 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}: % \begin{align*} -\propPi & \tp \left(∏_{a \tp A} \isProp\ (P\ a)\right) β†’ \isProp\ \left(∏_{a \tp A} P\ a\right) + \propPi & \tp \left(∏_{a \tp A} \isProp\ (P\ a)\right) β†’ \isProp\ \left(∏_{a \tp A} P\ a\right) \\ -\propSig & \tp \isProp\ A β†’ \left(∏_{a \tp A} \isProp\ (P\ a)\right) β†’ \isProp\ \left(βˆ‘_{a \tp A} P\ a\right) + \propSig & \tp \isProp\ A β†’ \left(∏_{a \tp A} \isProp\ (P\ a)\right) β†’ \isProp\ \left(βˆ‘_{a \tp A} P\ a\right) \end{align*} % The proof goes like this: We `eliminate' the 3 function abstractions -by applying $\propPi$ three times. So our proof obligation becomes: +by applying $\propPi$ three times. So our proof obligation becomes: % $$ \isProp\ \left( \left( \id \comp f ≑ f \right) \x \left( f \comp \id ≑ f \right) \right) @@ -223,30 +223,30 @@ us the two obligations $\isProp\ (\id \comp f ≑ f)$ and $\isProp\ (f \comp set. This example illustrates nicely how we can use these combinators to -reason about `canonical' types like $βˆ‘$ and $∏$. Similar -combinators can be defined at the other homotopic levels. These +reason about `canonical' types like $βˆ‘$ and $∏$. 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 +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: +show that the type of pre-categories is also a proposition. Formally: % \begin{equation} -\label{eq:propIsPreCategory} -\isProp\ \IsPreCategory + \label{eq:propIsPreCategory} + \isProp\ \IsPreCategory \end{equation} % Where the definition of $\IsPreCategory$ is the triple: % \begin{align*} -\var{isAssociative} & \tp \var{IsAssociative}\\ -\isIdentity & \tp \var{IsIdentity}\\ -\var{arrowsAreSets} & \tp \var{ArrowsAreSets} + \var{isAssociative} & \tp \var{IsAssociative}\\ + \isIdentity & \tp \var{IsIdentity}\\ + \var{arrowsAreSets} & \tp \var{ArrowsAreSets} \end{align*} % -Each corresponding to the first three laws for categories. Note that +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 +we will not have any combinators available to help us here. In stead the path type must be used directly. The type \ref{eq:propIsPreCategory} is judgmentally the same as: @@ -255,14 +255,14 @@ $$ ∏_{a, b \tp \IsPreCategory} a ≑ 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 ≑ b$ is to give a continuous path from the -index-type into the path-space. I.e.\ a function $\I β†’ -\IsPreCategory$. This path must satisfy being being judgmentally the -same as $a$ at the left endpoint and $b$ at the right endpoint. We +index-type into the path-space. I.e.\ a function $\I β†’ +\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 $b$, this follows from the type of all the projections being mere -propositions. For instance, the path between $a.\isIdentity$ and +propositions. For instance, the path between $a.\isIdentity$ and $b.\isIdentity$ is simply formed by: % $$ @@ -274,45 +274,44 @@ $$ So to give the continuous function $\I β†’ \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 +between all projections. Once we have such a path e.g.\ $p \tp a.\isIdentity ≑ b.\isIdentity$ we can eliminate it with $i$ and thus obtain $p\ i \tp -(p\ i).\isIdentity$. This element satisfies exactly that it corresponds to the -corresponding projections at either endpoint. Thus the element we construct at +(p\ i).\isIdentity$. This element satisfies exactly that it corresponds to the +corresponding projections at either endpoint. Thus the element we construct at $i$ becomes the triple: % \begin{equation} -\label{eq:proof-prop-IsPreCategory} -\begin{aligned} - & \var{propIsAssociative} && a.\var{isAssociative}\ - && b.\var{isAssociative} && i \\ - & \propIsIdentity && a.\isIdentity\ - && b.\isIdentity && i \\ - & \var{propArrowsAreSets} && a.\var{arrowsAreSets}\ - && b.\var{arrowsAreSets} && i -\end{aligned} + \label{eq:proof-prop-IsPreCategory} + \begin{aligned} + & \var{propIsAssociative} && a.\var{isAssociative}\ + && b.\var{isAssociative} && i \\ + & \propIsIdentity && a.\isIdentity\ + && b.\isIdentity && i \\ + & \var{propArrowsAreSets} && a.\var{arrowsAreSets}\ + && b.\var{arrowsAreSets} && i + \end{aligned} \end{equation} % I have found this to be a general pattern when proving things in homotopy type theory, namely that you have to wrap and unwrap -equalities at different levels. It is worth noting that proving this +equalities at different levels. It is worth noting that proving this theorem with the regular inductive equality type would already not be possible, since we at least need functional extensionality\index{functional extensionality} (the projections are -all $∏$-types). Assuming we had functional extensionality -available to us as an axiom, we would use functional extensionality -\TODO{in reverse?} to retrieve the equalities in $a$ and $b$, -pattern-match on them to see that they are both $\refl$ and then close -the proof with $\refl$. Of course this theorem is not so interesting -in the setting of ITT since we know a priori that equality proofs are -unique. +all $∏$-types). Assuming we had functional extensionality available to +us as an axiom, we would use functional extensionality to retrieve the +equalities in $a$ and $b$; pattern match on them to see that they are +both $\refl$ and then close the proof with $\refl$. Of course this +theorem is not so interesting in the setting of ITT since we know +a~priori that equality proofs are unique. The situation is a bit more complicated when we have a dependent type. -For instance, when we want to show that $\IsCategory$ is a mere -proposition. The type $\IsCategory$ is a record with two fields, a -witness to being a pre-category and the univalence condition. Recall -that the univalence condition is indexed by the identity-proof. So to +For instance when we want to show that $\IsCategory$ is a mere +proposition. The type $\IsCategory$ is a record with two fields, a +witness of being a pre-category and the univalence condition. Recall +that the univalence condition is indexed by the identity-proof. So to follow the same recipe as above, let $a, b \tp \IsCategory$ be given, -to show them equal, we now need to give two paths. One homogeneous: +to show them equal, we now need to give two paths. One homogeneous: % $$ p \tp a.\isPreCategory ≑ b.\isPreCategory @@ -324,28 +323,38 @@ $$ \Path\ (\lambda\; i β†’ (p\ i).Univalent)\ a.\isPreCategory\ b.\isPreCategory $$ % -Which depends on the choice of $p$. The first of these we can provide since, as -we have shown, $\IsPreCategory$ is a proposition. However, even though -$\Univalent$ is also a proposition, we cannot use this directly to show the -latter. This is because $\isProp$ talks about non-dependent paths. So we need to -'promote' the result that univalence is a proposition to a heterogeneous path. -To this end we can use $\lemPropF$, which was introduced in \S\ref{sec:lemPropF}. +This path depends on the choice of $p$. The first of these we can +provide since, as we have shown, $\IsPreCategory$ is a +proposition. However, even though $\Univalent$ is also a proposition, +we cannot use this directly to show the latter. This is because +$\isProp$ talks about non-dependent paths. So we need to 'promote' the +result that univalence is a proposition to a heterogeneous path. To +this end we can use $\lemPropF$, which was introduced in +\S\ref{sec:lemPropF}. -In this case $A = \var{IsIdentity}\ \identity$ and $B = \Univalent$. We have -shown that being a category is a proposition, a result that holds for any choice -of identity proof. Finally we must provide a proof that the identity proofs at -$a$ and $b$ are indeed the same, this we can extract from $p$ by applying -congruence of paths: +In this case $A = \var{IsIdentity}\ \identity$ and $B = +\Univalent$. We have shown that being a category is a proposition, a +result that holds for any choice of identity proof so it will also +hold for the witness obtained at an arbitrary point along $p$. Finally +we must provide a proof that the identity proofs at $a$ and $b$ are +indeed the same, this we can extract from $p$ by applying congruence +of paths: % $$ \congruence\ \isIdentity\ p $$ % +In summary the heterogeneous path is inhabited by: +% +$$ +\var{lemPropF}\ \var{propUnivalent}\ (\var{cong}\ p.\var{isIdentity}) +$$ +% And this finishes the proof that being-a-category is a mere proposition (\ref{eq:propIsPreCategory}). When we have a proper category we can make precise the notion of -``identifying isomorphic types''. That is, we can construct the +``identifying isomorphic types''. That is, we can construct the function: % $$ @@ -356,17 +365,17 @@ A perhaps somewhat surprising application of this is that we can show that terminal objects are propositional: % \begin{align} -\label{eq:termProp} -\isProp\ \var{Terminal} + \label{eq:termProp} + \isProp\ \var{Terminal} \end{align} % It follows from the usual observation that any two terminal objects are -isomorphic - and since categories are univalent, so are they equal. The proof is +isomorphic - and since categories are univalent, so are they equal. The proof is omitted here, but the curious reader can check the implementation for the -details. It is in the module: +details. It is in the module: % \begin{center} -\sourcelink{Cat.Category} + \sourcelink{Cat.Category} \end{center} \section{Equivalences} @@ -374,38 +383,39 @@ details. It is in the module: The usual notion of a function $f \tp A β†’ B$ having an inverses is: % \begin{equation} -\label{eq:isomorphism} -βˆ‘_{g \tp B β†’ A} \left( f \comp g ≑ \identity \right) \x \left( g \comp f ≑ \identity \right) + \label{eq:isomorphism} + βˆ‘_{g \tp B β†’ A} \left( f \comp g ≑ \identity \right) \x \left( g \comp f ≑ \identity \right) \end{equation} % This is defined in \cite[p. 129]{hott-2013} where it is referred to as the a -``quasi-inverse''. We shall refer to the type \ref{eq:isomorphism} as -$\Isomorphism\ f$. This also gives rise to the following type: +``quasi-inverse''. We shall refer to the type \ref{eq:isomorphism} as +$\Isomorphism\ f$. This also gives rise to the following type: % \begin{equation} -A \cong B β‰œ βˆ‘_{f \tp A β†’ B} \Isomorphism\ f + A \cong B β‰œ βˆ‘_{f \tp A β†’ B} \Isomorphism\ f \end{equation} % At the same place \cite{hott-2013} gives an ``interface'' for what the judgment $\isEquiv \tp (A β†’ B) β†’ \MCU$ must provide: % \begin{align} -\var{fromIso} & \tp \Isomorphism\ f β†’ \isEquiv\ f \\ -\var{toIso} & \tp \isEquiv\ f β†’ \Isomorphism\ f \\ -\label{eq:propIsEquiv} - &\mathrel{\ } \isEquiv\ f + \var{fromIso} & \tp \Isomorphism\ f β†’ \isEquiv\ f \\ + \var{toIso} & \tp \isEquiv\ f β†’ \Isomorphism\ f \\ + \label{eq:propIsEquiv} + &\mathrel{\ } \isEquiv\ f \end{align} % The maps $\var{fromIso}$ and $\var{toIso}$ naturally extend to these maps: % \begin{align} -\var{fromIsomorphism} & \tp A \cong B β†’ A ≃ B \\ -\var{toIsomorphism} & \tp A ≃ B β†’ A \cong B + \var{fromIsomorphism} & \tp A \cong B β†’ A ≃ B \\ + \var{toIsomorphism} & \tp A ≃ B β†’ A \cong B \end{align} % -Having this interface gives us both: a way to think rather abstractly about how -to work with equivalences and a way to use ad hoc definitions of equivalences. -The specific instantiation of $\isEquiv$ as defined in \cite{cubical-agda} is: +Having this interface gives us both a way to think rather abstractly +about how to work with equivalences and a way to use ad~hoc +definitions of equivalences. The specific instantiation of $\isEquiv$ +as defined in \cite{cubical-agda} is: % $$ isEquiv\ f β‰œ ∏_{b \tp B} \isContr\ (\fiber\ f\ b) @@ -420,7 +430,7 @@ move away from this specific instantiation and think about it more abstractly once we have shown that this definition actually works as an equivalence. The implementation of $\var{fromIso}$ can be found in -\cite{cubical-agda} where it is known as $\var{gradLemma}$. The +\cite{cubical-agda} where it is known as $\var{gradLemma}$. The implementation of $\var{fromIso}$ as well as the proof that this equivalence is a proposition (\ref{eq:propIsEquiv}) can be found in my implementation. @@ -429,14 +439,14 @@ We say that two types $A\;B \tp \Type$ are equivalent exactly if there exists an equivalence between them: % \begin{equation} -\label{eq:equivalence} -A ≃ B β‰œ βˆ‘_{f \tp A β†’ B} \isEquiv\ f + \label{eq:equivalence} + A ≃ B β‰œ βˆ‘_{f \tp A β†’ B} \isEquiv\ f \end{equation} % Note that the term equivalence here is overloaded referring both to the map $f -\tp A β†’ B$ and the type $A ≃ B$. The notion of an isomorphism is +\tp A β†’ B$ and the type $A ≃ B$. The notion of an isomorphism is similarly conflated as isomorphism can refer to the type $A \cong B$ as well as -the the map $A β†’ B$ that witness this. I will use these conflated terms when +the the map $A β†’ B$ that witness this. I will use these conflated terms when it is clear from the context what is being referred to. Both $\cong$ and $≃$ form equivalence relations (no pun intended). @@ -468,20 +478,22 @@ $$ (A ≑ B) \cong (A β‰Š B) $$ % -That is, we must demonstrate that there is an isomorphism (on types) between -equalities and isomorphisms (on arrows). It is worthwhile to dwell on this for a -few seconds. This type looks very similar to univalence for types and is -therefore perhaps a bit more intuitive to grasp the implications of. Of course -univalence for types (which is a proposition -- i.e.\ provable) does not imply -univalence of all pre-category since morphisms in a category are not regular -functions -- in stead they can be thought of as a generalization hereof. The univalence criterion therefore is simply a way of restricting arrows -to behave similarly to maps. +That is, we must demonstrate that there is an isomorphism (on types) +between equalities and isomorphisms (on arrows). It is worthwhile to +dwell on this for a few seconds. This type looks very similar to +univalence for types and is therefore perhaps a bit more intuitive to +grasp the implications of. Of course univalence for types (which is a +theorem -- i.e.\ provably holds) does not imply univalence of all +pre-category since morphisms in a category are not regular functions +-- in stead they can be thought of as a generalization hereof. The +univalence criterion therefore is simply a way of restricting arrows +to behave like maps with respect to univalence. I will now mention a few helpful theorems that follow from univalence that will become useful later. Obviously univalence gives us an isomorphism between $A ≑ B$ and $A -β‰Š B$. I will name these for convenience: +β‰Š B$. I will name these for convenience: % $$ \idToIso \tp A ≑ B β†’ A β‰Š B @@ -491,81 +503,91 @@ $$ \isoToId \tp A β‰Š B β†’ A ≑ B $$ % -The next few theorems are variations on theorem 9.1.9 from \cite{hott-2013}. Let -an isomorphism $A β‰Š B$ in some category $\bC$ be given. Name the -isomorphism $\iota \tp A β†’ B$ and its inverse $\inv{\iota} \tp B β†’ A$. -Since $\bC$ is a category (and therefore univalent) the isomorphism induces a -path $p \tp A ≑ B$. From this equality we can get two further paths: -$p_{\var{dom}} \tp \Arrow\ A\ X ≑ \Arrow\ B\ X$ and -$p_{\var{cod}} \tp \Arrow\ X\ A ≑ \Arrow\ X\ B$. We -then have the following two theorems: +The next few theorems are variations on theorem 9.1.9 from +\cite{hott-2013}. Let an isomorphism $A β‰Š B$ in some category $\bC$ be +given. Name the isomorphism $\iota \tp A β†’ B$ and its inverse +$\inv{\iota} \tp B β†’ A$. Since $\bC$ is a category (and therefore +univalent) the isomorphism induces a path +% +$$p \defeq \idToIso\ (\iota, \inv{\iota}, \dots) \tp A ≑ B$$ +% +From this equality we can get two further paths: +% +\begin{align*} + p_{\var{dom}} & \tp \Arrow\ A\ X ≑ \Arrow\ B\ X \\ + p_{\var{cod}} & \tp \Arrow\ X\ A ≑ \Arrow\ X\ B +\end{align*} +% +We then have the following two theorems: % \begin{align} -\label{eq:coeDom} -\var{coeDom} & \tp ∏_{f \tp A β†’ X} -\var{coe}\ p_{\var{dom}}\ f ≑ f \lll \inv{\iota} -\\ -\label{eq:coeCod} -\var{coeCod} & \tp ∏_{f \tp A β†’ X} -\var{coe}\ p_{\var{cod}}\ f ≑ \iota \lll f + \label{eq:coeDom} + \var{coeDom} & \tp ∏_{f \tp A β†’ X} + \var{coe}\ p_{\var{dom}}\ f ≑ f \lll \inv{\iota} + \\ + \label{eq:coeCod} + \var{coeCod} & \tp ∏_{f \tp A β†’ X} + \var{coe}\ p_{\var{cod}}\ f ≑ \iota \lll f \end{align} % I will give the proof of the first theorem here, the second one is analogous. % \begin{align*} -\var{coe}\ p_{\var{dom}}\ f - & ≑ f \lll \inv{(\idToIso\ p)} && \text{lemma} \\ + \var{coe}\ p_{\var{dom}}\ f + & ≑ f \lll (\idToIso\ p)_2 && \text{lemma} \\ & ≑ f \lll \inv{\iota} - && \text{$\idToIso$ and $\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{(\idToIso\ p)}$ denotes the map $B β†’ A$ induced by the -isomorphism $\idToIso\ p \tp A \cong B$. The helper-lemma is similar to -what we are trying to prove but talks about paths rather than isomorphisms: +In the second step we use the fact that $p$ is constructed from the +isomorphism $\iota$. The subscript in term $(\idToIso\ p)_2$ is +intended to denote the inverse map $B β†’ A$ from the isomorphism +$\idToIso\ p \tp A \cong B$. The helper-lemma is similar to what we +are trying to prove but talks about paths rather than isomorphisms: % \begin{equation} -\label{eq:coeDomIso} -∏_{f \tp \Arrow\ A\ B} ∏_{p \tp A ≑ B} -\var{coe}\ p_{\var{dom}}\ f ≑ f \lll \inv{(\idToIso\ p)} + \label{eq:coeDomIso} + ∏_{f \tp \Arrow\ A\ B} ∏_{p \tp A ≑ B} + \var{coe}\ p_{\var{dom}}\ f ≑ f \lll (\idToIso\ p)_{2} \end{equation} % -Again $p_{\var{dom}}$ denotes the path $\Arrow\ A\ X ≑ -\Arrow\ B\ X$ induced by $p$. To prove this statement I let $f$ and $p$ be -given and then invoke based-path-induction. The induction will be based at $A -\tp \Object$ Let $\widetilde{B} \tp \Object$ and $\widetilde{p} \tp A -≑ \widetilde{B}$ be given. The family that we perform induction over will -be: +Again $p_{\var{dom}}$ denotes the path $\Arrow\ A\ X ≑ \Arrow\ B\ X$ +induced by $p$. To prove this statement let $f$ and $p$ be given then +we invoke based path induction. The induction will be based at $A \tp +\Object$ Let $\widetilde{B} \tp \Object$ and $\widetilde{p} \tp A ≑ +\widetilde{B}$ be given. The family that we perform induction over +will be: % \begin{align} -D\ \widetilde{B}\ \widetilde{p} β‰œ + D\ \widetilde{B}\ \widetilde{p} β‰œ %% ∏_{\widetilde{B} \tp \Object} %% ∏_{\widetilde{p} \tp A ≑ \widetilde{B}} - \var{coe}\ {\widetilde{p}}^*\ f -≑ -f \lll \inv{(\idToIso\ \widetilde{p})} + \var{coe}\ {\widetilde{p}_{\var{dom}}}\ f + ≑ + f \lll (\idToIso\ \widetilde{p})_{2} \end{align} The base-case therefore becomes -$d \tp \var{coe}\ \refl^*\ f ≑ f \lll \inv{(\idToIso\ \refl)}$ +$d \tp \var{coe}\ \refl_{\var{dom}}\ f ≑ f \lll (\idToIso\ \refl)_{2}$ and is inhabited by: \begin{align*} -\var{coe}\ \refl^*\ f -& ≑ f + \var{coe}\ \refl_{\var{dom}}\ f + & ≑ f && \text{$\refl$ is a neutral element for $\var{coe}$}\\ -& ≑ f \lll \identity \\ -& ≑ f \lll \var{subst}\ \refl\ \identity + & ≑ f \lll \identity \\ + & ≑ f \lll \var{subst}\ \refl\ \identity && \text{$\refl$ is a neutral element for $\var{subst}$}\\ -& ≑ f \lll \inv{(\idToIso\ \refl)} + & = f \lll (\idToIso\ \refl)_{2} && \text{By definition of $\idToIso$}\\ \end{align*} % -To close the based-path-induction we must supply the value ``at the other''. In -this case this is simply $B \tp \Object$ and $p \tp A ≑ B$ which we have. -In summary the proof of \ref{eq:coeDomIso} is the term: +To close the based-path-induction we must supply the value ``at the +other end''. In this case this is simply $B \tp \Object$ and $p \tp A +≑ B$ which we have. In summary the proof of \ref{eq:coeDomIso} is the +term: % \begin{equation} -\label{eq:pathJ-example} -\pathJ\ D\ d\ B\ p + \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}. @@ -573,25 +595,25 @@ 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 will present is a pure construction on categories. Given -some category we can construct its dual, called the opposite category. Starting +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. Let $\bC$ be some category, we then define the opposite category -$\bC^{\var{Op}}$. It has the same objects, but the type of arrows are flipped, +$\bC^{\var{Op}}$. It has the same objects, but the type of arrows are flipped, that is to say an arrow from $A$ to $B$ in the opposite category corresponds to -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 +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 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 +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) ≑ h \rrr g \rrr f @@ -607,85 +629,85 @@ $$ This is just the swapped version of identity. 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 +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 straightforward. Luckily -section \S\ref{sec:equiv} gave us some tools to work with equivalences. We saw +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 ≑ B) β†’ (A \wideoverbar{β‰Š} B)$. From the original category we have that $\idToIso \tp (A ≑ B) β†’ (A \cong -B)$ is an isomorphism. Let us denote its inverse with $\isoToId \tp (A -β‰Š B) β†’ (A ≑ B)$. If we squint we can see what we need is a way to +B)$ is an isomorphism. Let us denote its inverse with $\isoToId \tp (A +β‰Š B) β†’ (A ≑ B)$. If we squint we can see what we need is a way to go between $\wideoverbar{β‰Š}$ and $β‰Š$. -An inhabitant of $A β‰Š B$ is simply an arrow $f \tp \Arrow\ A\ B$ -and its inverse $g \tp \Arrow\ B\ A$. In the opposite category $g$ will -play the role of the isomorphism and $f$ will be the inverse. Similarly we can -go in the opposite direction. I name these maps $\shufflef \tp (A β‰Š -B) β†’ (A \wideoverbar{β‰Š} B)$ and $\shufflef^{-1} \tp (A -\wideoverbar{β‰Š} B) β†’ (A β‰Š B)$ respectively. +An inhabitant of $A β‰Š B$ is simply an arrow $f \tp \Arrow\ A\ B$ and +its inverse $g \tp \Arrow\ B\ A$ (and a witness to them being +inverses). In the opposite category $g$ will play the role of the +isomorphism and $f$ will be the inverse. Similarly we can go in the +opposite direction. I name these maps $\shufflef \tp (A β‰Š B) β†’ (A +\wideoverbar{β‰Š} B)$ and $\shufflef^{-1} \tp (A \wideoverbar{β‰Š} B) β†’ (A +β‰Š B)$ respectively. As the inverse of $\wideoverbar{\idToIso}$ I will pick $\wideoverbar{\isoToId} -β‰œ \isoToId \comp \shufflef$. The proof that they are inverses go as +β‰œ \isoToId \comp \shufflef$. The proof that they are inverses go as follows: % \begin{align*} -\wideoverbar{\isoToId} \comp \wideoverbar{\idToIso} & = -\isoToId \comp \shufflef \comp \wideoverbar{\idToIso} -\\ -%% β‰‘βŸ¨ cong (λ \; Ο† β†’ Ο† x) (cong (λ \; Ο† β†’ Ξ· βŠ™ shuffle βŠ™ Ο†) (funExt lem)) ⟩ \\ -% -& ≑ -\isoToId \comp \shufflef \comp \inv{\shufflef} \comp \idToIso -&& \text{lemma} \\ -%% β‰‘βŸ¨βŸ© \\ -& ≑ -\isoToId \comp \idToIso -&& \text{$\shufflef$ is an isomorphism} \\ -& ≑ -\identity -&& \text{$\isoToId$ is an isomorphism} + \wideoverbar{\isoToId} \comp \wideoverbar{\idToIso} & = + \isoToId \comp \shufflef \comp \wideoverbar{\idToIso} + \\ + %% β‰‘βŸ¨ cong (λ \; Ο† β†’ Ο† x) (cong (λ \; Ο† β†’ Ξ· βŠ™ shuffle βŠ™ Ο†) (funExt lem)) ⟩ \\ + % + & ≑ + \isoToId \comp \shufflef \comp \inv{\shufflef} \comp \idToIso + && \text{lemma} \\ + %% β‰‘βŸ¨βŸ© \\ + & ≑ + \isoToId \comp \idToIso + && \text{$\shufflef$ is an isomorphism} \\ + & ≑ + \identity + && \text{$\isoToId$ is an isomorphism} \end{align*} % The other direction is analogous. The lemma used in step 2 of this proof states that $\wideoverbar{idToIso} ≑ -\inv{\shufflef} \comp \idToIso$. This is a rather straightforward 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. -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: +This finished the proof that the opposite category is in fact a category. Now, +to prove that opposite-of is an involution we must show: % $$ ∏_{\bC \tp \Category} \left(\bC^{\var{Op}}\right)^{\var{Op}} ≑ \bC $$ % -As we have seen the laws in $\left(\bC^{\var{Op}}\right)^{\var{Op}}$ get quite -involved\footnote{We have not even seen the full story because we have used - this `interface' for equivalences.}. Luckily since being-a-category is a mere -proposition, we need not concern ourselves with this bit when proving the above. -We can use the equality principle for categories that let us prove an equality -just by giving an equality on the data-part. So, given a category $\bC$ all we -must provide is the following proof: +The laws in $\left(\bC^{\var{Op}}\right)^{\var{Op}}$ get quite +involved. Luckily since being-a-category is a mere proposition, we +need not concern ourselves with this bit when proving the above. We +can use the equality principle for categories that let us prove an +equality just by giving an equality on the data-part. So, given a +category $\bC$ all we must provide is the following proof: % $$ \var{raw}\ \left(\bC^{\var{Op}}\right)^{\var{Op}} ≑ \var{raw}\ \bC $$ % -And these are judgmentally the same. I remind the reader that the left-hand side +And these are judgmentally the same. I remind the reader that the left-hand side is constructed by flipping the arrows, which judgmentally is an involution. \subsection{Category of sets} The category of sets has as objects, not types, but only those types that are -homotopic sets. This is encapsulated in Agda with the following type: +homotopic sets. This is encapsulated in Agda with the following type: % $$\Set β‰œ βˆ‘_{A \tp \MCU} \isSet\ A$$ % The more straightforward notion of a category where the objects are types is -not a valid \mbox{(1-)category}. This stems from the fact that types in cubical -Agda types can have higher homotopic structure. +not a valid \mbox{(1-)category}. This stems from the fact that types in cubical +Agda can have higher homotopic structure. Univalence does not follow immediately from univalence for types: % @@ -693,7 +715,7 @@ $$(A ≑ B) ≃ (A ≃ B)$$ % Because here $A, B \tp \Type$ whereas the objects in this category have the type $\Set$ so we cannot form the type $\var{hA} ≃ \var{hB}$ for objects -$\var{hA}\;\var{hB} \tp \Set$. In stead I show that this category +$\var{hA}\;\var{hB} \tp \Set$. In stead I show that this category satisfies: % $$ @@ -701,96 +723,95 @@ $$ $$ % 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 +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: % \begin{align*} -((A, s_A) ≑ (B, s_B)) - & ≃ (A ≑ B) && \ref{eq:equivPropSig} \\ - & ≃ (A ≃ B) && \text{Univalence} \\ - & ≃ ((A, s_A) β‰Š (B, s_B)) && \text{\ref{eq:equivSig} and \ref{eq:equivIso}} + ((A, s_A) ≑ (B, s_B)) + & ≃ (A ≑ B) && \ref{eq:equivPropSig} \\ + & ≃ (A ≃ B) && \text{Univalence} \\ + & ≃ ((A, s_A) β‰Š (B, s_B)) && \text{\ref{eq:equivSig} and \ref{eq:equivIso}} \end{align*} And since $≃$ is an equivalence relation we can chain these equivalences -together. Step one will be proven with the following lemma: +together. Step one will be proven with the lemma: % \begin{align} \label{eq:equivPropSig} -\left(∏_{a \tp A} \isProp\ (P\ a)\right) β†’ ∏_{x\;y \tp βˆ‘_{a \tp A} P\ a} (x ≑ y) ≃ (\fst\ x ≑ \fst\ y) + \left(∏_{a \tp A} \isProp\ (P\ a)\right) β†’ ∏_{x\;y \tp βˆ‘_{a \tp A} P\ a} (x ≑ y) ≃ (\fst\ x ≑ \fst\ y) \end{align} % -The lemma states that for pairs whose second component are mere propositions -equality is equivalent to equality of the first components. In this case the -type-family $P$ is $\isSet$ which itself is a proposition for any type $A \tp -\Type$. Step two is univalence. Step three will be proven with the following -lemma: +The lemma states that for pairs whose second component are mere +propositions equality is equivalent to equality of the first +components. In this case the type-family $P$ is $\isSet$ which itself +is a proposition for any type $A \tp \Type$. Step two is univalence +for types. Step three will be proven with the following lemma: % \begin{align} \label{eq:equivSig} -∏_{a \tp A} \left( P\ a ≃ Q\ a \right) β†’ βˆ‘_{a \tp A} P\ a ≃ βˆ‘_{a \tp A} Q\ a + ∏_{a \tp A} \left( P\ a ≃ Q\ a \right) β†’ βˆ‘_{a \tp A} P\ a ≃ βˆ‘_{a \tp A} Q\ a \end{align} % 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 β‰œ \isEquiv\ A\ B$ and $Q β‰œ -\Isomorphism$. So we must finally prove: +also be equivalent. For our purposes $P β‰œ \isEquiv\ A\ B$ and $Q β‰œ +\Isomorphism$. So we must finally prove: % \begin{align} \label{eq:equivIso} -∏_{f \tp A β†’ B} \left( \isEquiv\ A\ B\ f ≃ \Isomorphism\ f \right) + ∏_{f \tp A β†’ B} \left( \isEquiv\ A\ B\ f ≃ \Isomorphism\ f \right) \end{align} -First, lets prove \ref{eq:equivPropSig}: Let $propP \tp ∏_{a \tp A} \isProp\ (P\ a)$ and $x\;y \tp βˆ‘_{a \tp A} P\ a$ be given. Because +First, lets prove \ref{eq:equivPropSig}: Let $propP \tp ∏_{a \tp A} \isProp\ (P\ a)$ and $x\;y \tp βˆ‘_{a \tp A} P\ a$ be given. Because of $\var{fromIsomorphism}$ it suffices to give an isomorphism between $x ≑ y$ and $\fst\ x ≑ \fst\ y$: % %% FIXME: Too much alignement? \begin{equation*} -\begin{aligned} - f & β‰œ \congruence\ \fst + \begin{aligned} + f & β‰œ \congruence\ \fst && \tp x ≑ y && β†’ \fst\ x ≑ \fst\ y \\ - g & β‰œ \var{lemSig}\ \var{propP}\ x\ y + g & β‰œ \var{lemSig}\ \var{propP}\ x\ y && \tp \fst\ x ≑ \fst\ y && β†’ x ≑ y -\end{aligned} + \end{aligned} \end{equation*} % -\TODO{Is it confusing that I use point-free style here?}Here $\var{lemSig}$ is -a lemma that says that if the second component of a pair is a proposition, it -suffices to give a path between its first components to construct an equality of -the two pairs: +Here $\var{lemSig}$ is a lemma that says that if the second component +of a pair is a proposition, it suffices to give a path between its +first components to construct an equality of the two pairs: % \begin{align*} -\var{lemSig} \tp \left( ∏_{x \tp A} \isProp\ (B\ x) \right) β†’ -∏_{u\; v \tp βˆ‘_{a \tp A} B\ a} + \var{lemSig} \tp \left( ∏_{x \tp A} \isProp\ (B\ x) \right) β†’ + ∏_{u\; v \tp βˆ‘_{a \tp A} B\ a} \left( \fst\ u ≑ \fst\ v \right) β†’ u ≑ v \end{align*} % -The proof that these are indeed inverses has been omitted. The details -can be found in the module: +The proof that these are indeed inverses of one another has been +omitted. The details can be found in the module: \begin{center} -\sourcelink{Cat.Categories.Sets} + \sourcelink{Cat.Categories.Sets} \end{center} Now to prove \ref{eq:equivSig}: Let $e \tp ∏_{a \tp A} \left( P\ a -≃ Q\ a \right)$ be given. To prove the equivalence, it suffices +≃ Q\ a \right)$ be given. To prove the equivalence it suffices to give an isomorphism between $βˆ‘_{a \tp A} P\ a$ and $βˆ‘_{a \tp A} Q\ a$, but since they have identical first components it suffices to give an isomorphism between $P\ a$ and $Q\ a$ for all $a \tp A$. This is exactly what we can get from the equivalence $e$.\QED -Lastly we prove \ref{eq:equivIso}. Let $f \tp A β†’ B$ be given. For the maps we +Lastly we prove \ref{eq:equivIso}. Let $f \tp A β†’ B$ be given. For the maps we choose: % \begin{align*} -\var{toIso} + \var{toIso} & \tp \isEquiv\ f β†’ \Isomorphism\ f \\ -\var{fromIso} + \var{fromIso} & \tp \Isomorphism\ f β†’ \isEquiv\ f \end{align*} % -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: +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*} \var{fromIso} \comp \var{toIso} ≑ \identity_{\isEquiv\ f} @@ -803,13 +824,13 @@ For the other direction: \var{toIso} \comp \var{fromIso} ≑ \identity_{\Isomorphism\ f} \end{align*} % -We will show that $\Isomorphism\ f$ is also a mere proposition. To this -end, let $X\;Y \tp \Isomorphism\ f$ be given. Name the maps $x\;y \tp B -β†’ A$ respectively. Now, the proof that $X$ and $Y$ are the same is a pair of -paths: $p \tp x ≑ y$ and $\Path\ (\lambda\; i β†’ -\var{AreInverses}\ f\ (p\ i))\ \mathcal{X}\ \mathcal{Y}$ where $\mathcal{X}$ -and $\mathcal{Y}$ denotes the witnesses that $x$ (respectively $y$) is an -inverse to $f$. The path $p$ is inhabited by: +We will show that $\Isomorphism\ f$ is also a mere proposition. To +this end, let $X, Y \tp \Isomorphism\ f$ be given. Name the maps $x, y +\tp B β†’ A$ respectively. Now, the proof that $X$ and $Y$ are the same +is a pair of paths: $p \tp x ≑ y$ and $\Path\ (\lambda\; i β†’ +\var{AreInverses}\ f\ (p\ i))\ \mathcal{X}\ \mathcal{Y}$ where +$\mathcal{X}$ and $\mathcal{Y}$ denotes the witnesses that $x$ +(respectively $y$) is an inverse to $f$. The path $p$ is inhabited by: % \begin{align*} x @@ -823,11 +844,11 @@ inverse to $f$. The path $p$ is inhabited by: \end{align*} % For the other (dependent) path we can prove that being-an-inverse-of is a -proposition and then use $\lemPropF$. So we prove the generalization: +proposition and then use $\lemPropF$. So we prove the generalization: % \begin{align} -\label{eq:propAreInversesGen} -∏_{g \tp B β†’ A} \isProp\ (\var{AreInverses}\ f\ g) + \label{eq:propAreInversesGen} + ∏_{g \tp B β†’ A} \isProp\ (\var{AreInverses}\ f\ g) \end{align} % But $\var{AreInverses}\ f\ g$ is a pair of equations on arrows, so we use @@ -835,7 +856,7 @@ $\propSig$ and the fact that both $A$ and $B$ are sets to close this proof. %% \subsection{Category of categories} -%% Note that this category does in fact not exist. In stead I provide +%% Note that this category does in fact not exist. In stead I provide %% the definition of the ``raw'' category as well as some of the laws. %% Furthermore I provide some helpful lemmas about this raw category. @@ -843,65 +864,67 @@ $\propSig$ and the fact that both $A$ and $B$ are sets to close this proof. %% such a category. %% These lemmas can be used to provide the actual exponential object -%% in a context where we have a witness to this being a category. This +%% in a context 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} \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 +demonstrated. The goal in this section is to show that products are propositions: % $$ ∏_{\bC \tp \Category} ∏_{A\;B \tp \Object} \isProp\ (\var{Product}\ \bC\ A\ B) $$ % -Where $\var{Product}\ \bC\ A\ B$ denotes the type of products of objects $A$ -and $B$ in the category $\bC$. I do this by constructing a category whose -terminal objects are equivalent to products in $\bC$, and since terminal objects -are propositional in a proper category and equivalences preserve homotopy level, -then we know that products also are propositions. But before we get to that, -we recall the definition of products. +Where $\var{Product}\ \bC\ A\ B$ denotes the type of products of +objects $A$ and $B$ in the category $\bC$. I do this by constructing a +category whose terminal objects are equivalent to products in $\bC$, +and since terminal objects are propositional in a proper category and +equivalences preserve homotopy level, then we know that products are +also propositions. But before we get to that, we recall the definition +of products. \subsection{Definition of products} -Given a category $\bC$ and two objects $A$ and $B$ in $\bC$ we define the -product (object) of $A$ and $B$ to be an object $A \x B$ in $\bC$ and two arrows -$\pi_1 \tp A \x B β†’ A$ and $\pi_2 \tp A \x B β†’ B$ called the projections of -the product. The projections must satisfy the following property: +Given a category $\bC$ and two objects $A$ and $B$ in $\bC$ we say +that a product is triple consisting of an object and a pair of arrows. +The object is denoted with $A Γ— B$ in $\bC$ and is also referred to as +the product (object) of $A$ and $B$. The arrows will be named $\pi_1 +\tp A \x B β†’ A$ and $\pi_2 \tp A \x B β†’ B$ also called the projections +of the product. The projections must satisfy the following property: For all $X \tp Object$, $f \tp \Arrow\ X\ A$ and $g \tp \Arrow\ X\ B$ we have that there exists a unique arrow $\pi \tp \Arrow\ X\ (A \x B)$ satisfying % \begin{align} -\label{eq:umpProduct} -%% ∏_{X \tp Object} ∏_{f \tp \Arrow\ X\ A} ∏_{g \tp \Arrow\ X\ B}\\ -%% \uexists_{f \x g \tp \Arrow\ X\ (A \x B)} -\pi_1 \lll \pi ≑ f \x \pi_2 \lll \pi ≑ g + \label{eq:umpProduct} + %% ∏_{X \tp Object} ∏_{f \tp \Arrow\ X\ A} ∏_{g \tp \Arrow\ X\ B}\\ + %% \uexists_{f \x g \tp \Arrow\ X\ (A \x B)} + \pi_1 \lll \pi ≑ f \x \pi_{2} \lll \pi ≑ g \end{align} % -$\pi$ is called the product (arrow) of $f$ and $g$. - +The arrow $\pi$ is called the product (arrow) of $f$ and $g$. +% \subsection{Span category} -Given a base category $\bC$ and two objects in this category $\pairA$ and -$\pairB$ we can construct the \nomenindex{span category}: - -The type of objects in this category will be an object in the underlying +Given a base category $\bC$ and two objects in this category $\pairA$ +and $\pairB$ we construct the \nomenindex{span category}. The type of +objects in this category shall be an object in the underlying category, $X$, and two arrows (also from the underlying category) $\Arrow\ X\ \pairA$ and $\Arrow\ X\ \pairB$. \newcommand\pairf{\ensuremath{f}} \newcommand\pairFst{\mathcal{\pi_1}} -\newcommand\pairSnd{\mathcal{\pi_2}} +\newcommand\pairSnd{\mathcal{\pi_{2}}} -An arrow between objects $A ,\ a_0 ,\ a_1$ and $B ,\ b_0 ,\ b_1$ in this +An arrow between objects $A ,\ a_{\pairA} ,\ a_{\pairB}$ and $B ,\ b_{\pairA} ,\ b_{\pairB}$ in this category will consist of an arrow from the underlying category $\pairf \tp \Arrow\ A\ B$ satisfying: % \begin{align} -\label{eq:pairArrowLaw} -b_0 \lll f ≑ a_0 \x -b_1 \lll f ≑ a_1 + \label{eq:pairArrowLaw} + b_{\pairA} \lll f ≑ a_{\pairA} \x + b_{\pairB} \lll f ≑ a_{\pairB} \end{align} The identity morphism is the identity morphism from the underlying category. @@ -913,27 +936,27 @@ choose $g \lll f$ and we must now verify that it satisfies \ref{eq:pairArrowLaw}: % \begin{align*} - c_0 \lll (f \lll g) + c_{\pairA} \lll (f \lll g) & ≑ - (c_0 \lll f) \lll g + (c_{\pairA} \lll f) \lll g && \text{Associativity} \\ & ≑ - b_0 \lll g + b_{\pairA} \lll g && \text{$f$ satisfies \ref{eq:pairArrowLaw}} \\ & ≑ - a_0 + a_{\pairA} && \text{$g$ satisfies \ref{eq:pairArrowLaw}} \\ \end{align*} % -Now we must verify the category-laws. For all the laws we will follow the +Now we must verify the category-laws. For all the laws we will follow the pattern of using the law from the underlying category, and that the type of -arrows form a set. For instance, to prove associativity we must prove that +arrows form a set. For instance, to prove associativity we must prove that % \begin{align} -\label{eq:productAssoc} -\overline{h} \lll (\overline{g} \lll \overline{f}) -≑ -(\overline{h} \lll \overline{g}) \lll \overline{f} + \label{eq:productAssoc} + \overline{h} \lll (\overline{g} \lll \overline{f}) + ≑ + (\overline{h} \lll \overline{g}) \lll \overline{f} \end{align} % Here $\lll$ refers to the `embellished' composition and $\overline{f}$, @@ -942,48 +965,51 @@ underlying category ($f$, $g$ and $h$) and a pair of witnesses to \ref{eq:pairArrowLaw}. %% Luckily those winesses are paths in the hom-set of the %% underlying category which is a set, so these are mere propositions. -The proof obligations is consists of two things. The first one is: +The proof obligations consists of two things. The first one is: % \begin{align} -\label{eq:productAssocUnderlying} -h \lll (g \lll f) -≑ -(h \lll g) \lll f + \label{eq:productAssocUnderlying} + h \lll (g \lll f) + ≑ + (h \lll g) \lll f \end{align} % And the other proof obligation is that the witness to \ref{eq:pairArrowLaw} for the left-hand-side and the right-hand-side are the same. -The proof of the first goal comes directly from the underlying category. The -type of the second goal is very complicated. I will not write it out in full -here, but it suffices to show the type of the path-space. Note that the arrows -in \ref{eq:productAssoc} are arrows from $\mathcal{A} = (A , a_{\pairA} , -a_{\pairB})$ to $\mathcal{D} = (D , d_{\pairA} , d_{\pairB})$ where -$a_{\pairA}$, $a_{\pairB}$, $d_{\pairA}$ and $d_{\pairB}$ are arrows in the -underlying category. Given that $p$ is the chosen proof of +The proof of the first goal comes directly from the underlying +category. The type of the second goal is very complicated. I will not +write it out in full here, but for the purpose of the present +exposition it will suffices to show the type of the path-space. Note +that the arrows in \ref{eq:productAssoc} are arrows between objects on +the form $\wideoverbar{A} = (A , a_{\pairA} , a_{\pairB})$ to +$\wideoverbar{D} = (D , d_{\pairA} , d_{\pairB})$ where $a_{\pairA}$, +$a_{\pairB}$, $d_{\pairA}$ and $d_{\pairB}$ are arrows in the +underlying category. Given that $p$ is the chosen proof of \ref{eq:productAssocUnderlying} we then have that the witness to \ref{eq:pairArrowLaw} vary over the type: % \begin{align} -\label{eq:productPath} -λ \; i β†’ d_{\pairA} \lll p\ i ≑ 2 a_{\pairA} Γ— d_{\pairB} \lll p\ i ≑ a_{\pairB} + \label{eq:productPath} + λ \; i β†’ d_{\pairA} \lll p\ i ≑ a_{\pairA} Γ— d_{\pairB} \lll p\ i ≑ a_{\pairB} \end{align} % And these paths are in the type of the hom-set of the underlying category, so -they are mere propositions. We cannot apply the fact that arrows in $\bC$ are +they are mere propositions. We cannot apply the fact that arrows in $\bC$ are sets directly, however, since $\isSet$ only talks about non-dependent paths, in stead we generalize \ref{eq:productPath} to: % \begin{align} -\label{eq:productEqPrinc} -∏_{f \tp \Arrow\ X\ Y} \isProp\ \left( y_{\pairA} \lll f ≑ x_{\pairA} Γ— y_{\pairB} \lll f ≑ x_{\pairB} \right) + \label{eq:productEqPrinc} + ∏_{f \tp \Arrow\ X\ Y} \isProp\ \left( y_{\pairA} \lll f ≑ x_{\pairA} Γ— y_{\pairB} \lll f ≑ x_{\pairB} \right) \end{align} % -For all objects $X , x_{\pairA} , x_{\pairB}$ and $Y , y_{\pairA} , y_{\pairB}$, -but this follows from pairs preserving homotopical structure and arrows in the -underlying category being sets. This gives us an equality principle for arrows -in this category that says that to prove two arrows $f, f_0, f_1$ and $g, g_0, -g_1$ equal it suffices to give a proof that $f$ and $g$ are equal. +For all objects $X , x_{\pairA} , x_{\pairB}$ and $Y , y_{\pairA} , +y_{\pairB}$, but this follows from the fact that $∏$ and $βˆ‘$ preserve +homotopical structure. This gives us an equality principle for arrows +in this category that says that to prove two arrows $f, f_0, f_1$ and +$g, g_0, g_1$ equal it suffices to give a proof that $f$ and $g$ are +equal. %% % %% $$ %% ∏_{(f, f_0, f_1)\; (g,g_0,g_1) \tp \Arrow\ X\ Y} f ≑ g \to (f, f_0, f_1) ≑ (g,g_0,g_1) @@ -995,22 +1021,23 @@ And thus we have proven \ref{eq:productAssoc} simply with Now we must prove that arrows form a set: % $$ -\isSet\ (\Arrow\ \mathcal{X}\ \mathcal{Y}) +\isSet\ (\Arrow\ \wideoverbar{X}\ \wideoverbar{Y}) $$ % -Since pairs preserve homotopical structure this reduces to: +Since pairs preserve homotopical structure this reduces to the two +obligations: % $$ -\isSet\ (\Arrow_{\bC}\ X\ Y) +\isSet\ (\bC.\Arrow\ X\ Y) $$ % -Which holds. And +Which holds. And % $$ ∏_{f \tp \Arrow\ X\ Y} \isSet\ \left( y_{\pairA} \lll f ≑ x_{\pairA} - Γ— y_{\pairB} \lll f ≑ x_{\pairB} - \right) +Γ— y_{\pairB} \lll f ≑ x_{\pairB} +\right) $$ % This we get from \ref{eq:productEqPrinc} and the fact that homotopical structure @@ -1024,7 +1051,7 @@ That is, for any two objects $\mathcal{X} = (X, x_{\mathcal{A}} , x_{\mathcal{B} and $\mathcal{Y} = Y, y_{\mathcal{A}}, y_{\mathcal{B}}$ I will show: % \begin{align} -(\mathcal{X} ≑ \mathcal{Y}) \cong (\mathcal{X} β‰Š \mathcal{Y}) + (\mathcal{X} ≑ \mathcal{Y}) \cong (\mathcal{X} β‰Š \mathcal{Y}) \end{align} I do this by showing that the following sequence of types are isomorphic. @@ -1032,32 +1059,32 @@ I do this by showing that the following sequence of types are isomorphic. The first type is: % \begin{align} -\label{eq:univ-0} -(X , x_{\mathcal{A}} , x_{\mathcal{B}}) ≑ (Y , y_{\mathcal{A}} , y_{\mathcal{B}}) + \label{eq:univ-0} + (X , x_{\mathcal{A}} , x_{\mathcal{B}}) ≑ (Y , y_{\mathcal{A}} , y_{\mathcal{B}}) \end{align} % The next types will be the triple: % \begin{align} -\label{eq:univ-1} -\begin{split} -p \tp & X ≑ Y \\ -& \Path\ (λ \; i β†’ \Arrow\ (p\ i)\ \mathcal{A})\ x_{\mathcal{A}}\ y_{\mathcal{A}} \\ -& \Path\ (λ \; i β†’ \Arrow\ (p\ i)\ \mathcal{B})\ x_{\mathcal{B}}\ y_{\mathcal{B}} -\end{split} -%% \end{split} + \label{eq:univ-1} + \begin{split} + p \tp & X ≑ Y \\ + & \Path\ (λ \; i β†’ \Arrow\ (p\ i)\ \mathcal{A})\ x_{\mathcal{A}}\ y_{\mathcal{A}} \\ + & \Path\ (λ \; i β†’ \Arrow\ (p\ i)\ \mathcal{B})\ x_{\mathcal{B}}\ y_{\mathcal{B}} + \end{split} + %% \end{split} \end{align} The next type is very similar, but in stead of a path we will have an isomorphism, and create a path from this: % \begin{align} -\label{eq:univ-2} -\begin{split} -\var{iso} \tp & X β‰Š Y \\ -& \Path\ (λ \; i β†’ \Arrow\ (\widetilde{p}\ i)\ \mathcal{A})\ x_{\mathcal{A}}\ y_{\mathcal{A}} \\ -& \Path\ (λ \; i β†’ \Arrow\ (\widetilde{p}\ i)\ \mathcal{B})\ x_{\mathcal{B}}\ y_{\mathcal{B}} -\end{split} + \label{eq:univ-2} + \begin{split} + \var{iso} \tp & X β‰Š Y \\ + & \Path\ (λ \; i β†’ \Arrow\ (\widetilde{p}\ i)\ \mathcal{A})\ x_{\mathcal{A}}\ y_{\mathcal{A}} \\ + & \Path\ (λ \; i β†’ \Arrow\ (\widetilde{p}\ i)\ \mathcal{B})\ x_{\mathcal{B}}\ y_{\mathcal{B}} + \end{split} \end{align} % Where $\widetilde{p} β‰œ \isoToId\ \var{iso} \tp X ≑ Y$. @@ -1065,20 +1092,28 @@ Where $\widetilde{p} β‰œ \isoToId\ \var{iso} \tp X ≑ Y$. Finally we have the type: % \begin{align} -\label{eq:univ-3} -(X , x_{\mathcal{A}} , x_{\mathcal{B}}) β‰Š (Y , y_{\mathcal{A}} , y_{\mathcal{B}}) + \label{eq:univ-3} + (X , x_{\mathcal{A}} , x_{\mathcal{B}}) β‰Š (Y , y_{\mathcal{A}} , y_{\mathcal{B}}) \end{align} +% +So the proof is a chain of isomorphisms between the types +\ref{eq:univ-0}, \ref{eq:univ-1}, \ref{eq:univ-2} and +\ref{eq:univ-3}. I will highlight the most interesting bits of this +proof. For the full proof see the implementation in the module: +% +\begin{center} + \sourcelink{Cat.Categories.Span} +\end{center} \emph{Proposition} \ref{eq:univ-0} is isomorphic to \ref{eq:univ-1}: This is just an application of the fact that a path between two pairs $a_0, a_1$ and -$b_0, b_1$ corresponds to a pair of paths between $a_0,b_0$ and $a_1,b_1$ (check -the implementation for the details). +$b_0, b_1$ corresponds to a pair of paths between $a_0,b_0$ and $a_1,b_1$. \emph{Proposition} \ref{eq:univ-1} is isomorphic to \ref{eq:univ-2}: This proof of this has been omitted but can be found in the module: % \begin{center}% -\sourcelink{Cat.Categories.Span} + \sourcelink{Cat.Categories.Span} \end{center} % \emph{Proposition} \ref{eq:univ-2} is isomorphic to \ref{eq:univ-3}: For this I @@ -1090,54 +1125,56 @@ will show two corollaries of \ref{eq:coeCod}: For an isomorphism $(\iota, results % \begin{align} -\label{eq:domain-twist-0} -f & ≑ g \lll \iota \\ -\label{eq:domain-twist-1} -g & ≑ f \lll \inv{\iota} + \label{eq:domain-twist-0} + f & ≑ g \lll \iota \\ + \label{eq:domain-twist-1} + g & ≑ f \lll \inv{\iota} \end{align} % The proof is omitted but can be found in the module: \begin{center} -\sourcelink{Cat.Category} + \sourcelink{Cat.Category} \end{center} Now we can prove the equivalence in the following way: Given $(f, \inv{f}, \var{inv}_f) \tp X \cong Y$ and two heterogeneous paths % \begin{align*} -p_{\mathcal{A}} & \tp \Path\ (\lambda\; i β†’ p_{\var{dom}}\ i)\ x_{\mathcal{A}}\ y_{\mathcal{A}}\\ -% -q_{\mathcal{B}} & \tp \Path\ (\lambda\; i β†’ p_{\var{dom}}\ i)\ x_{\mathcal{B}}\ y_{\mathcal{B}} + p_{\mathcal{A}} & \tp \Path\ (\lambda\; i β†’ p_{\var{dom}}\ i)\ x_{\mathcal{A}}\ y_{\mathcal{A}}\\ + % + q_{\mathcal{B}} & \tp \Path\ (\lambda\; i β†’ p_{\var{dom}}\ i)\ x_{\mathcal{B}}\ y_{\mathcal{B}} \end{align*} % -all as in \ref{eq:univ-2}. I use $p_{\var{dom}}$ here again to mean the path -induced by the isomorphism $f, \inv{f}$. I must now construct an isomorphism -$(X, x_{\mathcal{A}}, x_{\mathcal{B}}) β‰Š (Y, y_{\mathcal{A}}, y_{\mathcal{B}})$ -as in \ref{eq:univ-3}. That is, an isomorphism in the present category. I remind -the reader that such a gadget is a triple. The first component shall be: +all as in \ref{eq:univ-2}. I use $p_{\var{dom}}$ here again to mean +the path induced by the isomorphism $(f, \inv{f}, \var{inv}_f)$. We +must now construct an isomorphism $(X, x_{\mathcal{A}}, +x_{\mathcal{B}}) β‰Š (Y, y_{\mathcal{A}}, y_{\mathcal{B}})$ as in +\ref{eq:univ-3}. That is, an isomorphism in the present category. I +remind the reader that such a gadget is a triple. The first component +shall be: % \begin{align} -f \tp \Arrow\ X\ Y + f \tp \Arrow\ X\ Y \end{align} % To show that this choice fits the bill I must now verify that it satisfies \ref{eq:pairArrowLaw}, which in this case becomes: % \begin{align} -(y_{\mathcal{A}} \lll f ≑ x_{\mathcal{A}}) Γ— (y_{\mathcal{B}} \lll f ≑ x_{\mathcal{B}}) + (y_{\mathcal{A}} \lll f ≑ x_{\mathcal{A}}) Γ— (y_{\mathcal{B}} \lll f ≑ x_{\mathcal{B}}) \end{align} % Which, since $f$ is an isomorphism and $p_{\mathcal{A}}$ (resp.\ $p_{\mathcal{B}}$) is a path varying according to a path constructed from this isomorphism, this is exactly what \ref{eq:domain-twist-0} gives us. % -The other direction is quite analogous. We choose $\inv{f}$ as the morphism and +The other direction is quite analogous. We choose $\inv{f}$ as the morphism and prove that it satisfies \ref{eq:pairArrowLaw} with \ref{eq:domain-twist-1}. -We must now show that this choice of arrows indeed form an isomorphism. Our -equality principle for arrows in this category (\ref{eq:productEqPrinc}) gives -us that it suffices to show that $f$ and $\inv{f}$, this is exactly -$\var{inv}_f$. +We must now show that this choice of arrows indeed form an +isomorphism. Our equality principle for arrows in this category +(\ref{eq:productEqPrinc}) gives us that it suffices to show that $f$ +and $\inv{f}$ are inverses, but this is of course just $\var{inv}_f$. This concludes the first direction of the isomorphism that we are constructing. For the other direction we are given the isomorphism: @@ -1161,70 +1198,70 @@ $$ This gives rise to the following paths: % \begin{align} -\begin{split} -\widetilde{p} & \tp X ≑ Y \\ -\widetilde{p}_{\mathcal{A}} & \tp \Arrow\ X\ \mathcal{A} ≑ \Arrow\ Y\ \mathcal{A} \\ -\widetilde{p}_{\mathcal{B}} & \tp \Arrow\ X\ \mathcal{B} ≑ \Arrow\ Y\ \mathcal{B} -\end{split} + \begin{split} + \widetilde{p} & \tp X ≑ Y \\ + \widetilde{p}_{\mathcal{A}} & \tp \Arrow\ X\ \mathcal{A} ≑ \Arrow\ Y\ \mathcal{A} \\ + \widetilde{p}_{\mathcal{B}} & \tp \Arrow\ X\ \mathcal{B} ≑ \Arrow\ Y\ \mathcal{B} + \end{split} \end{align} % 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}} -\end{split} + \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}} + \end{split} \end{align} % This is achieved with the following lemma: % \begin{align} -∏_{a \tp A} ∏_{b \tp B} ∏_{q \tp A ≑ B} \var{coe}\ q\ a ≑ b β†’ -\Path\ (λ \; i β†’ q\ i)\ a\ b + ∏_{a \tp A} ∏_{b \tp B} ∏_{q \tp A ≑ B} \var{coe}\ q\ a ≑ b β†’ + \Path\ (λ \; i β†’ q\ i)\ a\ b \end{align} % -Which is used without proof. See the implementation for the details. +Which is used without proof. See the implementation for the details. \ref{eq:product-paths} is then proven with the propositions: % \begin{align} -\begin{split} -%% \label{eq:product-paths} -\var{coe}\ \widetilde{p}_{\mathcal{A}}\ x_{\mathcal{A}} ≑ y_{\mathcal{A}}\\ -\var{coe}\ \widetilde{p}_{\mathcal{B}}\ x_{\mathcal{B}} ≑ y_{\mathcal{B}} -\end{split} + \begin{split} + %% \label{eq:product-paths} + \var{coe}\ \widetilde{p}_{\mathcal{A}}\ x_{\mathcal{A}} ≑ y_{\mathcal{A}}\\ + \var{coe}\ \widetilde{p}_{\mathcal{B}}\ x_{\mathcal{B}} ≑ y_{\mathcal{B}} + \end{split} \end{align} % The proof of the first one is: % \begin{align*} \var{coe}\ \widetilde{p}_{\mathcal{A}}\ x_{\mathcal{A}} - & ≑ x_{\mathcal{A}} \lll \fst\ \inv{f} && \text{\ref{eq:coeDom} and the isomorphism $f, \inv{f}$} \\ + & ≑ x_{\mathcal{A}} \lll \fst\ \inv{f} && \text{\ref{eq:coeDom} and the isomorphism $(f, \inv{f}, \var{inv}_{f})$} \\ & ≑ y_{\mathcal{A}} && \text{\ref{eq:pairArrowLaw} for $\inv{f}$} \end{align*} % -We have now constructed the maps between \ref{eq:univ-0} and \ref{eq:univ-1}. It -remains to show that they are inverses of each other. To cut a long story short, -the proof uses the fact that isomorphism-of is propositional and that arrows (in -both categories) are sets. The reader is referred to the implementation for the +We have now constructed the maps between \ref{eq:univ-0} and +\ref{eq:univ-1}. It remains to show that they are inverses of each +other. To cut a long story short, the proof uses the fact that +isomorphism-of is a proposition and that arrows (in both categories) +are sets. The reader is referred to the implementation for the full gory details. % \subsection{Products are propositions} % Now that we have constructed the span category\index{span category} I will demonstrate how to use this to prove that products are -propositions. On the face of it this may seem surprising. Products -look like they are a structure on categories. After all it consist of -a select element and two arrows given some two objects. If formulated -in set theory this would be the case but in the present setting -univalence of categories give us that products are properties. I will -show this by showing that terminal objects in the span category are -equivalent to products: +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 object and two arrows. If formulated in set theory this +would be the case but in the present setting univalence of categories +give us that products are properties. I will show this by showing +that terminal objects in the span category are equivalent to products: % \begin{align} -\var{Terminal} ≃ \var{Product}\ β„‚\ \mathcal{A}\ \mathcal{B} + \var{Terminal} ≃ \var{Product}\ β„‚\ \mathcal{A}\ \mathcal{B} \end{align} % And as always we do this by constructing an isomorphism: @@ -1237,49 +1274,50 @@ indeed a product. That is, for an object $Y$ and two arrows $y_π’œ \tp \Arrow\ Y\ X$ satisfying: % \begin{align} -\label{eq:pairCondRev} -%% \begin{split} + \label{eq:pairCondRev} + %% \begin{split} ( x_π’œ \lll f ≑ y_π’œ ) \x ( x_ℬ \lll f ≑ y_ℬ ) -%% \end{split} + %% \end{split} \end{align} % -Since $X, x_π’œ, x_ℬ$ is a terminal object there is a \emph{unique} arrow from -this object to any other object, so also $Y, y_π’œ, y_ℬ$ in particular (which is -also an object in the span category). The arrow we will play the role of $f$ and -it immediately satisfies \ref{eq:pairCondRev}. Any other arrow satisfying these +Since $X, x_π’œ, x_ℬ$ is a terminal object there is a \emph{unique} +arrow from this object to any other object, so in particular also $Y, +y_π’œ, y_ℬ$. The arrow we will play the role of $f$ and it immediately +satisfies \ref{eq:pairCondRev}. Any other arrow satisfying these conditions will be equal since $f$ is unique. -For the other direction we are now given a product $X, x_π’œ, x_ℬ$. Again this -will be the terminal object. So now it remains that for any other object there -is a unique arrow from that object into $X, x_π’œ, x_ℬ$. Let $Y, y_π’œ, y_ℬ$ be -another object. As the arrow $\Arrow\ Y\ X$ we choose the product-arrow $y_π’œ \x -y_ℬ$. Since this is a product-arrow it satisfies \ref{eq:pairCondRev}. Let us -name the witness to this $\phi_{y_π’œ \x y_ℬ}$. So we have picked as our center of -contraction $y_π’œ \x y_ℬ , \phi_{y_π’œ \x y_ℬ}$ we must now show that it is -contractible. So let $f \tp \Arrow\ X\ Y$ and $\phi_f$ be given (here $\phi_f$ -is the proof that $f$ satisfies \ref{eq:pairCondRev}). The proof will be a pair -of proofs: +For the other direction we are now given a product $X, x_π’œ, x_ℬ$. +Again this will be the terminal object. So now it remains that for +any other object there is a unique arrow from that object into $X, +x_π’œ, x_ℬ$. Let $Y, y_π’œ, y_ℬ$ be another object. As the arrow +$\Arrow\ Y\ X$ we choose the product-arrow $y_π’œ \x y_ℬ$. Since this +is a product-arrow it satisfies \ref{eq:pairCondRev}. Let us name the +witness to this $\phi_{y_π’œ \x y_ℬ}$. So we have picked as our center +of contraction $y_π’œ \x y_ℬ , \phi_{y_π’œ \x y_ℬ}$ we must now show that +it is contractible. So let $f \tp \Arrow\ X\ Y$ and $\phi_f$ be given +(here $\phi_f$ is the proof that $f$ satisfies \ref{eq:pairCondRev}). +The proof will be a pair of proofs: % \begin{alignat}{3} p \tp & \Path\ (\lambda\; i β†’ \Arrow\ X\ Y)\quad - && f\quad && y_π’œ \x y_ℬ \\ + && f\quad && y_π’œ \x y_ℬ \\ & \Path\ (\lambda\; i β†’ \Phi\ (p\ i))\quad - && \phi_f\quad && \phi_{y_π’œ \x y_ℬ} + && \phi_f\quad && \phi_{y_π’œ \x y_ℬ} \end{alignat} % Here $\Phi$ is given as: $$ ∏_{f \tp \Arrow\ Y\ X} - ( x_π’œ \lll f ≑ y_π’œ ) - Γ— - ( x_ℬ \lll f ≑ y_ℬ ) +( x_π’œ \lll f ≑ y_π’œ ) +Γ— +( x_ℬ \lll f ≑ y_ℬ ) $$ % -$p$ follows from the universal property of $y_π’œ \x y_ℬ$. For the latter we will -again use the same trick we did in \ref{eq:propAreInversesGen} and prove this -more general result: +We can construct $p$ from the universal property of $y_π’œ \x y_ℬ$. For +the latter we use the same trick we did in \ref{eq:propAreInversesGen} +and prove this more general result: % $$ ∏_{f \tp \Arrow\ Y\ X} \isProp\ ( @@ -1289,30 +1327,31 @@ $$ ) $$ % -Which follows from arrows being sets and pairs preserving such. Thus we can +Which follows from arrows being sets and pairs preserving such. Thus we can close the final proof with an application of $\lemPropF$. -This concludes the proof $\var{Terminal} ≃ -\var{Product}\ β„‚\ \mathcal{A}\ \mathcal{B}$ and since we have that equivalences -preserve homotopic levels along with \ref{eq:termProp} we get our final result. -That in any category: +This concludes the proof +$\var{Terminal} ≃ \var{Product}\ β„‚\ \mathcal{A}\ \mathcal{B}$ +and since we have that equivalences preserve homotopic levels along +with \ref{eq:termProp} we get our final result. That is, in any +category $\bC$ we have: % \begin{align} -∏_{A, B \tp \Object} \isProp\ (\var{Product}\ \bC\ A\ B) + ∏_{A, B \tp \Object} \isProp\ (\var{Product}\ \bC\ A\ B) \end{align} % \section{Functors and natural transformations} -For the sake of completeness I will mention the definition of functors -and natural transformations. Please refer to the implementation for -the full details. +For the sake of completeness I will briefly mention the definition of +functors and natural transformations. Please refer to the +implementation for the full details. % \subsection{Functors} Given two categories $\bC$ and $\bD$ a functor consists of the following data: % \begin{align*} - \omapF & \tp β„‚.\Object β†’ 𝔻.\Object \\ - \fmap & \tp β„‚.\Arrow\ A\ B β†’ 𝔻.\Arrow\ (\omapF\ A)\ (\omapF\ B) + \omapF & \tp β„‚.\Object β†’ 𝔻.\Object \\ + \fmap & \tp β„‚.\Arrow\ A\ B β†’ 𝔻.\Arrow\ (\omapF\ A)\ (\omapF\ B) \end{align*} % And the following laws: @@ -1327,16 +1366,17 @@ The implementation can be found here: \sourcelink{Cat.Category.Functor} \end{center} \subsection{Natural Transformation} -Given two functors between categories $\bC$ and $\bD$. Name them -$\FunF$ and $\FunG$. A natural transformation is a family of arrows: +\label{sec:nat-trans} +Given two functors between categories $\bC$ and $\bD$. Name them +$\FunF$ and $\FunG$. A natural transformation is a family of arrows: % \begin{align*} ∏_{C \tp β„‚.\Object} \bD.\Arrow\ (\omapF\ C)\ (\omapG\ C) \end{align*} % -This family of arrows can be seen as the data. If $\theta$ is a +This family of arrows can be seen as the data. If $\theta$ is a natural transformation $\theta\ C$ will be called the component (of -$\theta$) at $C$. The laws of this family of morphism is the +$\theta$) at $C$. The laws of this family of morphism is the naturality condition: % \begin{align*} @@ -1352,20 +1392,20 @@ The implementation can be found here: \section{Monads} \label{sec:monads} -In this section I present two formulations of monads. The two representations -are referred to as the monoidal- and Kleisli- representation respectively or -simply monoidal monads and Kleisli monads for short. We then show that the two -formulations are equivalent, which due to univalence gives us a path between the -two types. +In this section I present two formulations of monads. The two +representations are referred to as the monoidal- and Kleisli- +representation respectively or simply monoidal monads and Kleisli +monads. We then show that the two formulations are equivalent, which +due to univalence gives us a path between the two types. -Let a category $\bC$ be given. In the remainder of this sections all +Let a category $\bC$ be given. In the remainder of this sections all objects and arrows will implicitly refer to objects and arrows in this -category. I will also use the notation $\EndoR$ to refer to an -endofunctor on this category. Its map on objects will be denoted -$\omapR$ and its map on arrows will be denoted $\fmap$. Likewise I +category. I will also use the notation $\EndoR$ to refer to an +endofunctor on this category. Its map on objects will be denoted +$\omapR$ and its map on arrows will be denoted $\fmap$. Likewise I will use the notation $\pureNT$ to refer to a natural transformation and its component at a given (implicit) object will be denoted -$\pure$. +$\pure$. This is the same notation as in \S\ref{sec:nat-trans}. % \subsection{Monoidal formulation} The monoidal formulation of monads consists of the following data: @@ -1374,18 +1414,16 @@ The monoidal formulation of monads consists of the following data: \label{eq:monad-monoidal-data} \begin{split} \EndoR & \tp \Functor\ β„‚\ \bC \\ - \pureNT & \tp \NT{\EndoR^0}{\EndoR} \\ - \joinNT & \tp \NT{\EndoR^2}{\EndoR} + \pureNT & \tp \NT{\widehat{\identity}}{\EndoR} \\ + \joinNT & \tp \NT{(\EndoR \oplus \EndoR)}{\EndoR} \end{split} \end{align} % -Here $\NTsym$ denotes natural transformations, the super-script in $\EndoR^2$ -Denotes the composition of $\EndoR$ with itself. By the same token $\EndoR^0$ is -a curious way of denoting the identity functor. This notation has been chosen -for didactic purposes. +Here $\NTsym$ denotes natural transformations and $\oplus$ means +functor composition. -Denote the arrow-map of $\EndoR$ as $\fmap$, then this data must satisfy the -following laws: +Note that $\fmap$ is $\EndoR$'s map on arrows. This data must satisfy +the following laws. % \begin{align} \label{eq:monad-monoidal-laws-0} @@ -1400,23 +1438,22 @@ following laws: % The implicit arguments to the arrows above have been left out and the objects they range over are universally quantified. - +% \subsection{Kleisli formulation} % The Kleisli-formulation consists of the following data: % \begin{align} -\begin{split} -\label{eq:monad-kleisli-data} -\omapR & \tp \Object β†’ \Object \\ -\pure & \tp % ∏_{X \tp Object} - \Arrow\ X\ (\omapR\ X) \\ - \bind & \tp % ∏_{X\;Y \tp Object} β†’ \Arrow\ X\ (\omapR\ Y) - \Arrow\ (\omapR\ X)\ (\omapR\ Y) -\end{split} + \begin{split} + \label{eq:monad-kleisli-data} + \omapR & \tp \Object β†’ \Object \\ + \pure & \tp % ∏_{X \tp Object} + \Arrow\ X\ (\omapR\ X) \\ + \bind & \tp \Arrow\ X\ (\omapR\ Y) β†’ \Arrow\ (\omapR\ X)\ (\omapR\ Y) + \end{split} \end{align} % -The objects $X$ and $Y$ are implicitly universally quantified. With this data we can construct the \nomenindex{Kleisli arrow}: +The objects $X$ and $Y$ are implicitly universally quantified. With this data we can construct the \nomenindex{Kleisli arrow}: % \begin{align*} \fish & \tp \Arrow\ A\ (\omapR\ B) @@ -1425,15 +1462,15 @@ The objects $X$ and $Y$ are implicitly universally quantified. With this data we f \fish g & β‰œ f \rrr (\bind\ g) \end{align*} % -It is interesting to note here that this formulation does not talk about natural -transformations or other such constructs from category theory. All we have here -is a regular maps on objects and a pair of arrows. +It is interesting to note here that this formulation does mention +functors nor natural transformations. All we have here is a regular +map on objects and a pair of arrows. % This data must satisfy: % \begin{align} \label{eq:monad-kleisli-laws-0} -\bind\ \pure & ≑ \identity_{\EndoR\ X} \\ +\bind\ \pure & ≑ \identity_{\omapR\ X} \\ \label{eq:monad-kleisli-laws-1} \pure \fish f & ≑ f \\ \label{eq:monad-kleisli-laws-2} @@ -1443,15 +1480,16 @@ This data must satisfy: % Here likewise the arrows $f \tp \Arrow\ X\ (\omapR\ Y)$ and $g \tp \Arrow\ Y\ (\omapR\ Z)$ are universally quantified as well as the -objects they range over. +objects they range over. The third law is stated in terms of reverse +function composition to mirror the way in which it interacts with the +Kleisli arrow. % \subsection{Equivalence of formulations} % -The notation I have chosen here in the report -overloads e.g.\ $\pure$ to both refer to a natural transformation and an arrow. -This is of course not a coincidence as the arrow in the Kleisli formulation -shall correspond exactly to the map on arrows from the natural transformation -called $\pure$. +Both formulations mention a map called $\pure$. This is of course no +coincidence as that arrow in the Kleisli formulation shall correspond +exactly to the map on arrows for the natural transformation in the +monoidal formulation. In the monoidal formulation we can define $\bind$: % @@ -1471,14 +1509,14 @@ And likewise in the Kleisli formulation we can define $\join$: \end{align} % It now remains to show that this construction indeed gives rise to a -monad. This will be done in two steps. First we will assume that we +monad. This will be done in two steps. First we will assume that we have a monad in the monoidal form; $(\EndoR, \pure, \join)$ and then show that $(\omapR, \pure, \bind)$ is indeed a monad in the Kleisli -form. In the second part we will show the other direction. +form. In the second part we will show the other direction. \subsubsection{Monoidal to Kleisli} Let $(\EndoR, \pureNT, \joinNT)$ be given as in \ref{eq:monad-monoidal-data} -satisfying the laws \monoidallaws. For the data of the Kleisli +satisfying the laws \monoidallaws. For the data of the Kleisli formulation we pick: % \begin{align} @@ -1492,8 +1530,8 @@ formulation we pick: Again $\omapR$ is the object map of the endo-functor $\EndoR$, $\pure$ and $\join$ are the arrows from the natural transformations $\pureNT$ and $\joinNT$ respectively and $\fmap$ is the map on arrows of the -endofunctor $\EndoR$. It now just remains to verify the laws -\kleislilaws. For \ref{eq:monad-kleisli-laws-0}: +endofunctor $\EndoR$. It now just remains to verify the laws +\kleislilaws. For \ref{eq:monad-kleisli-laws-0}: % \begin{align*} \bind\ \pure & = @@ -1525,7 +1563,7 @@ For \ref{eq:monad-kleisli-laws-2}: \join \lll \join \lll (\fmap \comp \fmap)\ f \lll \fmap\ g && \text{$\join$ is a natural transformation} \\ & ≑ \join \lll \fmap\ \join \lll (\fmap \comp \fmap)\ f \lll \fmap\ g -&& \text{By \ref{eq:monad-monoidal-laws-0}} \\ & ≑ +&& \text{By \ref{eq:monad-monoidal-laws-0}} \\ & = \join \lll \fmap\ \join \lll \fmap\ (\fmap\ f) \lll \fmap\ g && \text{} \\ & ≑ \join \lll \fmap\ (\join \lll \fmap\ f \lll g) @@ -1544,7 +1582,7 @@ The construction can be found in the module: % \subsubsection{Kleisli to Monoidal} For the other direction we are given $(\omapR, \pure, \bind)$ as in -\ref{eq:monad-kleisli-data} satisfying the laws \kleislilaws. For the data of +\ref{eq:monad-kleisli-data} satisfying the laws \kleislilaws. For the data of the monoidal formulation we pick: % \begin{align} @@ -1557,9 +1595,10 @@ the monoidal formulation we pick: % We must now not only show the monad laws given for the monoidal formulation (\monoidallaws), we must also verify that $\EndoR$ is a -functor and that $\pure$ and $\join$ are natural transformations. I -will ommit this here. In stead we shall see how these two mappings are -indeed inverses. The full construction can be found in the module: +functor and that $\pure$ and $\join$ are natural transformations. I +will ommit this here. In stead we shall see how these two mappings +are indeed inverses. The full construction can be found in the +module: \begin{center} \mbox{\sourcelink{Cat.Category.Monad.Kleisli}} \end{center} @@ -1567,7 +1606,7 @@ indeed inverses. The full construction can be found in the module: \subsubsection{Equivalence} To prove that the two formulations are equivalent we must demonstrate that the two mappings sketched above are indeed inverses of each -other. To recap, these maps are: +other. To recap, these maps are: % \begin{align*} \toKleisli & \tp \var{Kleisli} β†’ \var{Monoidal} \\ @@ -1575,10 +1614,10 @@ other. To recap, these maps are: β†’ (\EndoR, \pure, \bind\ \identity) \end{align*} % -Where $\EndoR β‰œ (\omapR, \bind\ (\pure \lll f))$. The proof that +Where $\EndoR β‰œ (\omapR, \bind\ (\pure \lll f))$. The proof that this is indeed a functor is left implicit as well as the monad laws. Likewise the proof that $\pure$ and $\bind\ \identity$ are natural -transformations are left implicit. The inverse map will be: +transformations are left implicit. The inverse map will be: % \begin{align*} \toMonoidal & \tp \var{Monoidal} β†’ \var{Kleisli} \\ @@ -1586,8 +1625,8 @@ transformations are left implicit. The inverse map will be: β†’ (\omapR, \pure, \bind) \end{align*} % -Where $\bind\ f β‰œ \join \lll \fmap\ f$. Again the monad laws are -left implicit. Now we must show: +Where $\bind\ f β‰œ \join \lll \fmap\ f$. Again the monad laws are +left implicit. Now we must show: % \begin{align} \label{eq:monad-forwards} @@ -1597,15 +1636,15 @@ left implicit. Now we must show: \end{align} % For \ref{eq:monad-forwards} let $(\omapR, \pure, \bind)$ be a monad in -the Kleisli form. Since being-a-monad is a proposition\footnote{The - proof can be found in the implementation.} we get an -equality-principle for kleisli-monads that say that to equate two such -monads it suffices to equate their data-part. So it suffices to equate -the data-parts of the \ref{eq:monad-forwards}. Such a proof is a -triple equating the three projections of \ref{eq:monad-kleisli-data}. -The first two hold definitionally -- essentially one just wraps and -unwraps the morphism in a functor. For the last equation a little more -work is required: +the Kleisli form. Since being-a-monad is a proposition\footnote{The + proof was omitted here but can be found in the implementation.} we +get an equality-principle for kleisli-monads that say that to equate +two such monads it suffices to equate their data-part. So it suffices +to equate the data-parts of the \ref{eq:monad-forwards}. Such a proof +is a triple equating the three projections of +\ref{eq:monad-kleisli-data}. The first two hold definitionally -- +essentially one just wraps and unwraps the morphism in a functor. For +the last equation a little more work is required: % \begin{align*} \join \lll \fmap\ f & = @@ -1620,11 +1659,11 @@ work is required: \end{align*} % For the other direction (\ref{eq:monad-backwards}) we are given a -monad in the monoidal form; $(\EndoR, \pureNT, \joinNT)$. The various +monad in the monoidal form; $(\EndoR, \pureNT, \joinNT)$. The various equality-principles again give us that it is sufficient to equate the -data-part of the above. That is, we only need to verify that the +data-part of the above. That is, we only need to verify that the following pieces of data: $\omapR$, $\fmap$, $\pure$ and $\join$ get -mapped correctly. To see the full details check the implementation in +mapped correctly. To see the full details check the implementation in the module: % \begin{center} diff --git a/doc/introduction.tex b/doc/introduction.tex index d4effb8..476b62c 100644 --- a/doc/introduction.tex +++ b/doc/introduction.tex @@ -207,13 +207,13 @@ with \nomenindex{extensional sets} $(X, \sim)$. That is a type $X \tp \MCU$ and an equivalence relation $\sim\ \tp X \to X \to \MCU$ on that type. Under the setoid interpretation the equivalence relation serve as a sort of ``local'' propositional equality. Since the developer -gets to pick this relation it is not a\~priori a congruence +gets to pick this relation it is not a~priori a congruence relation. So this must be verified manually by the developer. Furthermore, functions between different setoids must be shown to be setoid homomorphism, that is; they preserve the relation. This approach has other drawbacks; it does not satisfy all -propositional equalities of type theory a priori. That is, the +propositional equalities of type theory a\~priori. That is, the developer must manually show that e.g.\ the relation is a congruence. Equational proofs $a \sim_{X} b$ are in some sense `local' to the extensional set $(X , \sim)$. To e.g.\ prove that $x ∼ y β†’ f\ x ∼