∀ (X : AlgebraicGeometry.Scheme) {X_1 Y Z : X.IdealSheafData} (f : X_1 ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.MorphismProperty.Over.homMk (AlgebraicGeometry.Scheme.IdealSheafData.inclusion ⋯) ⋯ ⋯).op.unop =
    (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MorphismProperty.Over.homMk (AlgebraicGeometry.Scheme.IdealSheafData.inclusion ⋯) ⋯ ⋯).op
        (CategoryTheory.MorphismProperty.Over.homMk (AlgebraicGeometry.Scheme.IdealSheafData.inclusion ⋯) ⋯ ⋯).op).unop