∀ {X Y : AlgebraicGeometry.Scheme} {domain : X.Opens} {dense_domain : Dense ↑domain} {hom : ↑domain ⟶ Y}
  {domain_1 : X.Opens} {dense_domain_1 : Dense ↑domain_1} {hom_1 : ↑domain_1 ⟶ Y},
  { domain := domain, dense_domain := dense_domain, hom := hom } =
      { domain := domain_1, dense_domain := dense_domain_1, hom := hom_1 } →
    domain = domain_1 ∧ hom ≍ hom_1