Small classes of morphisms

A class of morphisms W : MorphismProperty C is w-small if the corresponding set in Set (Arrow C) is.

class CategoryTheory.MorphismProperty.IsSmall {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : Prop

A class of morphisms W : MorphismProperty C is w-small if the corresponding set in Set (Arrow C) is.

• small_toSet : Small.{w, max u v} ↑W.toSet

instance CategoryTheory.MorphismProperty.isSmall_ofHoms {C : Type u} [Category.{v, u} C] {ι : Type t} [Small.{w, t} ι] {A B : ι → C} (f : (i : ι) → A i ⟶ B i) : IsSmall.{w, v, u} (ofHoms f)

theorem CategoryTheory.MorphismProperty.isSmall_iff_eq_ofHoms {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : IsSmall.{w, v, u} W ↔ ∃ (ι : Type w) (A : ι → C) (B : ι → C) (f : (i : ι) → A i ⟶ B i), W = ofHoms f