Abstract

Category theory internally in homotopy type theory is intricate as categorical laws can only be stated ‘up to homotopy’, requiring coherence (similar to how the associator in a bicategory requires the pentagon). To avoid this, one can consider definitions with truncated types such as the univalent categories by Ahrens-Kapulkin-Shulman, which however fail to capture some important examples. A more general structure are (n,1)-categories, ideally with n = infinity, and a possible definition is given by Capriotti’s complete semi-Segal types. I will show how simplified (complete) semi-Segal types are indeed equivalent to univalent categories. Very much related is the question what an appropriate notion of a type-valued diagram is (joint work with Sattler). Using the type universe as a semi-Segal type, I will present several constructions of homotopy coherent diagrams (some of them infinite) and show, as an application, how one can construct all the degeneracies that a priori are missing in a complete semi-Segal type. With a further construction, we get a (finite) definition of simplicial types (up to a finite level).