Ext groups are fundamental objects from homological algebra which underlie important computations in homotopy theory. We formalise the theory of Yoneda Ext groups 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.

翻译：Ext群是同调代数中的基本对象，支撑着同伦理论中的重要计算。我们使用Coq-HoTT库在同伦类型论（HoTT）中形式化了Yoneda Ext群的理论。这是一种不需要射影或内射分解的Ext处理方法，尽管它会产生较大的阿贝尔群。利用单值性，我们展示了这些Ext群如何在HoTT中被自然地表示。通过1-型（或群胚）的纤维序列，我们给出了通常的六项正合序列的新颖证明与形式化，并附带了应用。此外，我们讨论了Ext的反变长正合序列的形式化——这是一个重要的计算工具。在此过程中，我们实现并解释了扩张的Baer和以及Ext如何作为双函子的性质。