English
Let C be a category, A a presheaf on C, and F a presheaf over CostructuredArrow yoneda A. Given morphism f: X → Y in C, and compatible arrows s: yoneda.obj X ⟶ A and t: yoneda.obj Y ⟶ A with yoneda.map f ≫ t = s, and given u ∈ F.obj(op Y) together with a witness h that u forms an OverArrow with respect to η and t, there exists a corresponding OverArrow with respect to s using F.map f.op on u; that is, MakesOverArrow η s (F.map f.op u) exists whenever h is given.
Русский
Пусть C — категория, A — предшествование на C, и F — предшествование над CostructuredArrow yoneda A. Пусть f: X → Y и пары стрел s: yoneda.obj X ⟶ A, t: yoneda.obj Y ⟶ A удовлетворяют yoneda.map f ≫ t = s. Для произвольного u ∈ F.obj(op Y) с доказательством h, что существует надстрелка (OverArrow) η t u, тогда существует соответствующая надстрелка η s (F.map f.op u).
LaTeX
$$$\\forall {F : C^{\\mathrm{op}} \\to \\mathrm{Type}_v} \\; (\\eta : F ⟶ A) \\; {X,Y : C} \\; (f : X ⟶ Y) \\; {s : yoneda.obj X ⟶ A} \\; {t : yoneda.obj Y ⟶ A},\\;\n (hst : yoneda.map f ≫ t = s) \\; {u : F.obj (op Y)} \\; (h : MakesOverArrow η t u) : MakesOverArrow η s (F.map f.op u) $$$
Lean4
/-- "Functoriality of `MakesOverArrow η s` in `s`. -/
theorem map₂ {F : Cᵒᵖ ⥤ Type v} {η : F ⟶ A} {X Y : C} (f : X ⟶ Y) {s : yoneda.obj X ⟶ A} {t : yoneda.obj Y ⟶ A}
(hst : yoneda.map f ≫ t = s) {u : F.obj (op Y)} (h : MakesOverArrow η t u) : MakesOverArrow η s (F.map f.op u) :=
⟨by rw [elementwise_of% η.naturality, h.app, yonedaEquiv_naturality, hst]⟩
