∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f g : X ⟶ Y) (s : CategoryTheory.Limits.Cofork f g),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom f)
      (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom s.π) =
    AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom (CategoryTheory.CategoryStruct.comp g s.π)