From 4070e702d72343a8fc02c27a59744083ad61aeca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 7 May 2018 10:13:13 +0200 Subject: [PATCH] Various changes --- doc/chalmerstitle.sty | 13 +- doc/implementation.tex | 533 +++++++++++++++++++++++------------------ doc/introduction.tex | 95 ++++++-- doc/macros.tex | 1 + doc/main.tex | 4 + doc/refs.bib | 4 +- 6 files changed, 381 insertions(+), 269 deletions(-) diff --git a/doc/chalmerstitle.sty b/doc/chalmerstitle.sty index 64ddad3..70681d9 100644 --- a/doc/chalmerstitle.sty +++ b/doc/chalmerstitle.sty @@ -44,19 +44,16 @@ \fontseries{sb} %% \fontfamily{noto}\selectfont {\Huge\@title}\\[.5cm] -{\Large A formalization of category theory in Cubical Agda}\\[.5cm] -Master's thesis in Computer Science \\[.5cm] -{\Large\@author}\\[2cm] +{\Large A formalization of category theory in Cubical Agda}\\[2.5cm] \begin{center} \includegraphics[width=\linewidth,keepaspectratio]{isomorphism.png} \end{center} -\endgroup % Cover text \vfill %% \renewcommand{\familydefault}{\sfdefault} \normalfont % Set cover page font -\textsc{Department of Computer Science and Engineering}\\ -\textsc{Chalmers University of Technology}\\ -\textsc{Gothenburg, Sweden \the\year} +{\Large\@author}\\[.5cm] +Master's thesis in Computer Science +\endgroup %% \renewcommand{\familydefault}{\rmdefault} \normalfont % Reset standard font %% \end{titlepage} @@ -99,7 +96,7 @@ Master's thesis in Computer Science \\[.5cm] \thispagestyle{plain} \textit{\@title}\\ \@subtitle\\ -\copyright\ \the\year ~ \MakeUppercase{\@author} +\copyright\ \the\year ~ \textsc{\@author} \vspace{4.5cm} \setlength{\parskip}{0.5cm} diff --git a/doc/implementation.tex b/doc/implementation.tex index 9c9597c..7e18083 100644 --- a/doc/implementation.tex +++ b/doc/implementation.tex @@ -30,60 +30,111 @@ that we can provide a proof that the laws are mere propositions. As an example a category is defined to have two members: `raw` which is a collection of the data and `isCategory` which asserts some laws about that data. -This allows me to reason about things in a more mathematical way, where one can -reason about two categories by simply focusing on the data. This is acheived by -creating a function embodying the ``equality principle'' for a given type. +This allows me to reason about things in a more ``standard mathematical way'', +where one can reason about two categories by simply focusing on the data. This +is acheived by creating a function embodying the ``equality principle'' for a +given type. \section{Categories} -The data for a category consist of objects, morphisms (or arrows as I will refer -to them henceforth), the identity arrow and composition of arrows. - +The data for a category consist of a type for the sort of objects; a type for +the sort of arrows; an identity arrow and a composition operation for arrows. Another record encapsulates some laws about this data: associativity of composition, identity law for the identity morphism. These are standard -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. 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. +constituents of a category and can be found in typical mathematical expositions +on the topic. We, however, impose one further requirement on what it means to be +a category, namely that the type of arrows form a set. -Raw categories satisfying these properties are called a pre-categories. +Such categories are called \nomen{1-categories}. It's possible to relax this +requirement. This would lead to 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. Making based on higher categories would be a +very natural possible extension of this work. -As a further requirement to be a proper category we require it to be univalent. -This requirement is quite similiar to univalence for types, but we let -isomorphism on objects play the role of equivalence on types. The univalence -criterion is: +Raw categories satisfying all of the above requirements are called a +\nomen{pre}-categories. As a further requirement to be a proper category we +require it to be univalent. Before we can define this, I must introduce two more +definitions: If we let $p$ be a witness to the identity law, which formally is: % -$$ +\begin{equation} + \label{eq:identity} + \var{IsIdentity} \defeq + \prod_{A\ B \tp \Object} \prod_{f \tp A \to B} + \id \comp f \equiv f \x f \comp \id \equiv f +\end{equation} +% +Then we can construct the identity isomorphism $\var{idIso} \tp \identity, +\identity, p \tp A \approxeq A$ for any obejct $A$. Here $\approxeq$ denotes +isomorphism on objects (whereas $\cong$ denotes isomorphism of types). This will +be elaborated further on in sections \ref{sec:equiv} and \ref{sec:univalence}. +Moreover, due to substitution for paths we can construct an isomorphism from +\emph{any} path: +% +\begin{equation} +\var{idToIso} : 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: +% +\begin{align} +\label{eq:cat-univ} \isEquiv\ (A \equiv B)\ (A \approxeq B)\ \idToIso -$$ +\end{align} % -Here $\approxeq$ denotes isomorphism on objects (whereas $\cong$ denotes -isomorphism of types). - -Note that this is not the same as: +Note that \ref{eq:cat-univ} is \emph{not} the same as: % -$$ +\begin{equation} +\label{eq:cat-univalence} +\tag{Univalence, category} (A \equiv B) \simeq (A \approxeq B) -$$ +\end{equation} % -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 +However the two are logically equivalent: One can construct the latter from the +former simply by ``forgetting'' that $\idToIso$ plays the role of the equivalence. The other direction is more involved and will be discussed in section \ref{sec:univalence}. +In summary, the definition of a category is the following collection of data: +% +\begin{align} + \Object & \tp \Type \\ + \Arrow & \tp \Object \to \Object \to \Type \\ + \identity & \tp \Arrow\ A\ A \\ + \lll & \tp \Arrow\ B\ C \to \Arrow\ A\ B \to \Arrow\ A\ C +\end{align} +% +And laws: +% +\begin{align} +\tag{associativity} +h \lll (g \lll f) ≡ (h \lll g) \lll f \\ +\tag{identity} +\identity \lll f ≡ f \x +f \lll \identity ≡ f +\\ +\label{eq:arrows-are-sets} +\tag{arrows are sets} +\isSet\ (\Arrow\ A\ B)\\ +\tag{\ref{eq:cat-univ}} +\isEquiv\ (A \equiv B)\ (A \approxeq B)\ \idToIso +\end{align} +% +$\lll$ denotes arrow composition (right-to-left), and reverse function +composition (left-to-right, diagramatic order) is denoted $\rrr$. The objects +($A$, $B$ and $C$) and arrow ($f$, $g$, $h$) are implicitly universally +quantified. + With all this in place it is now possible to prove that all the laws are indeed mere propositions. Most of the proofs simply use the fact that the type of arrows are sets. This is because most of the laws are a collection of equations between arrows in the category. And since such a proof does not have any content exactly because the type of arrows form a set, two witnesses must be the same. -All the proofs are really quite mechanical. Lets have a look at one of them: The -identity law states that: +All the proofs are really quite mechanical. Lets have a look at one of them. +Proving that \ref{eq:identity} is a mere proposition: % \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 + \isProp\ \var{IsIdentity} \end{equation} % There are multiple ways to prove this. Perhaps one of the more intuitive proofs @@ -91,9 +142,9 @@ is by way of the `combinators' $\propPi$ and $\propSig$ presented in sections \ref{sec:propPi} and \ref{sec:propSig}: % \begin{align*} -\mathit{propPi} & \tp \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\prod_{a \tp A} P\ a\right) +\var{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) +\var{propSig} & \tp \isProp\ A \to \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\sum_{a \tp A} P\ a\right) \end{align*} % So the proof goes like this: We `eliminate' the 3 function abstractions by @@ -103,9 +154,10 @@ $$ \isProp \left( \id \comp f \equiv f \x f \comp \id \equiv f \right) $$ % -then we eliminate the (non-dependent) sigma-type by applying $\propSig$ giving +Then we eliminate the (non-dependent) sigma-type by applying $\propSig$ giving us the two obligations: $\isProp\ (\id \comp f \equiv f)$ and $\isProp\ (f \comp -\id \equiv f)$ which follows from the type of arrows being a set. +\id \equiv f)$ which follows from the type of arrows being a +set. This example illustrates nicely how we can use these combinators to reason about `canonical' types like $\sum$ and $\prod$. Similiar combinators can be defined @@ -119,11 +171,14 @@ available to help us here. In stead we'll have to use the path-type directly. What we want to prove is: % -$$ +\begin{equation} +\label{eq:propIsPreCategory} \isProp\ \IsPreCategory -$$ +\end{equation} % -Which is judgmentally the same as +%% \begin{proof} +% +This is judgmentally the same as % $$ \prod_{a\ b \tp \IsPreCategory} a \equiv b @@ -135,42 +190,44 @@ 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: +path between $a.\isIdentity$ and $b.\isIdentity$ is simply formed by: % $$ -\propIsIdentity\ \isIdentity_a\ \isIdentity_b \tp \isIdentity_a \equiv \isIdentity_b +\propIsIdentity\ a.\isIdentity\ b.\isIdentity +\tp +a.\isIdentity \equiv b.\isIdentity $$ % -So to give the continuous function $I \to \IsPreCategory$ that is our goal we +So to give the continuous function $I \to \IsPreCategory$, which is our goal, we introduce $i \tp I$ and proceed by constructing an element of $\IsPreCategory$ -by using that all the projections are propositions to generate paths between all -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 the triple: +by using the fact that all the projections are propositions to generate paths +between all projections. Once we have such a path e.g. $p \tp a.\isIdentity +\equiv b.\isIdentity$ we can elimiate 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 +$i$ becomes the triple: % \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 + & \var{propIsAssociative} && a.\var{isAssociative}\ + && b.\var{isAssociative} && i \\ + & \var{propIsIdentity} && a.\var{isIdentity}\ + && b.\var{isIdentity} && i \\ + & \var{propArrowsAreSets} && a.\var{arrowsAreSets}\ + && b.\var{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 -levels. It is worth noting that proving this theorem with the regular inductive -equality type would already not be possible, since we at least need -extensionality (the projections are all $\prod$-types). Assuming we had -functional extensionality available to us as an axiom, we would use functional -extensionality (in reverse?) to retreive the equalities in $a$ and $b$, -pattern-match on them to see that they are both $\mathit{refl}$ and then close -the proof with $\mathit{refl}$. Of course this theorem is not so interesting in -the setting of ITT since we know a priori that equality proofs are unique. +I've found this to be a general pattern when proving things in homotopy type +theory, namely that you have to wrap and unwrap equalities at different levels. +It is worth noting that proving this theorem with the regular inductive equality +type would already not be possible, since we at least need extensionality (the +projections are all $\prod$-types). Assuming we had functional extensionality +available to us as an axiom, we would use functional extensionality (in +reverse?) to retreive the equalities in $a$ and $b$, pattern-match on them to +see that they are both $\var{refl}$ and then close the proof with $\var{refl}$. +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. @@ -180,32 +237,35 @@ 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 \tp \isPreCategory_a \equiv \isPreCategory_b +p \tp a.\isPreCategory \equiv b.\isPreCategory $$ % and one heterogeneous: % $$ -\Path\ (\lambda\; i \mto Univalent_{p\ i})\ \isPreCategory_a\ \isPreCategory_b +\Path\ (\lambda\; i \to (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 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}. +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. So we need to +'promote' the result that univalence is a proposition to a heterogeneous path. +To this end we can use $\lemPropF$, which wasintroduced 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: +In this case $A = \var{IsIdentity}\ \identity$ and $B = \var{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 +congruence of paths: % $$ -\congruence\ \mathit{isIdentity}\ p +\congruence\ \var{isIdentity}\ p $$ % +And this finishes the proof that being-a-category is a mere proposition +(\ref{eq:propIsPreCategory}). + When we have a proper category we can make precise the notion of ``identifying isomorphic types'' \TODO{cite awodey here}. That is, we can construct the function: @@ -231,25 +291,38 @@ details. \TODO{The proof is a bit fun, should I include it?} \label{sec:equiv} The usual notion of a function $f \tp A \to B$ having an inverses is: % -$$ +\begin{equation} +\label{eq:isomorphism} \sum_{g \tp B \to A} f \comp g \equiv \identity_{B} \x g \comp f \equiv \identity_{A} -$$ +\end{equation} % -This is defined in \cite[p. 129]{hott-2013} and is referred to as the a -quasi-inverse. At the same place \cite{hott-2013} gives an ``interface'' for -what an equivalence $\isEquiv \tp (A \to B) \to \MCU$ must supply: +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: % -\begin{itemize} -\item - $\qinv\ f \to \isEquiv\ f$ -\item - $\isEquiv\ f \to \qinv\ f$ -\item - $\isEquiv\ f$ is a proposition -\end{itemize} +\begin{equation} +A \cong B \defeq \sum_{f \tp A \to B} \Isomorphism\ f +\end{equation} % -Having such an interface gives us both 1) a way to think rather abstractly about -how to work with equivalences and 2) to use ad-hoc definitions of equivalences. +At the same place \cite{hott-2013} gives an ``interface'' for what the judgment +$\isEquiv \tp (A \to B) \to \MCU$ must provide: +% +\begin{align} +\var{fromIso} & \tp \Isomorphism\ f \to \isEquiv\ f \\ +\var{toIso} & \tp \isEquiv\ f \to \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 \to A \simeq B \\ +\var{toIsomorphism} & \tp A \simeq B \to 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: % $$ @@ -264,40 +337,26 @@ I give it's definition here mainly for completeness, because as I stated we can move away from this specific instantiation and think about it more abstractly once we have shown that this definition actually works as an equivalence. -The first function from the list of requirements we will call -$\mathit{fromIsomorphism}$, this is known as $\mathit{gradLemma}$ in -\cite{cubical-agda} the second one we will refer to as $\mathit{toIsmorphism}$. It's -implementation can be found in the sources. Likewise the proof that this -equivalence is propositional can be found in my implementation. +$\var{fromIso}$ can be found in \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. 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 \simeq B \defeq \sum_{f \tp A \to B} \isEquiv\ f -$$ +\end{equation} % Note that the term equivalence here is overloaded referring both to the map $f -\tp A \to B$ and the type $A \simeq B$. I will use these conflated terms when it +\tp A \to B$ and the type $A \simeq 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 \to B$ that witness this. I will use these conflated terms when it is clear from the context what is being referred to. -Just like we could promote a quasi-inverse to an equivalence we can promote an -isomorphism to an equivalence: -% -$$ -\mathit{fromIsomorphism} \tp A \cong B \to A \simeq B -$$ -% -and vice-versa: -% -$$ -\mathit{toIsomorphism} \tp A \simeq B \to A \cong 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 \to B$ that witness this. - -Both $\cong$ and $\simeq$ form equivalence relations. +Both $\cong$ and $\simeq$ form equivalence relations (no pun intended). \section{Univalence} \label{sec:univalence} @@ -305,7 +364,7 @@ As noted in the introduction the univalence for types $A\; B \tp \Type$ states that: % $$ -\mathit{Univalence} \defeq (A \equiv B) \simeq (A \simeq B) +\var{Univalence} \defeq (A \equiv B) \simeq (A \simeq B) $$ % As mentioned the univalence criterion for some category $\bC$ says that for all @@ -332,9 +391,8 @@ 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 -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. +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. I will now mention a few helpful thoerems that follow from univalence that will become useful later. @@ -352,66 +410,72 @@ $$ % The next few theorems are variations on theorem 9.1.9 from \cite{hott-2013}. Let 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$. +isomorphism $\iota \tp A \to B$ and its inverse $\inv{\iota} \tp B \to A$. Since $\bC$ is a category (and therefore univalent) the isomorphism induces a path $p \tp A \equiv B$. From this equality we can get two further paths: -$p_{\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 +$p_{\var{dom}} \tp \var{Arrow}\ A\ X \equiv \var{Arrow}\ B\ X$ and +$p_{\var{cod}} \tp \var{Arrow}\ X\ A \equiv \var{Arrow}\ X\ B$. We then have the following two theorems: % -$$ -\mathit{coeDom} \tp \prod_{f \tp A \to X} \mathit{coe}\ p_{\mathit{dom}}\ f \equiv f \lll \widetilde{\iota} -$$ -% -% \begin{align} +\label{eq:coeDom} +\var{coeDom} & \tp \prod_{f \tp A \to X} +\var{coe}\ p_{\var{dom}}\ f \equiv f \lll \inv{\iota} +\\ \label{eq:coeCod} -\mathit{coeCod} \tp \prod_{f \tp A \to X} \mathit{coe}\ p_{\mathit{cod}}\ f \equiv \iota \lll f +\var{coeCod} & \tp \prod_{f \tp A \to X} +\var{coe}\ p_{\var{cod}}\ f \equiv \iota \lll f \end{align} % I will give the proof of the first theorem here, the second one is analagous. +% \begin{align*} -\mathit{coe}\ p_{\mathit{dom}}\ f - & \equiv f \lll \mathit{obverse}_{\mathit{idToIso}\ p} && \text{lemma} \\ - & \equiv f \lll \widetilde{\iota} - && \text{$\mathit{idToIso}$ and $\mathit{isoToId}$ are inverses}\\ +\var{coe}\ p_{\var{dom}}\ f + & \equiv f \lll \inv{(\var{idToIso}\ p)} && \text{lemma} \\ + & \equiv f \lll \inv{\iota} + && \text{$\var{idToIso}$ and $\var{isoToId}$ are inverses}\\ \end{align*} % In the second step we use the fact that $p$ is constructed from the isomorphism -$\iota$ -- $\mathit{obverse}$ denotes the map $B \to A$ induced by the -isomorphism $\mathit{idToIso}\ p \tp A \cong B$. The helper-lemma is similar to +$\iota$ -- $\inv{(\var{idToIso}\ p)}$ denotes the map $B \to A$ induced by the +isomorphism $\var{idToIso}\ p \tp A \cong B$. The helper-lemma is similar to what we're trying to prove but talks about paths rather than isomorphisms: % -$$ -\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} -$$ +\begin{equation} +\label{eq:coeDomIso} +\prod_{f \tp \var{Arrow}\ A\ B} \prod_{p \tp A \equiv B} +\var{coe}\ p_\var{dom}\ f \equiv f \lll \inv{(\var{idToIso}\ p)}} +\end{equation} % -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$ +Again $p_\var{dom}$ denotes the path $\var{Arrow}\ A\ X \equiv +\var{Arrow}\ B\ X$ induced by $p$. To prove this statement I let $f$ and $p$ be given and then invoke based-path-induction. The induction will be based at $A -\tp \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 +\tp \var{Object}$, so let $\widetilde{B} \tp \Object$ and $\widetilde{p} \tp +A \equiv \widetilde{B}$ be given. The family that we perform induction over will be: % $$ -\mathit{coe}\ {\widetilde{p}}^*\ f \equiv f \lll \mathit{obverse}_{\mathit{idToIso}\ \widetilde{p}} +\var{coe}\ {\widetilde{p}}^*\ f +\equiv +f \lll \inv{(\var{idToIso}\ \widetilde{p})} $$ The base-case therefore becomes: \begin{align*} -\mathit{coe}\ {\widetilde{\refl}}^*\ f +\var{coe}\ {\widetilde{\refl}}^*\ f & \equiv f \\ -& \equiv f \lll \mathit{identity} \\ -& \equiv f \lll \mathit{obverse}_{\mathit{idToIso}\ \widetilde{\refl}} +& \equiv f \lll \var{identity} \\ +& \equiv f \lll \inv{(\var{idToIso}\ \widetilde{\refl})} \end{align*} % The first step follows because reflixivity is a neutral element for coercions. The second step is the identity law in the category. The last step has to do -with the fact that $\mathit{idToIso}$ is constructed by substituting according -to the supplied path and since reflexivity is also the neutral element for +with the fact that $\var{idToIso}$ is constructed by substituting according to +the supplied path and since reflexivity is also the neutral element for substuitutions we arrive at the desired expression. To close the -based-path-induction we must supply the value at the other end and the -connecting path, but in this case this is simply $A' \tp \Object$ and $p \tp A -\equiv A'$ which we have. +based-path-induction we must supply the value ``at the other''. In this case +this is simply $B \tp \Object$ and $p \tp A \equiv B$ which we have. + +And this finishes the proof of \ref{eq:coeDomIso} and thus \ref{eq:coeDom}. % \section{Categories} \subsection{Opposite category} @@ -423,14 +487,18 @@ 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^{\mathit{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 composition will be reverse function composition from the underlying category. -Showing that this forms a pre-category is rather straightforward. I'll state the -laws in terms of the underlying category $\bC$: +I'll refer to things in terms of the underlying category, unless they have an +over-bar. So e.g. $\idToIso$ is a function in the underlying category and the +corresponding thing is denoted $\wideoverbar{\idToIso}$ in the opposite +category. + +Showing that this forms a pre-category is rather straightforward. % $$ h \rrr (g \rrr f) \equiv h \rrr g \rrr f @@ -440,78 +508,77 @@ Since $\rrr$ is reverse function composition this is just the symmetric version of associativity. % $$ -\mathit{identity} \rrr f \equiv f \x f \rrr identity \equiv f +\var{identity} \rrr f \equiv f \x f \rrr identity \equiv f $$ % 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 $\Hom_{A\ B}$ is a set for all $A\ B \tp -\Object$ then so is $\Hom_{B\ A}$. +arguments. Or in other words; since $\Arrow\ A\ B$ is a set for all $A\;B \tp +\Object$ then so is $Arrow\ B\ A$. -Now, to show that this category is univalent is not as straight-forward. Lucliy -section \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 -$\idToIso_{\mathit{Op}} \tp (A \equiv B) \to (A \approxeq_{\mathit{Op}} B)$. +Now, to show that this category is univalent is not as straight-forward. Luckily +section \ref{sec:equiv} gave us some tools to work with equivalences. We saw +that we can prove this category univalent by giving an inverse to +$\wideoverbar{\idToIso} \tp (A \equiv B) \to (A \wideoverbar{\approxeq} B)$. From the original category we have that $\idToIso \tp (A \equiv B) \to (A \cong -B)$ is an isomorphism. Let us denote it's inverse with $\eta \tp (A \approxeq B) -\to (A \equiv B)$. If we squint we can see what we need is a way to go between -$\approxeq_{\mathit{Op}}$ and $\approxeq$, well, an inhabitant of $A \approxeq -B$ is simply an arrow $f \tp \mathit{Arrow}\ A\ B$ and it's inverse $g \tp -\mathit{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 $\mathit{shuffle} \tp (A \approxeq B) \to (A -\approxeq_{\bC} B)$ and $\mathit{shuffle}^{-1} \tp (A \approxeq_{\bC} B) \to (A -\approxeq B)$ respectively. +B)$ is an isomorphism. Let us denote it's inverse with $\isoToId \tp (A +\approxeq B) \to (A \equiv B)$. If we squint we can see what we need is a way to +go between $\wideoverbar{\approxeq}$ and $\approxeq$. -As the inverse of $\idToIso_{\mathit{Op}}$ I will pick $\zeta \defeq \eta \comp -\var{shuffle}$. The proof that they are inverses go as follows: +An inhabitant of $A \approxeq B$ is simply an arrow $f \tp \var{Arrow}\ A\ B$ +and it's inverse $g \tp \var{Arrow}\ B\ A$. In the opposite category $g$ will +play the role of the isomorphism and $f$ will be the inverse. Similarly we can +go in the opposite direction. I name these maps $\var{shuffle} \tp (A \approxeq +B) \to (A \wideoverbar{\approxeq} B)$ and $\var{shuffle}^{-1} \tp (A +\wideoverbar{\approxeq} B) \to (A \approxeq B)$ respectively. + +As the inverse of $\wideoverbar{\idToIso}$ I will pick $\wideoverbar{\isoToId} +\defeq \isoToId \comp \var{shuffle}$. The proof that they are inverses go as +follows: % \begin{align*} -\zeta \comp \idToIso & \equiv -\eta \comp \var{shuffle} \comp \idToIso -&& \text{by definition} \\ +\wideoverbar{\isoToId} \comp \wideoverbar{\idToIso} & = +\isoToId \comp \var{shuffle} \comp \wideoverbar{\idToIso} +\\ %% ≡⟨ cong (λ φ → φ x) (cong (λ φ → η ⊙ shuffle ⊙ φ) (funExt lem)) ⟩ \\ % & \equiv -\eta \comp \var{shuffle} \comp \inv{\var{shuffle}} \comp \idToIso +\isoToId \comp \var{shuffle} \comp \inv{\var{shuffle}} \comp \idToIso && \text{lemma} \\ %% ≡⟨⟩ \\ & \equiv -\eta \comp \idToIso_{\bC} +\isoToId \comp \idToIso && \text{$\var{shuffle}$ is an isomorphism} \\ -%% ≡⟨ (λ i → verso-recto i x) ⟩ \\ & \equiv \identity -&& \text{$\eta$ is an ismorphism} +&& \text{$\isoToId$ is an ismorphism} \end{align*} % The other direction is analogous. -The lemma used in this proof states that $\idToIso \equiv \inv{\var{shuffle}} \comp -\idToIso_{\bC}$ it's a rather straight-forward proof since being-an-inverse-of -is a proposition. - -So, in conclusion, we've shown that the opposite category is indeed a category. +The lemma used in step 2 of this proof states that $\wideoverbar{idToIso} \equiv +\inv{\var{shuffle}} \comp \idToIso$. This is a rather straight-forward proof +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: % $$ -\prod_{\bC \tp \mathit{Category}} \left(\bC^{\mathit{Op}}\right)^{\mathit{Op}} \equiv \bC +\prod_{\bC \tp \var{Category}} \left(\bC^{\var{Op}}\right)^{\var{Op}} \equiv \bC $$ % -As we've seen the laws in $\left(\bC^{\mathit{Op}}\right)^{\mathit{Op}}$ get -quite involved.\footnote{We haven't even seen the full story because we've used - this `interface' for equivalences.} Luckily since being-a-category is a mere +As we've seen the laws in $\left(\bC^{\var{Op}}\right)^{\var{Op}}$ get quite +involved.\footnote{We haven't even seen the full story because we've used this + `interface' for equivalences.} Luckily since being-a-category is a mere proposition, we need not concern ourselves with this bit when proving the above. -We can use the equality principle for categories that lets us prove an equality +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: % $$ -\mathit{raw}\ \left(\bC^{\mathit{Op}}\right)^{\mathit{Op}} \equiv \mathit{raw}\ \bC +\var{raw}\ \left(\bC^{\var{Op}}\right)^{\var{Op}} \equiv \var{raw}\ \bC $$ % And these are judgmentally the same. I remind the reader that the left-hand side @@ -521,23 +588,23 @@ is constructed by flipping the arrows, which judgmentally is an involution. 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: % -$$\Set_\ell \defeq \sum_{A \tp \MCU_\ell} \isSet\ A$$ +$$\Set \defeq \sum_{A \tp \MCU} \isSet\ A$$ % The more straight-forward notion of a category where the objects are types is -not a valid (1-)category. Since 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 types can have higher homotopic structure. Univalence does not follow immediately from univalence for types: % $$(A \equiv B) \simeq (A \simeq B)$$ % Because here $A\ B \tp \Type$ whereas the objects in this category have the type -$\Set$ so we cannot form the type $\mathit{hA} \simeq \mathit{hB}$ for objects -$\mathit{hA}\;\mathit{hB} \tp \Set$. In stead I show that this category +$\Set$ so we cannot form the type $\var{hA} \simeq \var{hB}$ for objects +$\var{hA}\;\var{hB} \tp \Set$. In stead I show that this category satisfies: % $$ -(\mathit{hA} \equiv \mathit{hB}) \simeq (\mathit{hA} \approxeq \mathit{hB}) +(\var{hA} \equiv \var{hB}) \simeq (\var{hA} \approxeq \var{hB}) $$ % Which, as we saw in section \ref{sec:univalence}, is sufficient to show that the @@ -561,7 +628,7 @@ together. Step one will be proven with the following lemma: \end{align} % The lemma states that for pairs whose second component are mere propositions -equiality is equivalent to equality of the first components. In this case the +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: @@ -574,29 +641,31 @@ lemma: Which says that if two type-families are equivalent at all points, then pairs with identitical first components and these families as second components will also be equivalent. For our purposes $P \defeq \isEquiv\ A\ B$ and $Q \defeq -\mathit{Isomorphism}$. So we must finally prove: +\var{Isomorphism}$. So we must finally prove: % \begin{align} \label{eq:equivIso} -\prod_{f \tp A \to B} \left( \isEquiv\ A\ B\ f \simeq \mathit{Isomorphism}\ f \right) +\prod_{f \tp A \to B} \left( \isEquiv\ A\ B\ f \simeq \var{Isomorphism}\ f \right) \end{align} First, lets proove \ref{eq:equivPropSig}: Let $propP \tp \prod_{a \tp A} \isProp (P\ a)$ and $x\;y \tp \sum_{a \tp A} P\ a$ be given. Because -of $\mathit{fromIsomorphism}$ it suffices to give an isomorphism between +of $\var{fromIsomorphism}$ it suffices to give an isomorphism between $x \equiv y$ and $\fst\ x \equiv \fst\ y$: % -\begin{align*} - f & \defeq \congruence\ \fst \tp x \equiv y \to \fst\ x \equiv \fst\ y \\ - g & \defeq \mathit{lemSig}\ \mathit{propP}\ x\ y \tp \fst\ x \equiv \fst\ y \to x \equiv y -\end{align*} +\begin{alignat*}{5} + f & \defeq \congruence\ \fst + && \tp x && \equiv y && \to \fst\ x && \equiv \fst\ y \\ + g & \defeq \var{lemSig}\ \var{propP}\ x\ y + && \tp \fst\ x && \equiv \fst\ y && \to x && \equiv y +\end{alignat*} % -\TODO{Is it confusing that I use point-free style here?} -Here $\mathit{lemSig}$ is a lemma that says that if the second component of a -pair is a proposition, it suffices to give a path between it's first components -to construct an equality of the two pairs: +\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: % \begin{align*} -\mathit{lemSig} \tp \left( \prod_{x \tp A} \isProp\ (B\ x) \right) \to +\var{lemSig} \tp \left( \prod_{x \tp A} \isProp\ (B\ x) \right) \to \prod_{u\; v \tp \sum_{a \tp A} B\ a} \left( \fst\ u \equiv \fst\ v \right) \to u \equiv v \end{align*} @@ -615,31 +684,31 @@ Lastly we prove \ref{eq:equivIso}. Let $f \tp A \to B$ be given. For the maps we choose: % \begin{align*} -\mathit{toIso} - & \tp \isEquiv\ f \to \mathit{Isomorphism}\ f \\ -\mathit{fromIso} - & \tp \mathit{Isomorphism}\ f \to \isEquiv\ f +\var{toIso} + & \tp \isEquiv\ f \to \var{Isomorphism}\ f \\ +\var{fromIso} + & \tp \var{Isomorphism}\ f \to \isEquiv\ f \end{align*} % As mentioned in section \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*} - \mathit{fromIso} \comp \mathit{toIso} \equiv \identity_{\isEquiv\ f} + \var{fromIso} \comp \var{toIso} \equiv \identity_{\isEquiv\ f} \end{align*} % For this we can use the fact that being-an-equivalence is a mere proposition. For the other direction: % \begin{align*} - \mathit{toIso} \comp \mathit{fromIso} \equiv \identity_{\mathit{Isomorphism}\ f} + \var{toIso} \comp \var{fromIso} \equiv \identity_{\var{Isomorphism}\ f} \end{align*} % -We will show that $\mathit{Isomorphism}\ f$ is also a mere proposition. To this -end, let $X\;Y \tp \mathit{Isomorphism}\ f$ be given. Name the maps $x\;y \tp B +We will show that $\var{Isomorphism}\ f$ is also a mere proposition. To this +end, let $X\;Y \tp \var{Isomorphism}\ f$ be given. Name the maps $x\;y \tp B \to A$ respectively. Now, the proof that $X$ and $Y$ are the same is a pair of -paths: $p \tp x \equiv y$ and $\Path\ (\lambda\; i \mto -\mathit{AreInverses}\ f\ (p\ i))\ \mathcal{X}\ \mathcal{Y}$ where $\mathcal{X}$ +paths: $p \tp x \equiv y$ and $\Path\ (\lambda\; i \to +\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$. $p$ is inhabited by: % @@ -659,10 +728,10 @@ proposition and then use $\lemPropF$. So we prove the generalization: % \begin{align} \label{eq:propAreInversesGen} -\prod_{g \tp B \to A} \isProp\ (\mathit{AreInverses}\ f\ g) +\prod_{g \tp B \to A} \isProp\ (\var{AreInverses}\ f\ g) \end{align} % -But $\mathit{AreInverses}\ f\ g$ is a pair of equations on arrows, so we use +But $\var{AreInverses}\ f\ g$ is a pair of equations on arrows, so we use $\propSig$ and the fact that both $A$ and $B$ are sets to close this proof. \subsection{Category of categories} @@ -676,26 +745,26 @@ 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 is useful if this library is later extended to talk about higher categories. -\section{Product} +\section{Products} In the following I'll demonstrate a technique for using categories to prove properties. The goal in this section is to show that products are propositions: % $$ -\prod_{\bC \tp \Category} \prod_{A\;B \tp \Object} \isProp\ (\mathit{Product}\ \bC\ A\ B) +\prod_{\bC \tp \Category} \prod_{A\;B \tp \Object} \isProp\ (\var{Product}\ \bC\ A\ B) $$ % -Where $\mathit{Product}\ \bC\ A\ B$ denotes the type of products of objects $A$ +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, let's recall the definition of products. -\subsection{Products} +\subsection{Definition of products} Given a category $\bC$ and two objects $A$ and $B$ in $\bC$ we define the -product of $A$ and $B$ to be an object $A \x B$ in $\bC$ and two arrows $\pi_1 -\tp A \x B \to A$ and $\pi_2 \tp A \x B \to B$ called the projections of the -product. The projections must satisfy the following property: +product (object) of $A$ and $B$ to be an object $A \x B$ in $\bC$ and two arrows +$\pi_1 \tp A \x B \to A$ and $\pi_2 \tp A \x B \to B$ 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 @@ -1017,7 +1086,7 @@ 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{$\mathit{coeDom}$ and the isomorphism $f, \inv{f}$} \\ + & ≡ x_\mathcal{A} \lll \fst\ \inv{f} && \text{$\var{coeDom}$ and the isomorphism $f, \inv{f}$} \\ & ≡ y_\mathcal{A} && \text{\ref{eq:pairArrowLaw} for $\inv{f}$} \end{align*} % @@ -1214,7 +1283,5 @@ And likewise in the kleisli formulation we can define $\join$: \join \defeq \bind\ \identity \end{align} % -Which shall play the role of $\join$. - It now remains to show that we can prove the various laws given this choice. I refer the reader to my implementation for the details. diff --git a/doc/introduction.tex b/doc/introduction.tex index 6d4d98a..2695db8 100644 --- a/doc/introduction.tex +++ b/doc/introduction.tex @@ -24,7 +24,7 @@ $f \defeq (n : \bN) \mapsto (0 + n : \bN)$ $g \defeq (n : \bN) \mapsto (n + 0 : \bN)$ \end{multicols} % -$n + 0$ is \nomen{definitionally} equal to $n$ which we write as $n + 0 = n$. +$n + 0$ is \nomen{definitionally} equal to $n$, which we write as $n + 0 = n$. This is also called \nomen{judgmental} equality. We call it definitional equality because the \emph{equality} arises from the \emph{definition} of $+$ which is: @@ -39,7 +39,7 @@ which is: Note that $0 + n$ is \emph{not} definitionally equal to $n$. $0 + n$ is in normal form. I.e.; there is no rule for $+$ whose left-hand-side matches this expression. We \emph{do}, however, have that they are \nomen{propositionally} -equal which we write as $n + 0 \equiv n$. Propositional equality means that +equal, which we write as $n + 0 \equiv n$. Propositional equality means that there is a proof that exhibits this relation. Since equality is a transitive relation we have that $n + 0 \equiv 0 + n$. @@ -62,7 +62,7 @@ for a category $\bC$ and a fixed object in $A \in \bC$ is defined to be: \end{align*} % The proof obligation that this satisfies the identity law of functors -($\fmap\ \idFun \equiv \idFun$) becomes: +($\fmap\ \idFun \equiv \idFun$) thus becomes: % \begin{align*} \Hom(A, \idFun_{\bX}) = (g \mapsto \idFun \comp g) \equiv \idFun_{\Sets} @@ -86,7 +86,7 @@ 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 +More specifically what we are interested in is a way of identifying \nomen{equivalent} types. I will return to the definition of equivalence later in section \ref{sec:equiv}, but for now it is sufficient to think of an equivalence as a one-to-one correspondence. We write $A \simeq B$ to assert that @@ -102,7 +102,7 @@ In particular this allows us to construct an equality from an equivalence 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 +(abstract) algebras of functions'' (\cite{awodey-2006}). By that token functional extensionality is particularly useful for formulating Category Theory. In Category theory it is also common to identify isomorphic structures and univalence gives us a way to make this notion precise. In fact we can @@ -111,28 +111,38 @@ formulate this requirement within our formulation of categories by requiring the \section{Context} % -\begin{verbatim} -Inspiration: -* Awodey - formulation of categories -* 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 a first reference see this question on Math Overflow: \cite{mo-formalizations}. Notably these implementations of category theory in Agda: +% \begin{itemize} \item -\url{https://github.com/copumpkin/categories} -- setoid interpretation -\item -\url{https://github.com/pcapriotti/agda-categories} -- homotopic setting with postulates -\item -\url{https://github.com/pcapriotti/agda-categories} -- homotopic setting in coq -\item -\url{https://github.com/mortberg/cubicaltt} -- homotopic setting in \texttt{cubicaltt} -\end{itemize} + \url{https://github.com/copumpkin/categories} + A formalization in Agda using the setoid approach +\item + \url{https://github.com/pcapriotti/agda-categories} + + A formalization in Agda with univalence and functional extensionality as + postulates. +\item + \url{https://github.com/pcapriotti/agda-categories} + + A formalization in Coq in the homotopic setting +\item + \url{https://github.com/mortberg/cubicaltt} + + A formalization in CubicalTT - a language designed for cubical-type-theory. + Formalizes many different things, but only a few concepts from category + theory. + +\end{itemize} +% The contribution of this thesis is to explore how working in a cubical setting -will make it possible to prove more things and to reuse proofs. +will make it possible to prove more things and to reuse proofs and to try and +compare some aspects of this formalization with the existing ones.\TODO{How can + I live up to this?} There are alternative approaches to working in a cubical setting where one can still have univalence and functional extensionality. One option is to postulate @@ -147,11 +157,44 @@ 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 \tp X \to X \to \MCU$. - -Types should additionally `carry around' an equivalence relation that serve as +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. This approach has other drawbacks; it does not satisfy -all judgemental equalites of type theory, is cumbersome to work with in practice -(\cite[p. 4]{huber-2016}) and makes equational proofs less reusable since -equational proofs $a \sim_{X} b$ are inherently `local' to the extensional set -$(X , \sim)$. +all propositional equalites of type theory (\TODO{Citation needed}, is +cumbersome to work with in practice (\cite[p. 4]{huber-2016}) and makes +equational proofs less reusable since equational proofs $a \sim_{X} b$ are +inherently `local' to the extensional set $(X , \sim)$. + +\section{Conventions} +\TODO{Talk a bit about terminology. Find a good place to stuff this little + section.} + +In the remainder of this paper I will use the term \nomen{Type} to describe -- +well, types. Thereby diverging from the notation in Agda where the keyword +\texttt{Set} refers to types. \nomen{Set} on the other hand shall refer to the +homotopical notion of a set. I will also leave all universe levels implicit. + +And I use the term \nomen{arrow} to refer to morphisms in a category, whereas +the terms morphism, map or function shall be reserved for talking about +type-theoretic functions; i.e. functions in Agda. + +$\defeq$ will be used for introducing definitions. $=$ will be used to for +judgmental equality and $\equiv$ will be used for propositional equality. + +All this is summarized in the following table: + +\begin{center} +\begin{tabular}{ c c c } +Name & Agda & Notation \\ +\hline +\nomen{Type} & \texttt{Set} & $\Type$ \\ +\nomen{Set} & \texttt{Σ Set IsSet} & $\Set$ \\ +Function, morphism, map & \texttt{A → B} & $A → B$ \\ +Dependent- ditto & \texttt{(a : A) → B} & $∏_{a \tp A} → B$ \\ +\nomen{Arrow} & \texttt{Arrow A B} & $\Arrow\ A\ B$ \\ +\nomen{Object} & \texttt{C.Object} & $̱ℂ.Object$ +Definition & \texttt{=} & $̱\defeq$ +Judgmental equality & \null & $̱=$ +Propositional equality & \null & $̱\equiv$ +\end{tabular} +\end{center} diff --git a/doc/macros.tex b/doc/macros.tex index 0ce9273..a5e03db 100644 --- a/doc/macros.tex +++ b/doc/macros.tex @@ -71,6 +71,7 @@ \newcommand\Univalent{\var{Univalent}} \newcommand\refl{\var{refl}} \newcommand\isoToId{\var{isoToId}} +\newcommand\Isomorphism{\var{Isomorphism}} \newcommand\rrr{\ggg} \newcommand\fish{\mathrel{\wideoverbar{\rrr}}} \newcommand\fst{\var{fst}} diff --git a/doc/main.tex b/doc/main.tex index 9686f98..a894748 100644 --- a/doc/main.tex +++ b/doc/main.tex @@ -44,6 +44,10 @@ \bibliographystyle{plain} \addtocontents{toc}{\protect\thispagestyle{empty}} +%% \newtheorem{prop}{Proposition} +\makeatletter +\newcommand*{\rom}[1]{\expandafter\@slowroman\romannumeral #1@} +\makeatother \begin{document} \pagenumbering{roman} diff --git a/doc/refs.bib b/doc/refs.bib index 2e376a0..4f335ac 100644 --- a/doc/refs.bib +++ b/doc/refs.bib @@ -106,11 +106,11 @@ @MISC{mo-formalizations, TITLE = {Formalizations of category theory in proof assistants}, AUTHOR = {Jason Gross}, - HOWPUBLISHED = {MathOverflow}, NOTE = {Version: 2014-01-19}, year={2014}, EPRINT = {\url{https://mathoverflow.net/q/152497}}, - URL = {https://mathoverflow.net/q/152497} + url = {https://mathoverflow.net/q/152497}, + howpublished = {MathOverflow: \url{https://mathoverflow.net/q/152497}} } @Misc{UniMath, author = {Voevodsky, Vladimir and Ahrens, Benedikt and Grayson, Daniel and others},