Nicolai Kraus

Available identifiers

zbMath Open kraus.nicolaiMaRDI QIDQ1652994

List of research outcomes

Publication	Date of Publication	Type
Path spaces of higher inductive types in homotopy type theory	2024-12-19	Paper
Two-level type theory and applications	2024-03-05	Paper
Two-level type theory and applications - ERRATUM	2024-03-05	Paper
From cubes to twisted cubes via graph morphisms in type theory	2023-10-27	Paper
Connecting constructive notions of ordinals in homotopy type theory	2023-08-08	Paper
Type-theoretic approaches to ordinals	2023-04-27	Paper
A rewriting coherence theorem with applications in homotopy type theory	2023-02-28	Paper
Set-Theoretic and Type-Theoretic Ordinals Coincide	2023-01-25	Paper
Type-Theoretic Approaches to Ordinals	2022-08-07	Paper
A Rewriting Coherence Theorem with Applications in Homotopy Type Theory	2021-07-04	Paper
Coherence via well-foundedness. Taming set-quotients in homotopy type theory	2021-01-21	Paper
Free higher groups in homotopy type theory	2021-01-20	Paper
Internal $\infty$-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT	2020-09-03	Paper
Shallow embedding of type theory is morally correct	2020-05-05	Paper
Path Spaces of Higher Inductive Types in Homotopy Type Theory	2019-01-17	Paper
Quotient inductive-inductive types	2018-07-17	Paper
Constructions with non-recursive higher inductive types	2018-04-23	Paper
Functions out of higher truncations	2017-08-31	Paper
Extending homotopy type theory with strict equality	2017-07-19	Paper
The general universal property of the propositional truncation	2017-07-12	Paper
Univalent Higher Categories via Complete Semi-Segal Types	2017-07-12	Paper
Partiality, Revisited	2017-05-19	Paper
Notions of anonymous existence in Martin-Löf type theory	2017-05-08	Paper
Space-Valued Diagrams, Type-Theoretically (Extended Abstract)	2017-04-14	Paper
Higher homotopies in a hierarchy of univalent universes	2017-01-27	Paper
Generalizations of Hedberg's theorem	2013-06-28	Paper

Research outcomes over time

This page was built for person: Nicolai Kraus