diff --git a/proposal/macros.tex b/proposal/macros.tex index aec0c67..a092514 100644 --- a/proposal/macros.tex +++ b/proposal/macros.tex @@ -6,8 +6,8 @@ \newcommand{\bN}{\mathbb{N}} \newcommand{\bC}{\mathbb{C}} \newcommand{\bX}{\mathbb{X}} -\newcommand{\to}{\rightarrow}} -\newcommand{\mto}{\mapsto}} +\newcommand{\to}{\rightarrow} +\newcommand{\mto}{\mapsto} \newcommand{\UU}{\ensuremath{\mathcal{U}}\xspace} \let\type\UU \newcommand{\nomen}[1]{\emph{#1}} diff --git a/proposal/planning.tex b/proposal/planning.tex new file mode 100644 index 0000000..91d7cc6 --- /dev/null +++ b/proposal/planning.tex @@ -0,0 +1,72 @@ +\section{Planning report} +% +I have already implemented multiple essential building blocks for a +formalization of core-category theory. These concepts include: +% +\begin{itemize} +\item +Categories +\item +Functors +\item +Products +\item +Exponentials +\item +Natural transformations +\item +Concrete Categories +\subitem +Sets +\subitem +Cat +\subitem +Functor +\end{itemize} +% +Will all these things already in place it's my assessment that I am ahead of +schedule at this point.\footnote{I have omitted a lot of other things that + follow easily from the above, e.g. a cartesian-closed category is simply one + that has all products and exponentials.} + +Here is a plan for my thesis work organized on a week-by-week basis. +% +\begin{center} +\centering +\begin{tabular}{@{}lll@{}} +Goal & Deadline & Risk 1-5 \\ \hline +Yoneda embedding & Feb 2nd & 3 \\ +Categories with families & Feb 9th & 4 \\ +Presheafs $\Rightarrow$ CwF's & Feb 16th & 2 \\ +Cubical Category & Feb 23rd & 3 \\ +Writing seminar & Mar 2nd & \\ +Kan condition & Mar 9th & 4 \\ +Thesis outline and backlog & Mar 16th & 2 \\ +Half-time report & Mar 23rd & 2 \\ + & Mar 30th & \\ + & Apr 6th & \\ + & Apr 13th & \\ + & Apr 20th & \\ +Thesis draft & Apr 27th & 2 \\ +Writing seminar 2 & May 4th & \\ +Presentation & May 11th & \\ +Attend 1st presentation & May 18th & \\ +Attend 2nd presentation & May 25th & \\ +\end{tabular} +\end{center} +% +The first half part of my thesis-work will be focused on implementing core +elements of my Agda implementation. These core elements have been highlighted in +the above table. The elements noted there are the essential bits and pieces I +need to reach the ambitious goal of getting an implementation of a categorical +model for Cubical Type Theory. Along the way I will also have formalized +additional elements of more ``pure'' category theory. I will thus reach my goal +of formalizing (parts of) category theory. + +The high risk-factors for CwF's and the Kan-condition is due to this being +somewhat uncharted territory for me at this point. + +It's my plan that I will have formalized the core concepts needed around the +deadline for the half-time report which is due by March 23rd. Around this point +I will have a clearer idea of what additional things I need for a model of +category theory. diff --git a/proposal/proposal.tex b/proposal/proposal.tex index 7237479..c6cb67d 100644 --- a/proposal/proposal.tex +++ b/proposal/proposal.tex @@ -12,6 +12,7 @@ \usepackage{parskip} \usepackage{multicol} \usepackage{amsmath,amssymb} +\usepackage[toc,page]{appendix} % \setlength{\parskip}{10pt} % \usepackage{tikz} @@ -279,4 +280,7 @@ The thesis shall conclude with a discussion about the benefits of Cubical Agda. \nocite{cubical-demo} \nocite{coquand-2013} \bibliography{refs} +\begin{appendices} +\input{planning.tex} +\end{appendices} \end{document}