Add planning report
This commit is contained in:
parent
4db19b6420
commit
52dea06df9
|
@ -6,8 +6,8 @@
|
||||||
\newcommand{\bN}{\mathbb{N}}
|
\newcommand{\bN}{\mathbb{N}}
|
||||||
\newcommand{\bC}{\mathbb{C}}
|
\newcommand{\bC}{\mathbb{C}}
|
||||||
\newcommand{\bX}{\mathbb{X}}
|
\newcommand{\bX}{\mathbb{X}}
|
||||||
\newcommand{\to}{\rightarrow}}
|
\newcommand{\to}{\rightarrow}
|
||||||
\newcommand{\mto}{\mapsto}}
|
\newcommand{\mto}{\mapsto}
|
||||||
\newcommand{\UU}{\ensuremath{\mathcal{U}}\xspace}
|
\newcommand{\UU}{\ensuremath{\mathcal{U}}\xspace}
|
||||||
\let\type\UU
|
\let\type\UU
|
||||||
\newcommand{\nomen}[1]{\emph{#1}}
|
\newcommand{\nomen}[1]{\emph{#1}}
|
||||||
|
|
72
proposal/planning.tex
Normal file
72
proposal/planning.tex
Normal file
|
@ -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.
|
|
@ -12,6 +12,7 @@
|
||||||
\usepackage{parskip}
|
\usepackage{parskip}
|
||||||
\usepackage{multicol}
|
\usepackage{multicol}
|
||||||
\usepackage{amsmath,amssymb}
|
\usepackage{amsmath,amssymb}
|
||||||
|
\usepackage[toc,page]{appendix}
|
||||||
% \setlength{\parskip}{10pt}
|
% \setlength{\parskip}{10pt}
|
||||||
|
|
||||||
% \usepackage{tikz}
|
% \usepackage{tikz}
|
||||||
|
@ -279,4 +280,7 @@ The thesis shall conclude with a discussion about the benefits of Cubical Agda.
|
||||||
\nocite{cubical-demo}
|
\nocite{cubical-demo}
|
||||||
\nocite{coquand-2013}
|
\nocite{coquand-2013}
|
||||||
\bibliography{refs}
|
\bibliography{refs}
|
||||||
|
\begin{appendices}
|
||||||
|
\input{planning.tex}
|
||||||
|
\end{appendices}
|
||||||
\end{document}
|
\end{document}
|
||||||
|
|
Loading…
Reference in a new issue