English
We have a type-level equivalence between natural transformations from the Yoneda embedding and elements of F.obj(op X).
Русский
У нас есть эквивалентность типов между натуральными преобразованиями от внедрения Ёнеды и элементами F.obj(op X).
LaTeX
$$$ yonedaEquiv \\{ X \\} : (yoneda.obj X \\to F) \\simeq F.obj(\\operatorname{op} X) $$$
Lean4
/-- We have a type-level equivalence between natural transformations from the yoneda embedding
and elements of `F.obj X`, without any universe switching.
-/
def yonedaEquiv {X : C} {F : Cᵒᵖ ⥤ Type v₁} : (yoneda.obj X ⟶ F) ≃ F.obj (op X)
where
toFun η := η.app (op X) (𝟙 X)
invFun ξ := { app := fun _ f ↦ F.map f.op ξ }
left_inv := by
intro η
ext Y f
dsimp
rw [← FunctorToTypes.naturality]
simp
right_inv := by intro ξ; simp
