{X Y Z : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    (g : Y ⟶ Z) →
      (AlgebraicGeometry.Scheme.Modules.pullback g).comp (AlgebraicGeometry.Scheme.Modules.pullback f) ≅
        AlgebraicGeometry.Scheme.Modules.pullback (CategoryTheory.CategoryStruct.comp f g)