nLab Nicolai Kraus

Selected writings

On the universal property of propositional truncation:

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

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

On higher inductive types in homotopy type theory:

On quotient inductive types:

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

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

On quotient types and higher inductive types:

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

category: people

Last revised on May 7, 2023 at 18:10:42. See the history of this page for a list of all contributions to it.