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

Ulrik Buchholtz

Ulrik Buchholtz Home

Papers and preprints

  • Unordered pairs in homotopy type theory: draft version
  • Using Displayed Univalent Graphs to Formalize Higher Groups in Univalent Foundations, with Johannes Schipp von Branitz: draft version
  • Synthetic fibered (∞,1)-category theory, with Jonathan Weinberger: arXiv
  • The long exact sequence of homotopy n-groups, with Egbert Rijke: arXiv
  • Construction of the Circle in UniMath, with Marc Bezem and Dan Grayson: arXiv
  • Higher Structures in Homotopy Type Theory, a chapter for the FOMUS book: arXiv, doi
  • Higher Groups in Homotopy Type Theory, with Floris van Doorn and Egbert Rijke: arXiv, doi
  • Cellular Cohomology in Homotopy Type Theory, with Kuen-Bang Hou (Favonia): arXiv, doi
  • Syntactic Forcing Models for Coherent Logic, with Marc Bezem and Thierry Coquand: arXiv, doi
  • Homotopy Type Theory in Lean, with Floris van Doorn and Jakob von Raumer: arXiv, doi
  • The real projective spaces in homotopy type theory, with Egbert Rijke: arXiv, doi
  • Varieties of Cubical Sets, with Edward Morehouse: arXiv, doi
  • The Cayley-Dickson Construction in Homotopy Type Theory, with Egbert Rijke: arXiv, journal
  • Theories of proof-theoretic strength ψ(ΓΩ+1), with Gerhard Jäger and Thomas Strahm: preprint, doi

Symmetry Book

Together with Marc Bezem, Pierre Cagne, Bjørn Dundas, and Dan Grayson, I'm writing a book on group theory from the perspective of univalent mathematics and homotopy type theory. Working title: Symmetry

Selected Teaching

  • Together with Paolo Capriotti I taught a 2-semester sequence on Homotopy Type Theory. In WiSe19/20, Part I was an introduction to type theory (and constructive mathematics) together with univalence and higher inductive types as a tool for synthetic homotopy theory. In SoSe2020, Part II (by Paolo) focused on models with an emphasis on the simplicial model.
  • In Spring 2016, I taught a Seminar on Intuitionism and Constructive Mathematics at CMU, including historical, philosophical, and mathematics aspects. A large part was composed of student presentation. Most meetings were filmed and can be viewed on YouTube.


Various expository and research talks I've given:

  • Update on semisimplicial types in homotopy type theory, CIRM workshop 2689: slides
  • Toposes for probabilistic programming, CIRM workshop 2686: slides
  • Genuine pairs and the trouble with triples in homotopy type theory, Invited talk at TYPES, June 14, 2021: video, slides
  • (Co)cartesian families in simplicial type theory, HoTTEST, April 22, 2021: video, slides
  • What Rests on What, Homotopically?, CMU Philosophy Colloquium, February 24, 2020: slides
  • Higher Algebra in Homotopy Type Theory, Formal Methods in Mathematics / Lean Together 2020: slides, video
  • Universes in toy models of spatial type theory, Geometry in Modal HoTT, CMU, March 15, 2019: video
  • Non-abelian cohomology, Geometry in Modal HoTT, CMU, March 13, 2019: video
  • A mode theory for a type theory of cubical and simplicial types, EUTypes2018, Aarhus, October 9, 2018: slides
  • From Higher Groups to Homotopy Surfaces, HoTTEST, March 29, 2018: video, slides
  • Formalizing type theory in type theory using nominal techniques, HoTT/UF Workshop, FSCD 2017, Oxford, UK, September 9, 2017: slides
  • Nominal applications of the classifying space of the finitary permutation group, Big Proof meeting at the Isaac Newton Institute, Cambridge, UK, July 6, 2017: abstract and video
  • 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, video
  • 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

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.

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 4.0 License.