Small sets in the category of structured arrows

Here we prove a technical result about small sets in the category of structured arrows that will be used in the proof of the Special Adjoint Functor Theorem.

instance CategoryTheory.StructuredArrow.small_proj_preimage_of_locallySmall {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {𝒢 : Set C} [Small.{v₁, u₁} ↑𝒢] [CategoryTheory.LocallySmall.{v₁, v₂, u₂} D] : Small.{v₁, max u₁ v₂} ↑((CategoryTheory.StructuredArrow.proj S T).obj ⁻¹' 𝒢)

Equations

• ⋯ = ⋯

instance CategoryTheory.CostructuredArrow.small_proj_preimage_of_locallySmall {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor C D} {T : D} {𝒢 : Set C} [Small.{v₁, u₁} ↑𝒢] [CategoryTheory.LocallySmall.{v₁, v₂, u₂} D] : Small.{v₁, max u₁ v₂} ↑((CategoryTheory.CostructuredArrow.proj S T).obj ⁻¹' 𝒢)

Equations

• ⋯ = ⋯