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

instance CategoryTheory.MorphismProperty.isSmall_iSup {C : Type u} [Category.{v, u} C] {α : Type u_1} (W : α → MorphismProperty C) [Small.{w, u_1} α] [∀ (a : α), IsSmall.{w, v, u} (W a)] : IsSmall.{w, v, u} (iSup W)

instance CategoryTheory.MorphismProperty.instIsSmallISupOfSmall {C : Type u} [Category.{v, u} C] {α : Type t} [Small.{w, t} α] (W : α → MorphismProperty C) [∀ (i : α), IsSmall.{w, v, u} (W i)] : IsSmall.{w, v, u} (⨆ (i : α), W i)