equivalence₂UnitIso — Mathlib

Lean4
/-- The unit isomorphism of the equivalence `equivalence₂` between `A` and `B`. -/
@[simps!]
def equivalence₂UnitIso : 𝟭 A ≅ (F ⋙ eB.inverse) ⋙ eB.functor ⋙ e'.inverse ⋙ eA.inverse :=
  calc
    𝟭 A ≅ F ⋙ e'.inverse ⋙ eA.inverse := equivalence₁UnitIso hF
    _ ≅ F ⋙ 𝟭 B' ⋙ e'.inverse ⋙ eA.inverse := (isoWhiskerLeft _ (leftUnitor _).symm)
    _ ≅ F ⋙ (eB.inverse ⋙ eB.functor) ⋙ e'.inverse ⋙ eA.inverse :=
      (isoWhiskerLeft _ (isoWhiskerRight eB.counitIso.symm _))
    _ ≅ (F ⋙ eB.inverse ⋙ eB.functor) ⋙ e'.inverse ⋙ eA.inverse := (associator _ _ _).symm
    _ ≅ ((F ⋙ eB.inverse) ⋙ eB.functor) ⋙ e'.inverse ⋙ eA.inverse := (isoWhiskerRight (associator _ _ _).symm _)
    _ ≅ (F ⋙ eB.inverse) ⋙ eB.functor ⋙ e'.inverse ⋙ eA.inverse := associator _ _ _
Похожие утверждения