no goals
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i✝ j✝ k✝ : J
s : Set (F.obj i✝)
inst✝ : IsCofilteredOrEmpty J
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
i j : J
f g : i ⟶ j
k : J
φ : k ⟶ i
hφ : φ ≫ f = φ ≫ g
⊢ (fun g => g ∘ F.map φ) (F.map f) = (fun g => g ∘ F.map φ) (F.map g)
simp_rw [← types_comp, ← F.map_comp, hφ]