All Outputs (2)

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.

Notions of anonymous existence in Martin-Löf type theory (2017)
Journal Article
Kraus, N., Escardo, M., Coquand, T., & Altenkirch, T. (in press). Notions of anonymous existence in Martin-Löf type theory. Logical Methods in Computer Science, 13(1),

As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-L\"of type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do have uniqu... Read More about Notions of anonymous existence in Martin-Löf type theory.