Formalization of abelian (Grothendieck-) univalent categories of ring-modules, in homotopy type theory (univalent foundations of mathematics):
On delooping, H-spaces and Eilenberg-MacLane spaces in homotopy type theory:
Ulrik Buchholtz, J. Daniel Christensen, Jarl G. Taxerås Flaten, Egbert Rijke, Central H-spaces and banded types [arXiv:2301.02636]
Jarl G. Taxerås Flaten, Central H-spaces and banded types, Homotopy Type Theory Electronic Seminar Talks, 17 November 2022 (slides, video).
Last revised on June 13, 2023 at 16:59:32. See the history of this page for a list of all contributions to it.