walkingParallelPairOpEquiv — Mathlib

Lean4
/-- The equivalence `WalkingParallelPair ⥤ WalkingParallelPairᵒᵖ` sending left to left and right to
right.
-/
@[simps functor inverse]
def walkingParallelPairOpEquiv : WalkingParallelPair ≌ WalkingParallelPairᵒᵖ
    where
  functor := walkingParallelPairOp
  inverse := walkingParallelPairOp.leftOp
  unitIso := NatIso.ofComponents (fun j => eqToIso (by cases j <;> rfl)) (by rintro _ _ (_ | _ | _) <;> simp)
  counitIso :=
    NatIso.ofComponents
      (fun j =>
        eqToIso
          (by
            induction j with
            | _ X
            cases X <;> rfl))
      (fun {i} {j} f =>
        by
        induction i with
        | _ i
        induction j with
        | _ j
        let g := f.unop
        have : f = g.op := rfl
        rw [this]
        cases i <;> cases j <;> cases g <;> rfl)
  functor_unitIso_comp := fun j => by cases j <;> rfl
Похожие утверждения