∀ {I : Type u_1} [inst : CategoryTheory.Category.{u_1, u_1} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (i : I) (U : (D.obj i).Opens) ⦃X Y : CategoryTheory.Over i⦄ (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.opensDiagram D i U).map f)
      ((TopologicalSpace.Opens.map (D.map Y.hom).base).obj U).ι =
    CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map (D.map X.hom).base).obj U).ι
      (((CategoryTheory.Over.forget i).comp D).map f)