∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R) {U V W : Cᵒᵖ} (i : U ⟶ V) (j : V ⟶ W) (x : ↑(M.obj U)),
  (CategoryTheory.ConcreteCategory.hom (M.map (CategoryTheory.CategoryStruct.comp i j))) x =
    (CategoryTheory.ConcreteCategory.hom (M.map j)) ((CategoryTheory.ConcreteCategory.hom (M.map i)) x)