nLab mathematics presented in homotopy type theory

Idea

Homotopy type theory is a formal language in which it is possible to carry out synthetic mathematics using proof assistants, such as Coq and Agda. This is also possible in extensions to modal homotopy type theory.

Existing work

Homotopy type theory

Work conducted in homotopy type theory:

• HoTT book

• Dan Licata, Michael Shulman, Calculating the Fundamental Group of the Circle in Homotopy Type Theory, (arXiv:1301.3443), (doi).

• Kuen-Bang Hou (Favonia), Robert Harper, Covering Spaces in Homotopy Type Theory, (pdf), (doi).

• Ulrik Buchholtz, Floris van Doorn, Egbert Rijke, Higher Groups in Homotopy Type Theory, (arXiv:1802.04315), (doi).

• Nicolai Kraus, Thorsten Altenkirch, Free Higher Groups in Homotopy Type Theory, (arXiv:1805.02069), (doi)

• Daniel Christensen, Morgan Opie, Egbert Rijke, Luis Scoccola, Localization in Homotopy Type Theory, (arXiv:1807.04155), (doi).

• Guillaume Brunerie, The James construction and $\pi_4(S^3)$ in homotopy type theory, (arXiv:1710.10307), (doi).

• Dan Licata, Guillaume Brunerie, $\pi_n(S^n)$ in Homotopy Type Theory, Invited Paper, CPP 2013, PDF.

• Ulrik Buchholtz, Egbert Rijke, The Cayley-Dickson Construction in Homotopy Type Theory, (arXiv:1610.01134) (doi):

Construction of the quaternionic Hopf fibration

• Ulrik Buchholtz, Kuen-Bang Hou (Favonia), Cellular Cohomology in Homotopy Type Theory, Logical Methods in Computer Science, Volume 16, Issue 2 (June 1, 2020) (arXiv:1802.02191, lmcs:6518).

• Ulrik Buchholtz, Egbert Rijke, The real projective spaces in homotopy type theory, (arXiv:1704.05770), (doi).

• Robert Graham?, Synthetic Homology in Homotopy Type Theory, (arXiv:1706.01540)

• Guillaume Brunerie, On the homotopy groups of spheres in homotopy type theory, (arXiv:1606.05916)

• Kevin Quirin?, Nicolas Tabareau, Lawvere-Tierney sheafification in Homotopy Type Theory, Journal of Formalized Reasoning, ASDD-AlmaDL, 2016, 9 (2), 0.6092/issn.1972-5787/6232. hal-01451710, PDF

• Kuen-Bang Hou (Favonia), Eric Finster, Dan Licata, Peter LeFanu Lumsdaine, A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory, (arXiv:1605.03227), (doi).

• Kuen-Bang Hou (Favonia), Michael Shulman, The Seifert–van Kampen Theorem in Homotopy Type Theory, 2016, (pdf), (doi)

• Dan Licata and Eric Finster, Eilenberg-MacLane Spaces in Homotopy Type Theory, LICS 2014, PDF, (doi)

• Floris van Doorn, Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Egbert Rijke, and Mike Shulman, Spectral Sequences in Homotopy Type Theory. Paper forthcoming. 2018. github.

• Luis Scoccola, Nilpotent Types and Fracture Squares in Homotopy Type Theory (arXiv:1903.03245), (doi)

• Auke B. Booij, Analysis in univalent type theory (2020) $[$etheses:10411, pdf$]$

  (on analysis)

• Kristina Sojakova, The equivalence of the torus and the product of two circles in homotopy type theory, (arXiv:1510.03918)

• Ulrik Buchholtz, Higher Structures in Homotopy Type Theory, (arXiv:1807.02177)

• Nicolai Kraus, Jakob von Raumer, Path Spaces of Higher Inductive Types in Homotopy Type Theory, (arXiv:1901.06022)

• Ulrik Buchholtz, Egbert Rijke, The long exact sequence of homotopy $n$-groups, (arXiv:1912.08696), (doi).

• Daniel Christensen, Luis Scoccola, The Hurewicz theorem in Homotopy Type Theory, (arXiv:2007.05833), (doi).

• Martin E. Bidlingmaier, Florian Faissole, Bas Spitters, Synthetic topology in Homotopy Type Theory for probabilistic programming (arXiv:1912.07339)

• Ayberk Tosun, Formal Topology in Univalent Foundations, (pdf, slides)

• Daniel Carranza, Jonathan Chang, Chris Kapulkin, Ryan Sandford, 2-adjoint equivalences in homotopy type theory, (arXiv:2008.12433)

• Andrew Swan, On the Nielsen-Schreier Theorem in Homotopy Type Theory (arXiv:2010.01187) and (lmcs:8989).

  (on the Nielsen-Schreier theorem)

• Håkon Robbestad Gylterud, Elisabeth Bonnevier, Non-wellfounded sets in homotopy type theory, (arXiv:2001.06696)

• Martín Hötzel Escardó, Injective types in univalent mathematics, (arXiv:1903.01211, published online 5th January 2021 in Mathematical Structures in Computer Science)

• Martín Hötzel Escardó, The Cantor-Schröder-Bernstein Theorem for ∞-groupoids, (arXiv:2002.07079)

• Tom de Jong, Martín Hötzel Escardó, Domain Theory in Constructive and Predicative Univalent Foundations, in: 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, LIPIcs proceedings 183, 2021 (doi:10.4230/LIPIcs.CSL.2021.28, arXiv:2008.01422)

  (on domain theory)

• Martín Hötzel Escardó and Cory Knapp, Partial Elements and Recursion via Dominances in Univalent Type Theory, (LIPIcs:2017:7682)

• Martín Hötzel Escardó, Compact, totally separated and well-ordered types in univalent mathematics, (abstract at the author’s web page, also available at the Types 2019 Book of Abstracts)

• Marc Bezem, Ulrik Buchholtz, Daniel Grayson, Michael Shulman, Construction of the Circle in UniMath, (arXiv:1910.01856), (doi)

• Anders Mörtberg, Loïc Pujet, Cubical synthetic homotopy theory, CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs January 2020, pp. 158–171, doi:10.1145/3372885.3373825, (pdf)

• David Wärn, Eilenberg–Maclane spaces and stabilisation in homotopy type theory, Homotopy Relat. Struct. 18, 357–368 (2023), (doi).

• David Wärn, Path spaces of pushouts, (arXiv:2402.12339).

Modal homotopy type theory

Work which uses modal homotopy type theory, with, for example, modalities for cohesion, differential cohesion and supergeometry:

• Mike Shulman, Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (arXiv:1509.07584, doi:10.1017/S0960129517000147)

• Felix Wellen, Cartan Geometry in Modal Homotopy Type Theory, (arXiv:1806.05966)

• Felix Wellen, Cohesive Covering Theory (Extended Abstract), (pdf);

• David Jaz Myers, Good Fibrations through the Modal Prism, (arXiv:1908.08034), (doi).

• David Jaz Myers, Mitchell Riley, Commuting Cohesions, (arXiv:2301.13780).

• J. Daniel Christensen, Egbert Rijke,

  Characterizations of modalities and lex modalities, Journal of Pure and Applied Algebra, Volume 226, Issue 3, 2022, (doi).

See also Some thoughts on the future of modal homotopy type theory.