{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} →
          {f g : E.Hom F} → [SizeOf C] → CategoryTheory.PreOneHypercover.Homotopy f g → ℕ