HoTT Mathematics

Перелік гомотопічної математики, теореми якої механічно доводяться в імплементаціях гомотопічної теорії типів (HoTT).

Mathematics in Homotopy Type Theory:
• Symmetry: A book project about group theory from the univalent point of view, [1].
• Modalities and reflective subuniverses, [16].
• Higher Groups (k-symmetric n-groups), [3].
• ∥ΣA∥2 is a 1-type for all sets A, [13].
• Localization and L-separated types, [8].
• The James construction and π4(S3), [2].
• The Cayley-Dickson construction and the H-space structure on S3, [5].
• The join construction, [15].
• Cellular cohomology, [4].
• Real projective spaces RPn, [7].
• Homology theory, [12].
• Blakers-Massey connectivity theorem, [10].
• Seifert-van Kampen theorem, [11].
• Nilpotent types and fracture squares, [17].
• Eilenberg-MacLane Spaces K(G, n), [14].
• Spectral sequences, [9].
• Long exact sequence of homotopy n-groups, [6].
• Brouwer’s fixed-point theorem in real-cohesion, [18].
• Cartan Geometry using a modality, [19].
• Synthetic Cohomology Theory in Cubical Agda [20].
• Computing Cohomology Rings in Cubical Agda [21].

Some open problems:
• Do more “ordinary” (≤ 2-truncated) mathematics: Is univalence a practical advantage for formalizing scheme or manifold theory?
• Prove Freyd’s Adjoint Functor Theorem constructively.
• Calculate more homotopy groups of spheres.
• Is ΣA a 1-type for all sets A?
• Prove that all spheres Sn are ∞-truncated.
• Define the type BSU(2) (a delooping of S3); then define BSU(n), BSO(n), etc.
• Define the type of U-small semi-simplicial types.
• For which 0- or 1-categories D can we define the type of diagrams Fun(D,U)?
• Define the type of (∞, 1)-categories and develop (∞, 1)-category theory.
• Define the localization type of a 1-category C: the universal type with a functor from C.
• Give a general theory of ∞-quotients that can be used to solve above.
• Formalize the meta-theory of type theory in itself and show that lex modalities give inner models,
and that we have other model constructions from internal sites (and maybe internal realizability models?).

These are some open-ended discussion questions:
• What’s a good foundational framework for mathematics? Which criteria are essential, and which are “nice to have”?
• How does set theory fare according to your criteria? • How does (homotopy) type theory fare?

References:
[1] Marc Bezem, Ulrik Buchholtz, Bjorn Dundas, Dan Grayson, et al. Symmetry. 2020. url: https://github.com/ UniMath/SymmetryBook.
[2] Guillaume Brunerie. “The James Construction and π4(S3) in Homotopy Type Theory”. In: J. Autom. Reason. 63.2 (Aug. 2019), pp. 255–284. doi: 10.1007/s10817-018-9468-2. arXiv: 1710.10307.
[3] Ulrik Buchholtz, Floris van Doorn, and Egbert Rijke. “Higher Groups in Homotopy Type Theory”. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. LICS ’18. Oxford, United Kingdom: Association for Computing Machinery, 2018, pp. 205–214. doi: 10.1145/3209108.3209150. arXiv: 1802.04315.
[4] Ulrik Buchholtz and Favonia. “Cellular Cohomology in Homotopy Type Theory”. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. LICS ’18. Oxford, United Kingdom: Association for Computing Machinery, 2018, pp. 521–529. doi: 10.1145/3209108.3209188. arXiv: 1802.02191.
[5] Ulrik Buchholtz and Egbert Rijke. “The Cayley-Dickson construction in homotopy type theory”. In: Higher Structures 2.1 (2018), pp. 30–41. arXiv: 1610.01134.
[6] Ulrik Buchholtz and Egbert Rijke. The long exact sequence of homotopy n-groups. 2019. arXiv: 1912.08696.
[7] Ulrik Buchholtz and Egbert Rijke. “The real projective spaces in homotopy type theory”. In: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Los Alamitos, CA, USA: IEEE Computer Society, June 2017, pp. 1–8. doi: 10.1109/LICS.2017.8005146. arXiv: 1704.05770.
[8] J. Daniel Christensen, Morgan Opie, Egbert Rijke, and Luis Scoccola. Localization in Homotopy Type Theory. 2018. arXiv: 1807.04155.
[9] Floris van Doorn, Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Egbert Rijke, and Michael Shulman. Spectral Sequences in Homotopy Type Theory. 2019. url: https://github.com/cmu-phil/Spectral.
[10] Favonia, Eric Finster, Daniel R. Licata, and Peter L. Lumsdaine. “A Mechanization of the Blakers–Massey Connectivity Theorem in Homotopy Type Theory”. In: 2016 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). July 2016, pp. 1–10. arXiv: 1605.03227. url: https://ieeexplore.ieee.org/document/8576476.
[11] Favonia and Michael Shulman. “The Seifert-van Kampen Theorem in Homotopy Type Theory”. In: 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Ed. by Jean-Marc Talbot and Laurent Regnier. Vol. 62. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2016, 22:1–22:16. doi: 10.4230/LIPIcs.CSL.2016.22.
[12] Robert Graham. Synthetic Homology in Homotopy Type Theory. 2017. arXiv: 1706.01540.
[13] Nicolai Kraus and Thorsten Altenkirch. “Free Higher Groups in Homotopy Type Theory”. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. LICS ’18. Oxford, United Kingdom: Association for Computing Machinery, 2018, pp. 599–608. doi: 10.1145/3209108.3209183. arXiv: 1805.02069.
[14] Daniel R. Licata and Eric Finster. “Eilenberg-MacLane Spaces in Homotopy Type Theory”. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). CSL-LICS ’14. Vienna, Austria: Association for Computing Machinery, 2014. doi: 10.1145/2603088.2603153.
[15] Egbert Rijke. The join construction. 2017. arXiv: 1701.07538.
[16] Egbert Rijke, Michael Shulman, and Bas Spitters. “Modalities in homotopy type theory”. In: Logical Methods in Computer Science 16.1 (Jan. 2020). arXiv: 1706.07526. url: https://lmcs.episciences.org/6015.
[17] Luis Scoccola. Nilpotent Types and Fracture Squares in Homotopy Type Theory. 2019. arXiv: 1903.03245.
[18] Michael Shulman. “Brouwer’s fixed-point theorem in real-cohesive homotopy type theory”. In: Mathematical Structures in Computer Science 28.6 (2018), pp. 856–941. doi: 10.1017/S0960129517000147. arXiv: 1509.07584.
[19] Felix Wellen. Cartan Geometry in Modal Homotopy Type Theory. 2018. arXiv: 1806.05966.
[20] Guillaume Brunerie, Axel Ljungström, Anders Mörtberg. Synthetic Cohomology Theory in Cubical Agda https://staff.math.su.se/anders.mortberg/papers/zcohomology.pdf
[21] Thomas Lamiaux, Axel Ljungström, Anders Mörtberg. Computing Cohomology Rings in Cubical Agda https://arxiv.org/pdf/2212.04182 https://hott-uf.github.io/2023/slides/Lamiaux.pdf