English
A general variant of naturality for yonedaEquiv with general g.
Русский
Обобщённая вариация естественности для yonedaEquiv с общим g.
LaTeX
$$$ yonedaEquiv_naturality' \\{X Y : C^{op}\\} \\; {F : C^{op} ⥤ Type v} \\; (f : yoneda.obj (unop X) ⟶ F) (g : X ⟶ Y) : F.map g (yonedaEquiv f) = yonedaEquiv (yoneda.map g.unop ≫ f) $$$
Lean4
/-- Variant of `yonedaEquiv_naturality` with general `g`. This is technically strictly more general
than `yonedaEquiv_naturality`, but `yonedaEquiv_naturality` is sometimes preferable because it
can avoid the "motive is not type correct" error. -/
theorem yonedaEquiv_naturality' {X Y : Cᵒᵖ} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda.obj (unop X) ⟶ F) (g : X ⟶ Y) :
F.map g (yonedaEquiv f) = yonedaEquiv (yoneda.map g.unop ≫ f) :=
yonedaEquiv_naturality _ _
