∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (F : CategoryTheory.Functor Cᵒᵖ (Type u)) (G : PresheafOfModules R),
  (PresheafOfModules.freeAdjunction R).homEquiv F G = PresheafOfModules.freeHomEquiv