English
The map formula for yonedaPairing: (yonedaPairing C).map α β = yoneda.map α.fst.unop ≫ β ≫ α.snd.
Русский
Формула отображения для yonedaPairing: (yonedaPairing C).map α β = yoneda.map α.fst.unop ≫ β ≫ α.snd.
LaTeX
$$$ (\mathrm{yonedaPairing}\; C).map \alpha \beta = \yoneda.map \alpha.1.unop \gg \beta \gg \alpha.2 $$$
Lean4
/-- We have a type-level equivalence between natural transformations from the coyoneda embedding
and elements of `F.obj X.unop`, without any universe switching.
-/
def coyonedaEquiv {X : C} {F : C ⥤ Type v₁} : (coyoneda.obj (op X) ⟶ F) ≃ F.obj X
where
toFun η := η.app X (𝟙 X)
invFun ξ := { app := fun _ x ↦ F.map x ξ }
left_inv := fun η ↦ by
ext Y (x : X ⟶ Y)
dsimp
rw [← FunctorToTypes.naturality]
simp
right_inv := by intro ξ; simp
