Research Repository

See what's under the surface

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), doi: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

Quotient inductive-inductive types (2017)
Conference Proceeding
Altenkirch, T., Capriotti, P., Dijkstra, G., Kraus, N., & Nordvall Forsberg, F. (2017). Quotient inductive-inductive types. In C. Baier, & U. Dal Lago (Eds.), FoSSaCS 2018: Foundations of Software Science and Computation Structures, 293-310. doi:10.1007/978-3-319-89366-2_16

Higher inductive types (HITs) in Homotopy Type Theory (HoTT) allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotient types and allow to define types which are not sets in the sense of H... Read More