Ulrik Buchholtz

Ulrik Buchholtz Home

Papers and preprints

Central H-spaces and banded types, with J. Daniel Christensen, Jarl G. Taxerås Flaten and Egbert Rijke: arXiv
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 and Dan Grayson: 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 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 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, 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.