English
Two functors from Paths V to C are equal if they agree on objects and their action on singleton path morphisms satisfies a natural compatibility condition; this is an extensionality principle for Path functors.
Русский
Два функторa Path V → C равны, если они согласованы на объектах и их действие на морфизмы одиночного пути удовлетворяет естественному совместному условию; это принцип экстенсивности для функторов Path.
LaTeX
$$$\forall F,G: Paths V ⥤ C,\; F.obj = G.obj \\land \; \forall a,b,e,\; F.map e^{toPath} = eqToHom (congr_fun h_obj a) \; \Rightarrow \; G.map e^{toPath}$$$
Lean4
/-- Two functors out of a path category are equal when they agree on singleton paths. -/
@[ext (iff := false)]
theorem ext_functor {C} [Category C] {F G : Paths V ⥤ C} (h_obj : F.obj = G.obj)
(h :
∀ (a b : V) (e : a ⟶ b),
F.map e.toPath = eqToHom (congr_fun h_obj a) ≫ G.map e.toPath ≫ eqToHom (congr_fun h_obj.symm b)) :
F = G := by
fapply Functor.ext
· intro X
rw [h_obj]
· intro X Y f
induction f with
| nil => erw [F.map_id, G.map_id, Category.id_comp, eqToHom_trans, eqToHom_refl]
| cons g e ih =>
erw [F.map_comp g (Quiver.Hom.toPath e), G.map_comp g (Quiver.Hom.toPath e), ih, h]
simp only [Category.id_comp, eqToHom_refl, eqToHom_trans_assoc, Category.assoc]
