\begin{center}
\LARGE
Universal structure and categorical reasoning in type theory

\end{center}

\begin{center}
\Large
Makoto Takeyama

\end{center}

\noindent
Date:  July 18th (Thursday)\\
Time:  15:05-15:25\\

\begin{center}
\large
Abstract
\end{center}

Computer implementations of type theory have been used for studies of various formalized objects
in both computer science and mathematics. Category theory can provide a unifying and clarifying
framework for such studies. Universal structure is a classification scheme for categories with extra
structure that is aimed at machine-checked, interactive development of categorical proofs in a type
theory implementation. The traditional classification, (essentially) algebraic structure on
categories, tends to force unnatural thinking and awkward computation for this purpose. To avoid
the problems, we define universal structure in terms of universal properties, universality being the
most important and most central concept of category theory. We express universal properties by
representability of appropriate functors / modules, so we develop some basic theory of
representability. Many instances of universal structure are of great interest to computer scientists,
such as cartesian closed structure, fibrations with extra structure, limits, colimits, and natural
numbers objects. We use our definition of universal structure to develop a ``category theory layer''
on top of the LEGO implementation of type theory, and discuss the difficulties encountered. 

