All Outputs (3)

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.

Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type (2017)
Conference Proceeding
Altenkirch, T., Danielson, N. A., & Kraus, N. (2017). Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type. In Foundations of Software Science and Computation Structures: FoSSaCS 2017 (534-549). https://doi.org/10.1007/978-3-662-54458-7_31

Capretta's delay monad can be used to model partial computations, but it has the ``wrong'' notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the ``right''notion of equality, weak bisimilarity. However,... Read More about Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type.