∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.SheafedSpace C} (α : X ⟶ Y)
  (β : Y ⟶ Z) (U : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace),
  (CategoryTheory.CategoryStruct.comp α β).hom.c.app (Opposite.op U) =
    CategoryTheory.CategoryStruct.comp (β.hom.c.app (Opposite.op U))
      (α.hom.c.app (Opposite.op ((TopologicalSpace.Opens.map β.hom.base).obj U)))