∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat) {X Y Z : SheafOfModules R} (f : X ⟶ Y) (g : Y ⟶ Z),
  {
      val :=
        ((SheafOfModules.forget R).comp (PresheafOfModules.toPresheaf R.val)).map
          (CategoryTheory.CategoryStruct.comp f g) } =
    CategoryTheory.CategoryStruct.comp
      { val := ((SheafOfModules.forget R).comp (PresheafOfModules.toPresheaf R.val)).map f }
      { val := ((SheafOfModules.forget R).comp (PresheafOfModules.toPresheaf R.val)).map g }