∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover)
  (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀),
  CategoryTheory.CategoryStruct.comp (((fun i => ((fun j => (𝒰.X j).affineCover) i).toPreZeroHypercover) i.fst).f i.snd)
      (CategoryTheory.CategoryStruct.id (𝒰.X i.fst)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (𝒰.affineRefinement.openCover.X i))
      ((𝒰.X i.fst).affineCover.f i.snd)