### 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

### Selected Teaching

- Together with Paolo Capriotti I'm teaching 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) will focus 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:

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