Univalent higher categories via complete semi-segal types

Capriotti, Paolo; Kraus, Nicolai

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.

Out of the large variety of approaches to higher category theory that mathematicians have proposed, we believe that, for type theory, the simplicial strategy is best suited. Work by Lurie and Harpaz motivates the following definition. Given the first (n + 3) levels of a semisimplicial type S, we can equip S with three properties: first, contractibility of the types of certain horn fillers; second, a completeness property; and third, a truncation condition. We call this a complete semi-Segal n-type. This is very similar to an earlier suggestion by Schreiber.

The definition of a univalent (1-) category by Ahrens et al. can easily be extended or restricted to the definition of a univalent n-category (more precisely, (n, 1)-category) for n ∈ {0, 1, 2}, and we show that the type of complete semi-Segal n-types is equivalent to the type of univalent n-categories in these cases. Thus, we believe that the notion of a complete semi-Segal n-type can be taken as the definition of a univalent n-category.

We provide a formalisation in the proof assistant Agda using a completely explicit representation of semi-simplicial types for levels up to 4.

• Journal Article Type: Article
• Acceptance Date: Sep 26, 2017
• Online Publication Date: Dec 27, 2017
• Publication Date: Jan 31, 2018
• Deposit Date: Jan 29, 2018
• Publicly Available Date: Jan 29, 2018
• Journal: Proceedings of the ACM on Programming Languages
• Electronic ISSN: 2475-1421
• Publisher: Association for Computing Machinery (ACM)
• Peer Reviewed: Peer Reviewed
• Volume: 2
• Issue: POPL
• DOI: https://doi.org/10.1145/3158132
• Keywords: Homotopy type theory, higher categories, complete Segal spaces
• Public URL: https://nottingham-repository.worktribe.com/output/907619
• Publisher URL: https://dl.acm.org/citation.cfm?doid=3177123.3158132
• Related Public URLs: https://arxiv.org/abs/1707.03693; https://gitlab.com/pcapriotti/agda-segal