Half-time report
This commit is contained in:
parent
96fb1d3a3b
commit
c8c61a8d03
|
|
@ -81,7 +81,7 @@ Definition of what it means for an object to be a product in a given category.
|
|||
|
||||
Definition of what it means for a category to have all products.
|
||||
|
||||
\WIP Prove propositionality for being a product and having products.
|
||||
\WIP{} Prove propositionality for being a product and having products.
|
||||
|
||||
\subsubsection{Exponentials}
|
||||
Definition of what it means to be an exponential object.
|
||||
|
|
@ -132,25 +132,45 @@ Propositionality proofs and equality principle is provided.
|
|||
|
||||
\subsubsubsection{Voevodsky's construction}
|
||||
|
||||
Provides construction 2.3 as presented in an unpublished paper by the late
|
||||
Vladimir Voevodsky. This construction is similiar to the equivalence provided
|
||||
for the two preceding formulations
|
||||
Provides construction 2.3 as presented in an unpublished paper by Vladimir
|
||||
Voevodsky. This construction is similiar to the equivalence provided for the two
|
||||
preceding formulations
|
||||
\footnote{ TODO: I would like to include in the thesis some motivation for why
|
||||
this construction is particularly interesting.}
|
||||
|
||||
\subsubsection{Homotopy sets}
|
||||
The typical category of sets where the objects are modelled by an Agda set
|
||||
(henceforth ``type'') at a given level is not a valid category in this cubical
|
||||
settings, we need to restrict the types to be those that are homotopy sets. Thus the objects of this category are:
|
||||
(henceforth ``$\Type$'') at a given level is not a valid category in this cubical
|
||||
settings, we need to restrict the types to be those that are homotopy sets. Thus
|
||||
the objects of this category are:
|
||||
%
|
||||
$$\Set_\ell \defeq \sum_{A \tp \MCU_\ell} \isSet\ A$$
|
||||
$$\hSet_\ell \defeq \sum_{A \tp \MCU_\ell} \isSet\ A$$
|
||||
%
|
||||
\WIP{} I'm still missing a few details for the proof that this category is
|
||||
univalent. Indeed this doesn't not follow immediately from
|
||||
The definition of univalence for categories I have defined is:
|
||||
%
|
||||
$$\mathit{univalence} \tp (A \cong B) \simeq (A \simeq B)$$
|
||||
$$\isEquiv\ (\hA \equiv \hB)\ (\hA \cong \hB)\ \idToIso$$
|
||||
%
|
||||
since $A$ and $B$ are of type $\MCU \neq \Set$.
|
||||
Where $\hA and \hB$ denote objects in the category. Note that this is stronger
|
||||
than
|
||||
%
|
||||
$$(\hA \equiv \hB) \simeq (\hA \cong \hB)$$
|
||||
%
|
||||
Because we require that the equivalence is constructed from the witness to:
|
||||
%
|
||||
$$\id \comp f \equiv f \x f \comp \id \equiv f$$
|
||||
%
|
||||
And indeed univalence does not follow immediately from univalence for types:
|
||||
%
|
||||
$$(A \equiv B) \simeq (A \simeq B)$$
|
||||
%
|
||||
Because $A\ B \tp \Type$ whereas $\hA\ \hB \tp \hSet$.
|
||||
|
||||
For this reason I have shown that this category satisfies the following
|
||||
equivalent formulation of being univalent:
|
||||
%
|
||||
$$\prod_{A \tp hSet} \isContr \left( \sum_{X \tp hSet} A \cong X \right)$$
|
||||
%
|
||||
But I have not shown that it is indeed equivalent to my former definition.
|
||||
\subsubsection{Categories}
|
||||
Note that this category does in fact not exist. In stead I provide the
|
||||
definition of the ``raw'' category as well as some of the laws.
|
||||
|
|
@ -169,9 +189,71 @@ the set of presheaf categories.
|
|||
\WIP{} I have not shown that the category of functors is univalent.
|
||||
|
||||
\subsubsection{Relations}
|
||||
The category of relations. \WIP I have not shown that this category is
|
||||
The category of relations. \WIP{} I have not shown that this category is
|
||||
univalent. Not sure I intend to do so either.
|
||||
|
||||
\subsubsection{Free category}
|
||||
The free category of a category. \WIP I have not shown that this category is
|
||||
The free category of a category. \WIP{} I have not shown that this category is
|
||||
univalent.
|
||||
|
||||
\subsection{Current Challenges}
|
||||
Besides the items marked \WIP{} above I still feel a bit unsure about what to
|
||||
include in my report. Most of my work so far has been specifically about
|
||||
developing this library. Some ideas:
|
||||
%
|
||||
\begin{itemize}
|
||||
\item
|
||||
Modularity properties
|
||||
\item
|
||||
Compare with setoid-approach to solve similiar problems.
|
||||
\item
|
||||
How to structure an implementation to best deal with types that have no
|
||||
structure (propositions) and those that do (sets and everything above)
|
||||
\end{itemize}
|
||||
%
|
||||
\subsection{Ideas for future developments}
|
||||
\subsubsection{Higher categories}
|
||||
I only have a notion of (1-)categories. Perhaps it would be nice to also
|
||||
formalize higher categories.
|
||||
|
||||
\subsubsection{Hierarchy of concepts related to monads}
|
||||
In Haskell the type-class Monad sits in a hierarchy atop the notion of a functor
|
||||
and applicative functors. There's probably a similiar notion in the
|
||||
category-theoretic approach to developing this.
|
||||
|
||||
As I have already defined monads from these two perspectives, it would be
|
||||
interesting to take this idea even further and actually show how monads are
|
||||
related to applicative functors and functors. I'm not entirely sure how this
|
||||
would look in Agda though.
|
||||
|
||||
\subsubsection{Use formulation on the standard library}
|
||||
I also thought it would be interesting to use this library to show certain
|
||||
properties about functors, applicative functors and monads used in the Agda
|
||||
Standard library. So I went ahead and tried to show that agda's standard
|
||||
library's notion of a functor (along with suitable laws) is equivalent to my
|
||||
formulation (in the category of homotopic sets). I ran into two problems here,
|
||||
however; the first one is that the standard library's notion of a functor is
|
||||
indexed by the object map:
|
||||
%
|
||||
$$
|
||||
\Functor & \tp (\Type \to \Type) \to \Type
|
||||
$$
|
||||
%
|
||||
Where $\Functor\ F$ has the member:
|
||||
%
|
||||
$$
|
||||
\fmap \tp (A \to B) \to F A \to F B
|
||||
$$
|
||||
%
|
||||
Whereas the object map in my definition is existentially quantified:
|
||||
%
|
||||
$$
|
||||
\Functor & \tp \Type
|
||||
$$
|
||||
%
|
||||
And $\Functor$ has these members:
|
||||
\begin{align*}
|
||||
F & \tp \Type \to \Type \\
|
||||
\fmap & \tp (A \to B) \to F A \to F B\}
|
||||
\end{align*}
|
||||
%
|
||||
|
|
|
|||
|
|
@ -19,8 +19,17 @@
|
|||
\newcommand{\idFun}{\mathit{id}}
|
||||
\newcommand{\Sets}{\mathit{Sets}}
|
||||
\newcommand{\Set}{\mathit{Set}}
|
||||
\newcommand{\hSet}{\mathit{hSet}}
|
||||
\newcommand{\Type}{\mathcal{U}}
|
||||
\newcommand{\isEquiv}{\mathit{isEquiv}}
|
||||
\newcommand{\idToIso}{\mathit{idToIso}}
|
||||
\newcommand{\MCU}{\UU}
|
||||
\newcommand{\isSet}{\mathit{isSet}}
|
||||
\newcommand{\tp}{\;\mathord{:}\;}
|
||||
\newcommand{\isContr}{\mathit{isContr}}
|
||||
\newcommand{\id}{\mathit{id}}
|
||||
\newcommand{\tp}{\,\mathord{:}\,}
|
||||
\newcommand\hA{\mathit{hA}}
|
||||
\newcommand\hB{\mathit{hB}}
|
||||
\newcommand\Functor{\mathit{Functor}}
|
||||
\newcommand{\subsubsubsection}[1]{\textbf{#1}}
|
||||
\newcommand{\WIP}[1]{\textbf{[WIP]}}
|
||||
\newcommand{\WIP}{\textbf{WIP}}
|
||||
|
|
|
|||
|
|
@ -113,7 +113,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
|
|||
module Univalence (isIdentity : IsIdentity 𝟙) where
|
||||
-- | The identity isomorphism
|
||||
idIso : (A : Object) → A ≅ A
|
||||
idIso A = 𝟙 , (𝟙 , isIdentity)
|
||||
idIso A = 𝟙 , 𝟙 , isIdentity
|
||||
|
||||
-- | Extract an isomorphism from an equality
|
||||
--
|
||||
|
|
|
|||
Loading…
Reference in a new issue