FP Lab logo (Sigma to lambda with equality), by Jacob Neumann at Copenhagen's Blaa Planet Aquarium drinking Geisha at the Coffee Collective in Copenhagen speaking at the Josephinum to Sy Friedman

Ulrik Buchholtz

Ulrik Buchholtz Home

Papers and preprints

  • The Yoneda embedding in simplicial type theory, with Daniel Gratzer and Jonathan Weinberger: arXiv
  • Directed univalence in simplicial homotopy type theory, with Daniel Gratzer and Jonathan Weinberger: arXiv
  • Epimorphisms and Acyclic Types in Univalent Mathematics, with Tom de Jong and Egbert Rijke: arXiv, doi
  • Primitive Recursive Dependent Type Theory, with Johannes Schipp von Branitz: arXiv, doi
  • On symmetries of spheres in univalent foundations, with Marc Bezem, Pierre Cagne and Nicolai Kraus: arXiv, doi
  • Central H-spaces and banded types, with J. Daniel Christensen, Jarl G. Taxerås Flaten and Egbert Rijke: arXiv, doi
  • 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, doi
  • The long exact sequence of homotopy n-groups, with Egbert Rijke: arXiv, doi
  • Construction of the Circle in UniMath, with Marc Bezem, Dan Grayson, and Michael Shulman: arXiv, doi
  • 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, doi
  • 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

  • If you want me to supervise your BSc or MSci project in CS or CS+AI at the University of Nottingham, check out the projects page.
  • I'm teaching COMP1043, Mathematics for Computer Scientists 2, at the University of Nottingham. I'm using a customized open-source textbook, Interactive Linear Algebra. The UoN edition is here.
  • I was one of the lecturers for the Midlands Graduate School 2024 (MGS). I taught an advanced course, on Synthetic Homotopy Theory. The lecture notes, with exercises, are available here: pdf.
  • I was one of the 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.

Talks

Various expository and research talks I've given:

  • On symmetries of spheres in univalent foundations, LICS 2024, Tallinn, 9 July, 2024: slides
  • Universes in simplicial type theory, TYPES 2024, Copenhagen, 13 June, 2023: slides
  • Coinductive definitions and constructive mathematics, Workshop on inductive definitions, Prague, 3 May, 2024: slides
  • On epimorphisms and acyclic types in univalent mathematics, HoTT/UF Workshop, Vienna, 23 April, 2023: slides
  • 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, 14 June, 2021: video, slides
  • (Co)cartesian families in simplicial type theory, HoTTEST, 22 April, 2021: video, slides
  • What Rests on What, Homotopically?, CMU Philosophy Colloquium, 14 February, 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, 15 March, 2019: video
  • Non-abelian cohomology, Geometry in Modal HoTT, CMU, 13 March, 2019: video
  • A mode theory for a type theory of cubical and simplicial types, EUTypes2018, Aarhus, 9 October, 2018: slides
  • From Higher Groups to Homotopy Surfaces, HoTTEST, 29 March, 2018: video, slides
  • Formalizing type theory in type theory using nominal techniques, HoTT/UF Workshop, FSCD 2017, Oxford, UK, 9 September, 2017: slides
  • Nominal applications of the classifying space of the finitary permutation group, Big Proof meeting at the Isaac Newton Institute, Cambridge, UK, 6 July, 2017: abstract and video
  • Higher groups and projective spaces in HoTT, CMU, 23 September, 2016: notes
  • Proof theory of homotopy type theory: what we know so far, FoMUS talk, 22 July, 2016: slides, video
  • Synthetic homotopy theory and higher inductive types, FoMUS workshop, July, 2016: slides
  • The quaternionic Hopf fibration in HoTT, CMU, 22 January, 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, 28 March, 2015.
  • Proof-theoretic ordinals related to unfoldings, Münchenwiler, October, 2014: slides
  • Lower bounds in type theory with ordinals and universes, Münchenwiler, 20 June, 2014: slides
  • Survey of systems of strength ψ(ΓΩ+1), PCC 2014, Paris: slides
  • Two operational systems of strength ψ(ΓΩ+1), 13 March, 2014: slides
  • The Unfolding of Systems of Inductive Definitions, 31 October, 2013: slides
  • Univalent Foundations and the Structure Identity Principle, 8 January, 2013: slides
  • Formalizing forcing arguments in subsystems of second-order arithmetic, 26 April, 2011: slides
  • Functional interpretation and inductive definitions, 1 February, 2011: slides
  • Transfinitely iterated fixpoint theories, 26 October and 2 November, 2010: slides
  • Functional interpretation of arithmetical comprehension, 27 May, 2010: slides
  • Normalization of intuitionistic set theories, 13 April, 2010: slides
  • Geometric theorem proving, 3 March, 2010: slides
  • Girard-Reynolds System F, 3 December, 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.