nLab Nicolai Kraus (changes)

Showing changes from revision #11 to #12: Added | Removed | Changed

• webpage

Selected writings

On the universal property of propositional truncation:

• Nicolai Kraus, The General Universal Property of the Propositional Truncation, in TYPES 2014 Leibniz International Proceedings in Informatics (LIPIcs) 39 (2015) [[arXiv:1411.2682](https://arxiv.org/abs/1411.2682), doi:10.4230/LIPIcs.TYPES.2014.111]

On homotopy n-types (“homotopy levels”) in homotopy type theory:

• Nicolai Kraus, Truncation levels in Homotopy Type Theory, Nottingham (2015) [[pdf](https://eprints.nottingham.ac.uk/28986/1/thesis.pdf), eprints:28986]

On weakly constant functions and propositional truncation in homotopy type theory:

• Nicolai Kraus, Martín Escardó, Thierry Coquand, Thorsten Altenkirch, Notions of Anonymous Existence in Martin-Löf Type Theory, Logical Methods in Computer Science 13 1 [, arXiv:1610.03346]

On higher inductive types in homotopy type theory:

• Jakob von Raumer, Nicolai Kraus, Path Spaces of Higher Inductive Types in Homotopy Type Theory, 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Vancouver, Canada, 2019 (arXiv:1901.06022)

On quotient inductive types:

• Thorsten Altenkirch, Nils A. Danielsson, Nicolai Kraus, Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type, FoSSaCS 2017, Lecture Notes in Computer Science 10203 Springer (2017) [[arXiv:1610.09254](https://arxiv.org/abs/1610.09254)]

On a version of the Homotopy Type System with application to semi-simplicial types in homotopy type theory:

• Danil Annenkov, Paolo Capriotti, Nicolai Kraus, Christian Sattler: Two-Level Type Theory and Applications [[arXiv:1705.03307](https://arxiv.org/abs/1705.03307)]

On free groups and $\infty$-groups in homotopy type theory:

• Nicolai Kraus, Thorsten Altenkirch, Free Higher Groups in Homotopy Type Theory, LICS ‘18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, (2018) [[arXiv;1805.02069](https://arxiv.org/abs/1805.02069), doi:10.1145/3209108.3209183]

On quotient types and higher inductive types:

• Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, Fredrik Forsberg, Quotient inductive-inductive types, Foundations of Software Science and Computation Structures (FoSSaCS 2018), Lecture Notes in Computer Science 10803 (2018) [[doi:10.1007/978-3-319-89366-2_16](https://doi.org/10.1007/978-3-319-89366-2_16), arXiv:1612.02346]

On ordinals in type theory and marked extensional well-founded orders:

• Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu, Set-Theoretic and Type-Theoretic Ordinals Coincide [[arXiv:2301.10696](https://arxiv.org/abs/2301.10696)]

Related entries

• univalent category

• category object in an (infinity,1)-category