English
There is a canonical isomorphism between YonedaCollection (restrictedYonedaObj η) X and F.obj (op X) given by unitForward and unitBackward, with the two compositions equal to the identity.
Русский
Существует каноническое изоморфирование между YonedaCollection (restrictedYonedaObj η) X и F.obj (op X), задаваемое unitForward и unitBackward, при котором составы дают тождественный морфизм.
LaTeX
$$$$ \text{unitForward}_\eta X : \operatorname{YonedaCollection}(\operatorname{restrictedYonedaObj}\eta)X \to F(\operatorname{op}X), \\ \text{unitBackward}_\eta X : F(\operatorname{op}X) \to \operatorname{YonedaCollection}(\operatorname{restrictedYonedaObj}\eta)X $$$$
Lean4
theorem unitBackward_unitForward {F : Cᵒᵖ ⥤ Type v} (η : F ⟶ A) (X : C) : unitBackward η X ∘ unitForward η X = id :=
by
refine funext fun p => YonedaCollection.ext ?_ (OverArrows.ext ?_)
· simpa [unitForward, unitBackward] using congrArg yonedaEquiv.symm p.snd.app_val
· simp [unitForward, unitBackward]
