\chapter{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.