178 lines
6.7 KiB
TeX
178 lines
6.7 KiB
TeX
\section{Halftime report}
|
|
I've written this as an appendix because 1) the aim of the thesis changed
|
|
drastically from the planning report/proposal 2) partly I'm not sure how to
|
|
structure my thesis.
|
|
|
|
My work so far has very much focused on the formalization, i.e. coding. It's
|
|
unclear to me at this point what I should have in the final report. Here I will
|
|
describe what I have managed to formalize so far and what outstanding challenges
|
|
I'm facing.
|
|
|
|
\subsection{Implementation overview}
|
|
The overall structure of my project is as follows:
|
|
|
|
\begin{itemize}
|
|
\item Core categorical concepts
|
|
\subitem Categories
|
|
\subitem Functors
|
|
\subitem Products
|
|
\subitem Exponentials
|
|
\subitem Cartesian closed categories
|
|
\subitem Natural transformations
|
|
\subitem Yoneda embedding
|
|
\subitem Monads
|
|
\subsubitem Monoidal monads
|
|
\subsubitem Kleisli monads
|
|
\subsubitem Voevodsky's construction
|
|
\item Category of \ldots
|
|
\subitem Homotopy sets
|
|
\subitem Categories
|
|
\subitem Relations
|
|
\subitem Functors
|
|
\subitem Free category
|
|
\end{itemize}
|
|
|
|
I also started work on the category with families as well as the cubical
|
|
category as per the original goal of the thesis. However I have not gotten so
|
|
far with this.
|
|
|
|
In the following I will give an overview of overall results in each of these
|
|
categories (no pun).
|
|
|
|
As an overall design-guideline I've defined concepts in a such a way that the
|
|
``data'' and the ``laws'' about that data is split up in seperate modules. 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 record. In
|
|
the case of monads, to prove two categories propositionally equal it enough to
|
|
provide a proof that their data is equal.
|
|
|
|
\subsubsection{Categories}
|
|
Defines the basic notion of a category. This definition closely follows that of
|
|
[HoTT]: That is, the standard definition of a category (data; objects, arrows,
|
|
composition and identity, laws; preservation of identity and composition) plus
|
|
the extra condition that it is univalent - namely that you can get an equality
|
|
of two objects from an isomorphism.
|
|
|
|
I make no distinction between a pre-category and a real category (as in the
|
|
[HoTT]-sense). A pre-category in my implementation would be a category sans the
|
|
witness to univalence.
|
|
|
|
I also prove that being a category is a proposition. This gives rise to an
|
|
equality principle for monads that focuses on the data-part.
|
|
|
|
I also show that the opposite category is indeed a category. (\WIP{} I have not
|
|
shown that univalence holds for such a construction)
|
|
|
|
I also show that taking the opposite is an involution.
|
|
|
|
\subsubsection{Functors}
|
|
Defines the notion of a functor - also split up into data and laws.
|
|
|
|
Propositionality for being a functor.
|
|
|
|
Composition of functors and the identity functor.
|
|
|
|
\subsubsection{Products}
|
|
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.
|
|
|
|
\subsubsection{Exponentials}
|
|
Definition of what it means to be an exponential object.
|
|
|
|
Definition of what it means for a category to have all exponential objects.
|
|
|
|
\subsubsection{Cartesian closed categories}
|
|
Definition of what it means for a category to be cartesian closed; namely that
|
|
it has all products and all exponentials.
|
|
|
|
\subsubsection{Natural transformations}
|
|
Definition of transformations\footnote{Maybe this is a name I made up for a
|
|
family of morphisms} and the naturality condition for these.
|
|
|
|
Proof that naturality is a mere proposition and the accompanying equality
|
|
principle. Proof that natural transformations are homotopic sets.
|
|
|
|
The identity natural transformation.
|
|
|
|
\subsubsection{Yoneda embedding}
|
|
|
|
The yoneda embedding is typically presented in terms of the category of
|
|
categories (cf. Awodey) \emph however this is not stricly needed - all we need
|
|
is what would be the exponential object in that category - this happens to be
|
|
functors and so this is how we define the yoneda embedding.
|
|
|
|
\subsubsection{Monads}
|
|
|
|
Defines an equivalence between these two formulations of a monad:
|
|
|
|
\subsubsubsection{Monoidal monads}
|
|
|
|
Defines the standard monoidal representation of a monad:
|
|
|
|
An endofunctor with two natural transformations (called ``pure'' and ``join'')
|
|
and some laws about these natural transformations.
|
|
|
|
Propositionality proofs and equality principle is provided.
|
|
|
|
\subsubsubsection{Kleisli monads}
|
|
|
|
A presentation of monads perhaps more familiar to a functional programer:
|
|
|
|
A map on objects and two maps on morphisms (called ``pure'' and ``bind'') and
|
|
some laws about these maps.
|
|
|
|
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
|
|
\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:
|
|
%
|
|
$$\Set_\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
|
|
%
|
|
$$\mathit{univalence} \tp (A \cong B) \simeq (A \simeq B)$$
|
|
%
|
|
since $A$ and $B$ are of type $\MCU \neq \Set$.
|
|
\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.
|
|
|
|
Furthermore I provide some helpful lemmas about this raw category. For instance
|
|
I have shown what would be the exponential object in such a category.
|
|
|
|
These lemmas can be used to provide the actual exponential object in a context
|
|
where we have a witness to this being a category. This is useful if this library
|
|
is later extended to talk about higher categories.
|
|
|
|
\subsubsection{Functors}
|
|
The category of functors and natural transformations. An immediate corrolary is
|
|
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
|
|
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
|
|
univalent.
|