∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T),
  (CategoryTheory.Over.opEquivOpUnder X).counitIso =
    CategoryTheory.Iso.refl
      ({ obj := fun Y => CategoryTheory.Over.mk (Opposite.unop Y).hom.op,
            map := fun {Z Y} f => CategoryTheory.Over.homMk f.unop.right.op ⋯, map_id := ⋯, map_comp := ⋯ }.comp
        { obj := fun Y => Opposite.op (CategoryTheory.Under.mk Y.hom.unop),
          map := fun {Z Y} f => Opposite.op (CategoryTheory.Under.homMk f.left.unop ⋯), map_id := ⋯, map_comp := ⋯ })