|
|
|
|
@ -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.
|
|
|
|
|
|
