∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X),
  (CategoryTheory.Over.equivalenceOfIsTerminal hX).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Iso.refl
          (({ obj := fun Y => CategoryTheory.Over.mk (hX.from Y), map := fun {X_1 Y} f => CategoryTheory.Over.homMk f ⋯,
                    map_id := ⋯, map_comp := ⋯ }.comp
                (CategoryTheory.Over.forget X)).obj
            x))
      ⋯