We develop the theory of Yoneda Ext groups over a ring in homotopy type theory (HoTT) and describe their interpretation into an $\infty$-topos. This is an abstract approach to Ext groups which does not require projective or injective resolutions. While it produces group objects that are a priori large, we show that the $\operatorname{Ext}^1$ groups are equivalent to small groups, leaving open the question of whether the higher Ext groups are essentially small as well. We also show that the $\operatorname{Ext}^1$ groups take on the usual form as a product of cyclic groups whenever the input modules are finitely presented and the ring is a PID (in the constructive sense). When interpreted into an $\infty$-topos of sheaves on a 1-category, our Ext groups recover (and give a resolution-free approach to) sheaf Ext groups, which arise in algebraic geometry. (These are also called "local" Ext groups.) We may therefore interpret results about Ext from HoTT and apply them to sheaf Ext. To show this, we prove that injectivity of modules in HoTT interprets to internal injectivity in these models. It follows, for example, that sheaf Ext can be computed using resolutions which are projective or injective in the sense of HoTT, when they exist, and we give an example of this in the projective case. We also discuss the relation between internal $\mathbb{Z} G$-modules (for a $0$-truncated group object $G$) and abelian groups in the slice over $BG$, and study the interpretation of our Ext groups in both settings.

翻译：我们发展了同伦类型论（HoTT）中环上Yoneda Ext群的理论，并描述了它们到∞-拓扑斯中的解释。这是一种抽象的对Ext群的处理方式，不需要投射或内射分解。虽然它产生的是先验的大群对象，但我们证明了Ext^1群等价于小群，而更高阶Ext群是否本质上是小群的问题仍未解决。我们还证明了，当输入模是有限表示的且环是（构造意义下的）主理想整环时，Ext^1群呈现出通常的形式——即循环群的直积。当解释到1-范畴上的层∞-拓扑斯中时，我们的Ext群恢复（并提供了无需分解的方法）了代数几何中出现的层Ext群（也称为“局部”Ext群）。因此，我们可以解释HoTT中关于Ext的结果并将其应用于层Ext。为证明这一点，我们证明了HoTT中模的内射性在这些模型中解释为内部内射性。由此可得，例如，当存在HoTT意义上的投射或内射分解时，层Ext可用此类分解计算，我们在投射情形给出了一个例子。我们还讨论了（对于0-截断群对象G）内部Z G-模与BG切片范畴中阿贝尔群之间的关系，并研究了我们的Ext群在这两种背景下的解释。