∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.MonoidalOpposite.mopMopEquivalence C =
    (CategoryTheory.MonoidalOpposite.unmopEquiv Cᴹᵒᵖ).trans (CategoryTheory.MonoidalOpposite.unmopEquiv C)