Univalent higher categories via complete semi-segal types
(2017)
Journal Article
Capriotti, P., & Kraus, N. (2018). Univalent higher categories via complete semi-segal types. Proceedings of the ACM on Programming Languages, 2(POPL), https://doi.org/10.1145/3158132
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... Read More about Univalent higher categories via complete semi-segal types.