• Higher Structures in Homotopy Type Theory
    In Stefania Centrone, Deborah Kant & Deniz Sarikaya (eds.), Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts, Springer Verlag. pp. 151-172. 2019.
    The intended model of the homotopy type theories used in Univalent Foundations is the ∞-category of homotopy types, also known as ∞-groupoids. The problem of higher structures is that of constructing the homotopy types needed for mathematics, especially those that aren’t sets. The current repertoire of constructions, including the usual type formers and higher inductive types, suffice for many but not all of these. We discuss the problematic cases, typically those involving an infinite hierarchy…Read more
  • Higher Structures in Homotopy Type Theory
    In Deniz Sarikaya, Deborah Kant & Stefania Centrone (eds.), Reflections on the Foundations of Mathematics, Springer Verlag. 2019.
  •  29
    Theories of Proof-Theoretic Strength Ψ
    with Thomas Strahm and Gerhard Jäger
    In Peter Schuster & Dieter Probst (eds.), Concepts of Proof in Mathematics, Philosophy, and Computer Science, De Gruyter. pp. 115-140. 2016.