∀ {R : Type u} [inst : CommRing R] {S : Type u} [inst_1 : CommRing S] (f : R →+* S)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) {Z : CommRingCat}
  (h :
    {
        carrier :=
          ↑((AlgebraicGeometry.Spec.structureSheaf S).val.obj
              (Opposite.op
                ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U))),
        commRing :=
          ((AlgebraicGeometry.Spec.structureSheaf S).val.obj
              (Opposite.op
                ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ })
                  U))).commRing } ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom (algebraMap R ↑((AlgebraicGeometry.Spec.structureSheaf R).val.obj (Opposite.op U))))
      (CategoryTheory.CategoryStruct.comp
        (CommRingCat.ofHom
          (AlgebraicGeometry.StructureSheaf.comap f U
            ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U) ⋯))
        h) =
    CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom f)
      (CategoryTheory.CategoryStruct.comp
        (CommRingCat.ofHom
          (algebraMap S
            ↑((AlgebraicGeometry.Spec.structureSheaf S).val.obj
                (Opposite.op
                  ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U)))))
        h)