Univalent higher categories via complete Semi-Segal types
Abstract
Category theory in homotopy type theory is intricate as categorical laws can only be stated "up to homotopy", and thus require coherences. The established notion of a univalent category (as introduced by Ahrens et al.) solves this by considering only truncated types, roughly corresponding to an ordinary category. This fails to capture many naturally occurring structures, stemming from the fact that the naturally occurring structures in homotopy type theory are not ordinary, but rather higher categories.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Dec 27, 2017
- Source ID
- 10.1145/3158132
Entities
People
- Nicolai Kraus
- Paolo Capriotti
Organizations
- Engineering and Physical Sciences Research Council
- United States Air Force
- University of Nottingham