Formalized results from the literature

[fredrik-bakke]

We should have a list of publications that are formalized in the library. This would be good for exposition, would give new readers some pointers for what to read in the library, and would allow us to brag a little about what the library contains.

The way I see it, the list should be split into two sections. One where the original publication was made with our library in mind, and one where the formalization appeared after the publication, and/or where it may not have been formalized by any of the original authors of the publication. We can also consider subdividing it further into more and less "serious" publications. E.g. published papers in high-standing journals vs. pre-prints & blog posts.

A list of desiderata are

• [ ] Have lists of formalized publications
• [ ] Add references to main theorems where they are formalized
• [ ] Have guidelines for when this list can be updated
• [ ] Some sort of credit-giving mechanism to the formalizers
• [ ] Have a list of work-in-progress formalizations of publications

Depends on #957.

[fredrik-bakke]

I'll try to compile a list of such publications in this comment, please comment below if you have any additions/corrections to make.

Publications with intended formalizations

• The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations https://arxiv.org/abs/2402.04893
• Mangel É. and Rijke E. "Delooping the sign homomorphism in univalent mathematics".
• Introduction to Homotopy Type Theory https://arxiv.org/abs/2212.11082
• Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson, Symmetry (draft, GitHub)
• the forthcoming Acyclic types?

Work-in-progress formalizations of publications that are not part of the publication

• Michael Shulman, Brouwer's fixed-point theorem in real-cohesive homotopy type theory, 2015 (arXiv:1509.07584)
• Michael Shulman, Idempotents in intensional type theory, 2015 (arXiv:1507.03634)
• Egbert Rijke, Michael Shulman, Bas Spitters, Modalities in homotopy type theory, Logical Methods in Computer Science, Volume 16, Issue 1, 2020 (arXiv:1706.07526, DOI:10.23638/LMCS-16(1:2)2020)
• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013) (website, arXiv:1308.0729)
• Benedikt Ahrens and Krzysztof Kapulkin and Michael Shulman, Univalent Categories and the Rezk completion (2015) (arXiv:1303.0584, DOI:10.1017/S0960129514000486)
  • [Wär23]: David Wärn. Path spaces of pushouts. Preprint. https://dwarn.se/po-paths.pdf. 2023.
• Egbert Rijke, The join construction, 2017 (arXiv:1701.07538)
• Egbert Rijke, Classifying Types (arXiv:1906.09435)
• Martín H. Escardó, The Cantor–Schröder–Bernstein Theorem for ∞-groupoids, Journal of Homotopy and Related Structures, Volume 16, Issue 3, 2021 (arXiv:2002.07079,DOI:10.1007/S40062-021-00284-6)
• Kristina Sojakova and Floris van Doorn and Egbert Rijke, Sequential Colimits in Homotopy Type Theory, 2020 (DOI:10.1145/3373718.3394801)
• Nicolai Kraus and Jakob von Raumer, Path Spaces of Higher Inductive Types in Homotopy Type Theory, 2019 (arXiv:1901.06022)

[VojtechStep]

I like what the cubical people do with https://agda.github.io/cubical/Cubical.Papers.Everything.html, where they have a module per publication, and then import the constructions/lemmas/results from the actual library.

[fredrik-bakke]

Ah, that's a bit similar to how we organize the OEIS page, that could work!