English
Two enriched functors F and G are equal if they agree on objects and on maps (after transporting along object equality).
Русский
Два обогащённого функторa F и G равны, если совпадают их отображения на объектов и на стрелы (после переноса по равенству объектов).
LaTeX
$$$\\forall X: C, F(X) = G(X) \\quad\\text{and}\\quad \\forall X,Y: C, F(X\\to Y) = G(X\\to Y) \\implies F = G$$$
Lean4
theorem ext {C : Type u₁} {D : Type u₂} [EnrichedCategory V C] [EnrichedCategory V D] {F G : EnrichedFunctor V C D}
(h_obj : ∀ X, F.obj X = G.obj X) (h_map : ∀ (X Y : C), F.map X Y ≫ eqToHom (by rw [h_obj, h_obj]) = G.map X Y) :
F = G := by
match F, G with
| mk F_obj F_map _ _,
mk G_obj G_map _ _ =>
obtain rfl : F_obj = G_obj := funext fun X ↦ h_obj X
congr
ext X Y
simpa using h_map X Y
