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.