Formalising Yoneda Ext in Univalent Foundations

Author Jarl G. Taxerås Flaten

Thumbnail PDF


  • Filesize: 0.79 MB
  • 17 pages

Document Identifiers

Author Details

Jarl G. Taxerås Flaten
  • University of Western Ontario, London, Ontario, Canada


The theory of Yoneda Ext in HoTT is joint work with Dan Christensen, to whom I am also grateful for discussions and contributions related to the formalisation. I thank Jacob Ender for contributions to the formalisation of the Baer sum, and the collaborators of the Coq-HoTT library - and Ali Caglayan in particular - for their review of, and contributions to, the various pull requests related to this project. I also thank the anonymous reviewers for valuable feedback.

Cite AsGet BibTex

Jarl G. Taxerås Flaten. Formalising Yoneda Ext in Univalent Foundations. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Ext groups are fundamental objects from homological algebra which underlie important computations in homotopy theory. We formalise the theory of Yoneda Ext groups [Yoneda, 1954] in homotopy type theory (HoTT) using the Coq-HoTT library. This is an approach to Ext which does not require projective or injective resolutions, though it produces large abelian groups. Using univalence, we show how these Ext groups can be naturally represented in HoTT. We give a novel proof and formalisation of the usual six-term exact sequence via a fibre sequence of 1-types (or groupoids), along with an application. In addition, we discuss our formalisation of the contravariant long exact sequence of Ext, an important computational tool. Along the way we implement and explain the Baer sum of extensions and how Ext is a bifunctor.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Algebraic topology
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
  • homotopy type theory
  • homological algebra
  • Yoneda Ext
  • formalisation
  • Coq


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Ulrik Buchholtz, J. Daniel Christensen, Jarl G. Taxerås Flaten, and Egbert Rijke. Central H-spaces and banded types, 2023. URL:
  2. J. Daniel Christensen and Jarl G. Taxerås Flaten. Ext groups in homotopy type theory, 2023. URL:
  3. Coq-HoTT. The Coq-HoTT library. URL:
  4. René Guitart and Luc Van den Bril. Calcul des satellites et présentations des bimodules à l'aide des carrés exacts. Cahiers de Topologie et Géométrie Différentielle Catégoriques, 24(3):299-330, 1983. URL:
  5. René Guitart and Luc Van den Bril. Calcul des satellites et présentations des bimodules à l'aide des carrés exacts (2e partie). Cahiers de Topologie et Géométrie Différentielle Catégoriques, 24(4):333-369, 1983. URL:
  6. Saunders Mac Lane. Homology. Springer, 1963. Google Scholar
  7. Barry Mitchell. Theory of categories. Academic Press, 1965. Google Scholar
  8. Vladimir S. Retakh. Homotopic properties of categories of extensions. Russian Mathematical Surveys, 41(6):217-218, December 1986. URL:
  9. Egbert Rijke. Introduction to Homotopy Type Theory. Cambridge University Press, 2023. To appear. Google Scholar
  10. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics., Institute for Advanced Study, 2013.
  11. Floris van Doorn. On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory. PhD thesis, Carnegie Mellon University, 2018. URL:
  12. Nobuo Yoneda. On the homology theory of modules. Journal of the Faculty of Science, the University of Tokyo Section I, 7:193-227, 1954. Google Scholar
  13. Nobuo Yoneda. On Ext and exact sequences. Journal of the Faculty of Science, the University of Tokyo Section I, 8:507-576, 1960. Google Scholar