∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C),
  (CategoryTheory.Dial.tensorUnitImpl.tensorObjImpl X).rel =
    (CategoryTheory.Subobject.pullback
          (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.leftUnitor X.src).hom
            (CategoryTheory.Limits.prod.leftUnitor X.tgt).hom)).obj
      X.rel