C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
S : C ⥤ D
T : D
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : CostructuredArrow S T
f g : X ⟶ Y
hfg : ∀ (G : CostructuredArrow S T), G ∈ (proj S T).toPrefunctor.obj ⁻¹' 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : C
hG : G ∈ 𝒢
h : G ⟶ X.left
⊢ h ≫ f.left = h ≫ g.left
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
S : C ⥤ D
T : D
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
⊢ IsSeparating ((proj S T).toPrefunctor.obj ⁻¹' 𝒢)
refine' fun X Y f g hfg => ext _ _ (h𝒢 _ _ fun G hG h => _)
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
S : C ⥤ D
T : D
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : CostructuredArrow S T
f g : X ⟶ Y
hfg : ∀ (G : CostructuredArrow S T), G ∈ (proj S T).toPrefunctor.obj ⁻¹' 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : C
hG : G ∈ 𝒢
h : G ⟶ X.left
⊢ h ≫ f.left = h ≫ g.left
exact congr_arg CommaMorphism.left (hfg (mk (S.map h ≫ X.hom)) hG (homMk h rfl))