largeCurriedCoyonedaLemma — Mathlib

Lean4

/-- The curried version of the Coyoneda lemma. -/
def largeCurriedCoyonedaLemma {C : Type u₁} [Category.{v₁} C] :
    (coyoneda.rightOp ⋙ coyoneda) ≅ evaluation C (Type v₁) ⋙ (whiskeringRight _ _ _).obj uliftFunctor.{u₁} :=
  NatIso.ofComponents
    (fun X =>
      NatIso.ofComponents (fun _ => Equiv.toIso <| coyonedaEquiv.trans Equiv.ulift.symm)
        (by
          intro Y Z f
          ext g
          rw [← ULift.down_inj]
          simpa using coyonedaEquiv_comp _ _))
    (by
      intro Y Z f
      ext F g
      rw [← ULift.down_inj]
      simpa using (coyonedaEquiv_naturality _ _).symm)

Похожие утверждения