{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.Limits.HasFiniteProducts C} →
      {inst_2 : CategoryTheory.Limits.HasPullbacks C} → {X Y : CategoryTheory.Dial C} → [SizeOf C] → X.Hom Y → ℕ