∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Functor.equiv.unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Discrete.natIso fun x_1 =>
          CategoryTheory.Iso.refl
            (((CategoryTheory.Functor.id (CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{w + 1}) C)).obj x).obj
              x_1))
      ⋯