∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (S : C)
  (x x_1 : (CategoryTheory.PreZeroHypercover.singleton (CategoryTheory.CategoryStruct.id S)).I₀),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id S)
      ((CategoryTheory.PreZeroHypercover.singleton (CategoryTheory.CategoryStruct.id S)).f x) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id S)
      ((CategoryTheory.PreZeroHypercover.singleton (CategoryTheory.CategoryStruct.id S)).f x_1)