∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F)
  (i : F.I₀), CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (e.inv.h₀ i)) (F.f i) = E.f (e.inv.s₀ i)