## Thorsten Altenkirch (University of Nottingham (UK)), What is a category? (in univalent type theory)

### Schedule

- Feb. 11, 2016, 10:30 - 12:00

### Abstract

Category theory is one of the main tools in theoretical computer
science. Univalent type theory allows us to represent ordinary category
theory in a very straightforward way but we need to assume that the
hom-types are **sets** in the sense of univalent type theory, that is
their equalities are mere propositions. In my talk I a going to explore
how we can lift this limitation and how we can define
(\omega,1)-categories in a 2-level type theory. The 2-level theory is
necessary because we have to distinguish between **strict** and **weak**
equality and consequently between **types** and **pretypes**. One
application of this approach is a generic theory of higher inductive
types.

This is based on ongoing work with Paolo Capriotti, Gabe Dijkstra, Frederik Forsberg and Nicolai Kraus.