drinking Geisha at the Coffee Collective in Copenhagen speaking at the Josephinum to Sy Friedman at Copenhagen's Blaa Planet Aquarium

Ulrik Buchholtz

Ulrik Buchholtz Home

Papers and preprints

  • The Cayley-Dickson Construction in Homotopy Type Theory, with Egbert Rijke: preprint, arxiv
  • Theories of proof-theoretic strength ψ(ΓΩ+1), with Gerhard Jäger and Thomas Strahm: preprint, chapter


  • Intuitionism and Constructive Mathematics — 80-518/818 at CMU, Spring 2016: course webpage
  • Category Theory — 80-413/713 at CMU, Spring 2015: course webpage


  • Formal systems for Foundations of Mathematics
  • Homotopy Type Theory
  • Feferman's Unfolding Program & Explicit Mathematics

PhD Thesis

December 6, 2013 I finished my PhD thesis at Stanford University under the direction of Solomon Feferman. You can download my thesis here: Unfolding of Systems of Inductive Definitions. If you want a paper version, it can be acquired cheaply from amazon.com, amazon.co.uk, amazon.de, and other book sellers.


Various expository and research talks I've given:

  • Higher groups and projective spaces in HoTT, CMU, September 23, 2016: notes
  • Proof theory of homotopy type theory: what we know so far, FoMUS talk, July 22, 2016: slides
  • Synthetic homotopy theory and higher inductive types, FoMUS workshop, July, 2016: slides
  • The quaternionic Hopf fibration in HoTT, CMU, January 22, 2016: video (cf. slides prepared for a similar talk at MPIM in Bonn, February 12, 2016; however, I used the blackboards instead.)
  • Primitive recursive homotopy type theory, ASL meeting in Urbana, March 28, 2015.
  • Proof-theoretic ordinals related to unfoldings, Münchenwiler, October, 2014: slides
  • Lower bounds in type theory with ordinals and universes, Münchenwiler, June 20, 2014: slides
  • Survey of systems of strength ψ(ΓΩ+1), PCC 2014, Paris: slides
  • Two operational systems of strength ψ(ΓΩ+1), March 13, 2014: slides
  • The Unfolding of Systems of Inductive Definitions, October 31, 2013: slides
  • Univalent Foundations and the Structure Identity Principle, January 8, 2013: slides
  • Formalizing forcing arguments in subsystems of second-order arithmetic, April 26, 2011: slides
  • Functional interpretation and inductive definitions, February 1, 2011: slides
  • Transfinitely iterated fixpoint theories, October 26 and November 2, 2010: slides
  • Functional interpretation of arithmetical comprehension, May 27, 2010: slides
  • Normalization of intuitionistic set theories, April 13, 2010: slides
  • Geometric theorem proving, March 3, 2010: slides
  • Girard-Reynolds System F, December 3, 2009: slides

MSc Thesis

I wrote my MSc thesis at the University of Copenhagen. My advisor was Jesper Grodal, and you can download my thesis here: The Atiyah-Segal Completion Theorem.

Creative Commons License Work by Ulrik Buchholtz licensed under a Creative Commons Attribution-Noncommercial-Share Alike 3.0 United States License.