∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.prod.leftUnitorEquivalence C =
    { functor := CategoryTheory.prod.leftUnitor C, inverse := CategoryTheory.prod.leftInverseUnitor C,
      unitIso := CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Discrete PUnit.{w + 1} × C)),
      counitIso :=
        CategoryTheory.Iso.refl ((CategoryTheory.prod.leftInverseUnitor C).comp (CategoryTheory.prod.leftUnitor C)),
      functor_unitIso_comp := ⋯ }