Ext in Grothendieck abelian categories

Let C : Type u be an abelian category (with Category.{v} C). If C is a Grothendieck abelian category relatively to a universe w, the morphisms in C must be w-small, and as C has enough injectives, the Ext-groups are also w-small. If C is a nonzero category, it is possible to show that any w-small type T injects in a type of morphisms in C (consider the various inclusions X ⟶ ∐ (fun (_ : T) ↦ X) for a nonzero object X : C). It follows that it is reasonable to think that the universe w is unique, and is the best choice for the universe where the Ext-groups in C shall be defined.

In this situation, we make HasExt.{w} C an instance. As result, when X and Y are objects in C and n : ℕ, we have Ext X Y n : Type w.

instance CategoryTheory.IsGrothendieckAbelian.hasExt (C : Type u) [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{w, v, u} C] : HasExt C