∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover)
  (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀)
  {Z : AlgebraicGeometry.Scheme} (h : 𝒰.affineRefinement.openCover.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso f 𝒰 i).inv
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰.affineRefinement.openCover f i)
        h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Cover.pullbackHom (𝒰.X i.fst).affineCover
        (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i.fst) i.snd)
      h