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:
Last revised on February 2, 2023 at 19:09:28. See the history of this page for a list of all contributions to it.