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 (to appear in Higher Structures)
  • 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

  • I'm one of lecturers for the HoTTEST Summer School 2022, a massive online event aiming to make homotopy type theory accessible to, and inclusive of, everyone who is interested, regardless of cultural background, age, ability, formal education, ethnicity, gender identity, or expression. All the lectures and problem sessions from the school are on YouTube.
  • 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.