∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.Comon.Comon_EquivMon_OpOp C).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Comon C)).obj x)) ⋯