From 71d9acff9a96fb65c5205e3ea7c7d19139da3b56 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 20 Mar 2018 17:27:41 +0100 Subject: [PATCH] Stuff about half-time report --- proposal/BACKLOG.md | 22 ++++++ proposal/halftime.tex | 177 ++++++++++++++++++++++++++++++++++++++++++ proposal/macros.tex | 6 ++ proposal/proposal.tex | 3 + 4 files changed, 208 insertions(+) create mode 100644 proposal/BACKLOG.md create mode 100644 proposal/halftime.tex diff --git a/proposal/BACKLOG.md b/proposal/BACKLOG.md new file mode 100644 index 0000000..b889c92 --- /dev/null +++ b/proposal/BACKLOG.md @@ -0,0 +1,22 @@ +Remove stuff about models of type theory + +Add references to specific (noteable) implementaitons of category theory: +* Unimath +* cubicaltt +* https://github.com/pcapriotti/agda-categories +* https://github.com/copumpkin/categories +* ... + +Talk about structure of library: +=== + +Propositional- and non-propositional stuff split up +Providing "equiality principles" +Provide overview of what has been proven. + +What can I say about reusability? + +Misc +==== + +Propositional content diff --git a/proposal/halftime.tex b/proposal/halftime.tex new file mode 100644 index 0000000..11dc836 --- /dev/null +++ b/proposal/halftime.tex @@ -0,0 +1,177 @@ +\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. diff --git a/proposal/macros.tex b/proposal/macros.tex index d1bf101..2653ac3 100644 --- a/proposal/macros.tex +++ b/proposal/macros.tex @@ -18,3 +18,9 @@ \newcommand{\fmap}{\mathit{fmap}} \newcommand{\idFun}{\mathit{id}} \newcommand{\Sets}{\mathit{Sets}} +\newcommand{\Set}{\mathit{Set}} +\newcommand{\MCU}{\UU} +\newcommand{\isSet}{\mathit{isSet}} +\newcommand{\tp}{\;\mathord{:}\;} +\newcommand{\subsubsubsection}[1]{\textbf{#1}} +\newcommand{\WIP}[1]{\textbf{[WIP]}} diff --git a/proposal/proposal.tex b/proposal/proposal.tex index c6cb67d..073ecb5 100644 --- a/proposal/proposal.tex +++ b/proposal/proposal.tex @@ -13,6 +13,8 @@ \usepackage{multicol} \usepackage{amsmath,amssymb} \usepackage[toc,page]{appendix} +\usepackage{xspace} + % \setlength{\parskip}{10pt} % \usepackage{tikz} @@ -282,5 +284,6 @@ The thesis shall conclude with a discussion about the benefits of Cubical Agda. \bibliography{refs} \begin{appendices} \input{planning.tex} +\input{halftime.tex} \end{appendices} \end{document}