On the fat Delta category:
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 a version of the Homotopy Type System with application to semi-simplicial types in homotopy type theory:
On free groups and -groups in homotopy type theory:
On quotient types and higher inductive types:
On ordinals in dependent type theory and marked extensional well-founded orders:
On ordinal exponentiation in dependent type theory, see:
Last revised on April 8, 2025 at 02:51:34. See the history of this page for a list of all contributions to it.