Universal structure and categorical reasoning in type theory
Date: July 18th (Thursday)
Time: 15:05-15:25
Abstract
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.
