From 545fb0ade6c0f7a630c23d2826d58d62a28142f9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 3 May 2018 14:18:51 +0200 Subject: [PATCH] Corrections --- doc/BACKLOG.md | 15 ----- doc/cubical.tex | 4 ++ doc/implementation.tex | 147 +++++++++++++++++++---------------------- doc/introduction.tex | 60 ++++++++--------- doc/main.tex | 5 +- 5 files changed, 105 insertions(+), 126 deletions(-) diff --git a/doc/BACKLOG.md b/doc/BACKLOG.md index b889c92..8bf5f45 100644 --- a/doc/BACKLOG.md +++ b/doc/BACKLOG.md @@ -1,22 +1,7 @@ -Remove stuff about models of type theory - -Add references to specific (noteable) implementaitons of category theory: -* Unimath -* cubicaltt -* https://github.com/pcapriotti/agda-categories -* https://github.com/copumpkin/categories -* ... - Talk about structure of library: === -Propositional- and non-propositional stuff split up -Providing "equiality principles" -Provide overview of what has been proven. - What can I say about reusability? Misc ==== - -Propositional content diff --git a/doc/cubical.tex b/doc/cubical.tex index 0fc8cbb..b7dc0e9 100644 --- a/doc/cubical.tex +++ b/doc/cubical.tex @@ -192,6 +192,7 @@ of these theorems here, as they will be used later in chapter \ref{ch:implementation} throughout. \subsection{Path induction} +\label{sec:pathJ} The induction principle for paths intuitively gives us a way to reason about a type-family indexed by a path by only considering if said path is $\refl$ (the ``base-case''). For \emph{based path induction}, that equaility is \emph{based} @@ -216,6 +217,7 @@ $$ $$ % \subsection{Paths over propositions} +\label{sec:lemPropF} Another very useful combinator is $\lemPropF$: To `promote' this to a dependent path we can use another useful combinator; @@ -258,6 +260,7 @@ $$ $$ % \subsection{Functions over propositions} +\label{sec:propPi} $\prod$-types preserve propositionality when the co-domain is always a proposition. % @@ -265,6 +268,7 @@ $$ \mathit{propPi} \tp \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\prod_{a \tp A} P\ a\right) $$ \subsection{Pairs over propositions} +\label{sec:propSig} % $\sum$-types preserve propositionality whenever it's first component is a proposition, and it's second component is a proposition for all points of in the diff --git a/doc/implementation.tex b/doc/implementation.tex index f1ad008..9c9597c 100644 --- a/doc/implementation.tex +++ b/doc/implementation.tex @@ -42,10 +42,11 @@ Another record encapsulates some laws about this data: associativity of composition, identity law for the identity morphism. These are standard requirements for being a category as can be found in standard mathematical expositions on the topic. We, however, impose one further requirement on what it -means to be a category, namely that the type of arrows form a set. We could -relax this requirement, this would give us the notion of higher categorier -(\cite[p. 307]{hott-2013}). For the purpose of this project, however, this -report will restrict itself to 1-categories. +means to be a category, namely that the type of arrows form a set. Such +categories are called \nomen{1-categories}. We could relax this requirement, +this would give us the notion of higher categorier (\cite[p. 307]{hott-2013}). +For the purpose of this project, however, this report will restrict itself to +1-categories. Raw categories satisfying these properties are called a pre-categories. @@ -68,8 +69,9 @@ $$ $$ % The two types are logically equivalent, however. 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. +from the former simply by ``forgetting'' that $\idToIso$ plays the role of the +equivalence. The other direction is more involved and will be discussed in +section \ref{sec:univalence}. 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 @@ -79,28 +81,21 @@ exactly because the type of arrows form a set, two witnesses must be the same. All the proofs are really quite mechanical. Lets have a look at one of them: The identity law states that: % -$$ -\prod_{A\ B \tp \Object} \prod_{f \tp A \to B} \id \comp f \equiv f \x f \comp \id \equiv f -$$ +\begin{equation} + \var{IsIdentity} \defeq + \prod_{A\ B \tp \Object} \prod_{f \tp A \to B} \id \comp f \equiv f \x f \comp \id \equiv f +\end{equation} % There are multiple ways to prove this. Perhaps one of the more intuitive proofs -is by way of the following `combinators': +is by way of the `combinators' $\propPi$ and $\propSig$ presented in sections +\ref{sec:propPi} and \ref{sec:propSig}: % -$$ -\mathit{propPi} \tp \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\prod_{a \tp A} P\ a\right) -$$ +\begin{align*} +\mathit{propPi} & \tp \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\prod_{a \tp A} P\ a\right) + \\ +\mathit{propSig} & \tp \isProp\ A \to \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\sum_{a \tp A} P\ a\right) +\end{align*} % -I.e.; pi-types preserve propositionality when the co-domain is always a -proposition. -% -$$ -\mathit{propSig} \tp \isProp\ A \to \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\sum_{a \tp A} P\ a\right) -$$ -% -I.e.; sigma-types preserve propositionality whenever it's first component is a -proposition, and it's second component is a proposition for all points of in the -left type. - So the proof goes like this: We `eliminate' the 3 function abstractions by applying $\propPi$ three times. So our proof obligation becomes: % @@ -135,13 +130,12 @@ $$ $$ % So let $a\ b \tp \IsPreCategory$ be given. To prove the equality $a \equiv b$ is -to give a continuous path from the index-type into path-space - in this case -$\IsPreCategory$. This path must satisfy being being judgmentally the same as -$a$ at the left endpoint and $b$ at the right endpoint. I.e. a function $I \to -\IsPreCategory$. 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 $\isIdentity_a$ and $\isIdentity_b$ -is simply formed by: +to give a continuous path from the index-type into the path-space. I.e. a +function $I \to \IsPreCategory$. This path must satisfy being being judgmentally +the same as $a$ at the left endpoint and $b$ at the right endpoint. We know we +can form a continuous path between all projections of $a$ and $b$, this follows +from the type of all the projections being mere propositions. For instance, the +path between $\isIdentity_a$ and $\isIdentity_b$ is simply formed by: % $$ \propIsIdentity\ \isIdentity_a\ \isIdentity_b \tp \isIdentity_a \equiv \isIdentity_b @@ -154,17 +148,18 @@ projections. Once we have such a path e.g. $p \tp \isIdentity_a \equiv \isIdentity_b$ we can elimiate it with $i$ and thus obtaining $p\ i \tp \isIdentity_{p\ i}$ and this element satisfies exactly that it corresponds to the corresponding projections at either endpoint. Thus the element we construct -at $i$ becomes: +at $i$ becomes the triple: % -\begin{align*} - & \{\ \mathit{propIsAssociative}\ \mathit{isAssociative}_x\ - \mathit{isAssociative}_y\ i \\ - & ,\ \mathit{propIsIdentity}\ \mathit{isIdentity}_x\ - \mathit{isIdentity}_y\ i \\ - & ,\ \mathit{propArrowsAreSets}\ \mathit{arrowsAreSets}_x\ - \mathit{arrowsAreSets}_y\ i \\ - & \} -\end{align*} +\begin{equation} +\begin{alignat}{4} + & \mathit{propIsAssociative} && x.\mathit{isAssociative}\ + && y.\mathit{isAssociative} && i \\ + & \mathit{propIsIdentity} && x.\mathit{isIdentity}\ + && y.\mathit{isIdentity} && i \\ + & \mathit{propArrowsAreSets} && x.\mathit{arrowsAreSets}\ + && y.\mathit{arrowsAreSets} && i +\end{alignat} +\end{equation} % I've found that this to be a general pattern when proving things in homotopy type theory, namely that you have to wrap and unwrap equalities at different @@ -181,11 +176,11 @@ 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. $\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 if we follow the same recipe as above, let $a\ b \tp -\IsCategory$, to show them equal, we now need to give two paths. One homogenous: +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 homogenous: % $$ -p_{\isPreCategory} \tp \isPreCategory_a \equiv \isPreCategory_b +p \tp \isPreCategory_a \equiv \isPreCategory_b $$ % and one heterogeneous: @@ -194,29 +189,23 @@ $$ \Path\ (\lambda\; i \mto Univalent_{p\ i})\ \isPreCategory_a\ \isPreCategory_b $$ % -Which depends on the choice of $p_{\isPreCategory}$. 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 becasue $\isProp$ talks about non-dependent paths. To -`promote' this to a dependent path we can use another useful combinator; -$\lemPropF$. Given a type $A \tp \MCU$ and a type family on $A$; $B \tp A \to -\MCU$. Let $P$ be a proposition indexed by an element of $A$ and say we have a -path between some two elements in $A$; $p \tp a_0 \equiv a_1$ then we can built a -heterogeneous path between any two $b$'s at the endpoints: -% -$$ -\Path\ (\lambda\; i \mto B\ (p\ i))\ b0\ b1 -$$ -% -where $b_0 \tp B a_0$ and $b_1 \tp B\ a_1$. This is quite a mouthful, but the -example at present should serve as an illustration. In this case $A = -\mathit{IsIdentity}\ \mathit{identity}$ and $B = \mathit{Univalent}$ we've 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_{\isPreCategory}$ by -applying using congruence of paths: $\congruence\ \mathit{isIdentity}\ -p_{\isPreCategory}$ +Which depends on the choice of $p$. The first of these we can provide since, as +we have shown, $\IsPreCategory$ is constantly a proposition. However, even +though $\Univalent$ is also a proposition, we cannot use this directly to show +the latter. This is becasue $\isProp$ talks about non-dependent paths. To +`promote' this to a dependent path we can use the combinator; $\lemPropF$ +introduced in \ref{sec:lemPropF}. +In this case $A = \mathit{IsIdentity}\ \mathit{identity}$ and $B = +\mathit{Univalent}$ we've 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 using congruence of paths: +% +$$ +\congruence\ \mathit{isIdentity}\ p +$$ +% When we have a proper category we can make precise the notion of ``identifying isomorphic types'' \TODO{cite awodey here}. That is, we can construct the function: @@ -311,7 +300,7 @@ the type $A \cong B$ as well as the the map $A \to B$ that witness this. Both $\cong$ and $\simeq$ form equivalence relations. \section{Univalence} -\label{univalence} +\label{sec:univalence} As noted in the introduction the univalence for types $A\; B \tp \Type$ states that: % @@ -342,16 +331,16 @@ equalities and isomorphisms (on arrows). It's 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 in any category since morphisms in a category are not regular maps -- -in stead they can be thought of as a generalization hereof; i.e. arrows. The -univalence criterion therefore is simply a way of restricting arrows to behave -similarly to maps. +univalence of all pre-category since morphisms in a category are not regular +maps -- in stead they can be thought of as a generalization hereof; i.e. arrows. +The univalence criterion therefore is simply a way of restricting arrows to +behave similarly to maps. I will now mention a few helpful thoerems that follow from univalence that will become useful later. -Obviously univalence gives us an isomorphism $A \equiv B \to A \approxeq B$. I -will name these for convenience: +Obviously univalence gives us an isomorphism between $A \equiv B$ and $A +\approxeq B$. I will name these for convenience: % $$ \idToIso \tp A \equiv B \to A \approxeq B @@ -366,8 +355,8 @@ an isomorphism $A \approxeq B$ in some category $\bC$ be given. Name the isomorphism $\iota \tp A \to B$ and its inverse $\widetilde{\iota} \tp B \to A$. Since $\bC$ is a category (and therefore univalent) the isomorphism induces a path $p \tp A \equiv B$. From this equality we can get two further paths: -$p_{\mathit{dom}} \tp \mathit{Arrow}\ A\ X \equiv \mathit{Arrow}\ A'\ X$ and -$p_{\mathit{cod}} \tp \mathit{Arrow}\ X\ A \equiv \mathit{Arrow}\ X\ A'$. We +$p_{\mathit{dom}} \tp \mathit{Arrow}\ A\ X \equiv \mathit{Arrow}\ B\ X$ and +$p_{\mathit{cod}} \tp \mathit{Arrow}\ X\ A \equiv \mathit{Arrow}\ X\ B$. We then have the following two theorems: % $$ @@ -394,11 +383,11 @@ isomorphism $\mathit{idToIso}\ p \tp A \cong B$. The helper-lemma is similar to what we're trying to prove but talks about paths rather than isomorphisms: % $$ -\prod_{f \tp \mathit{Arrow}\ A\ B} \prod_{p \tp A \equiv A'} \mathit{coe}\ p^*\ f \equiv f \lll \mathit{obverse}_{\mathit{idToIso}\ p} +\prod_{f \tp \mathit{Arrow}\ A\ B} \prod_{p \tp A \equiv B} \mathit{coe}\ p_\var{dom}\ f \equiv f \lll \mathit{obverse}_{\mathit{idToIso}\ p} $$ % -Note that the asterisk in $p^*$ denotes the path $\mathit{Arrow}\ A\ B \equiv -\mathit{Arrow}\ A'\ B$ induced by $p$. To prove this statement I let $f$ and $p$ +Again $p_\var{dom}$ denotes the path $\mathit{Arrow}\ A\ X \equiv +\mathit{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 \mathit{Object}$, so let $\widetilde{A} \tp \Object$ and $\widetilde{p} \tp A \equiv \widetilde{A}$ be given. The family that we perform induction over will @@ -551,7 +540,7 @@ $$ (\mathit{hA} \equiv \mathit{hB}) \simeq (\mathit{hA} \approxeq \mathit{hB}) $$ % -Which, as we saw in section \ref{univalence}, is sufficient to show that the +Which, as we saw in section \ref{sec:univalence}, is sufficient to show that the category is univalent. The way that I have shown this is with a three-step process. For objects $(A, s_A)\; (B, s_B) \tp \Set$ I show the following chain of equivalences: diff --git a/doc/introduction.tex b/doc/introduction.tex index 24442e9..6d4d98a 100644 --- a/doc/introduction.tex +++ b/doc/introduction.tex @@ -70,27 +70,27 @@ The proof obligation that this satisfies the identity law of functors % One needs functional extensionality to ``go under'' the function arrow and apply the (left) identity law of the underlying category to proove $\idFun \comp g -\equiv g$ and thus closing the goal. +\equiv g$ and thus close the goal. % \subsection{Equality of isomorphic types} % -Let $\top$ denote the unit type -- a type with a single constructor. In -the propositions-as-types interpretation of type theory $\top$ is the -proposition that is always true. The type $A \x \top$ and $A$ has an element for -each $a : A$. So in a sense they are the same. The second element of the pair -does not add any ``interesting information''. It can be useful to identify such -types. In fact, it is quite commonplace in mathematics. Say we look at a set -$\{x \mid -\phi\ x \land \psi\ x\}$ and somehow conclude that $\psi\ x \equiv \top$ for all -$x$. A mathematician would immediately conclude $\{x \mid \phi\ x \land -\psi\ x\} \equiv \{x \mid \phi\ x\}$ without thinking twice. Unfortunately such -an identification can not be performed in ITT. +Let $\top$ denote the unit type -- a type with a single constructor. In the +propositions-as-types interpretation of type theory $\top$ is the proposition +that is always true. The type $A \x \top$ and $A$ has an element for each $a : +A$. So in a sense they have the same shape (greek; \nomen{isomorphic}). The +second element of the pair does not add any ``interesting information''. It can +be useful to identify such types. In fact, it is quite commonplace in +mathematics. Say we look at a set $\{x \mid \phi\ x \land \psi\ x\}$ and somehow +conclude that $\psi\ x \equiv \top$ for all $x$. A mathematician would +immediately conclude $\{x \mid \phi\ x \land \psi\ x\} \equiv \{x \mid +\phi\ x\}$ without thinking twice. Unfortunately such an identification can not +be performed in ITT. More specifically; what we are interested in is a way of identifying -\nomen{equivalent} types. I will return to the definition of equivalence later, -but for now, it is sufficient to think of an equivalence as a one-to-one -correspondence. We write $A \simeq B$ to assert that $A$ and $B$ are equivalent -types. The principle of univalence says that: +\nomen{equivalent} types. I will return to the definition of equivalence later +in section \ref{sec:equiv}, but for now it is sufficient to think of an +equivalence as a one-to-one correspondence. We write $A \simeq B$ to assert that +$A$ and $B$ are equivalent types. The principle of univalence says that: % $$\mathit{univalence} \tp (A \simeq B) \simeq (A \equiv B)$$ % @@ -99,14 +99,14 @@ In particular this allows us to construct an equality from an equivalence \section{Formalizing Category Theory} % -The above examples serve to illustrate the limitation of Agda. One case where -these limitations are particularly prohibitive is in the study of Category -Theory. At a glance category theory can be described as ``the mathematical study -of (abstract) algebras of functions'' (\cite{awodey-2006}). So by that token +The above examples serve to illustrate a limitation of ITT. One case where these +limitations are particularly prohibitive is in the study of Category Theory. At +a glance category theory can be described as ``the mathematical study of +(abstract) algebras of functions'' (\cite{awodey-2006}). So by that token functional extensionality is particularly useful for formulating Category Theory. In Category theory it is also common to identify isomorphic structures -and this is exactly what we get from univalence. In fact we can formulate this -requirement within our formulation of categories by requiring the +and univalence gives us a way to make this notion precise. In fact we can +formulate this requirement within our formulation of categories by requiring the \emph{categories} themselves to be univalent as we shall see. \section{Context} @@ -117,7 +117,7 @@ Inspiration: * HoTT - sketch of homotopy proofs \end{verbatim} The idea of formalizing Category Theory in proof assistants is not new. There -are a multitude of these available online. Just as first reference see this +are a multitude of these available online. Just as a first reference see this question on Math Overflow: \cite{mo-formalizations}. Notably these implementations of category theory in Agda: \begin{itemize} @@ -137,17 +137,17 @@ will make it possible to prove more things and to reuse proofs. There are alternative approaches to working in a cubical setting where one can still have univalence and functional extensionality. One option is to postulate these as axioms. This approach, however, has other shortcomings, e.g.; you lose -\nomen{canonicity} (\cite{huber-2016}). Canonicity means that any well-typed -term evaluates to a \emph{canonical} form. For example for a closed term $e : -\bN$ it will be the case that $e$ reduces to $n$ applications of $\mathit{suc}$ -to $0$ for some $n$; $e = \mathit{suc}^n\ 0$. Without canonicity terms in the -language can get ``stuck'' -- meaning that they do not reduce to a canonical -form. +\nomen{canonicity} (\TODO{Pageno!} \cite{huber-2016}). Canonicity means that any +well-typed term evaluates to a \emph{canonical} form. For example for a closed +term $e : \bN$ it will be the case that $e$ reduces to $n$ applications of +$\mathit{suc}$ to $0$ for some $n$; $e = \mathit{suc}^n\ 0$. Without canonicity +terms in the language can get ``stuck'' -- meaning that they do not reduce to a +canonical form. Another approach is to use the \emph{setoid interpretation} of type theory (\cite{hofmann-1995,huber-2016}). With this approach one works with \nomen{extensionals sets} $(X, \sim)$, that is a type $X \tp \MCU$ and an -equivalence relation $\sim$. +equivalence relation $\sim \tp X \to X \to \MCU$. Types should additionally `carry around' an equivalence relation that serve as propositional equality. This approach has other drawbacks; it does not satisfy diff --git a/doc/main.tex b/doc/main.tex index 76ea1b8..9686f98 100644 --- a/doc/main.tex +++ b/doc/main.tex @@ -43,14 +43,15 @@ \researchgroup{Programming Logic Group} \bibliographystyle{plain} - +\addtocontents{toc}{\protect\thispagestyle{empty}} \begin{document} \pagenumbering{roman} \maketitle + \tableofcontents -% \pagenumbering{arabic} +% \input{introduction.tex} \input{cubical.tex} \input{implementation.tex}