∀ {R : Type u} [inst : CommRing R] [inst_1 : Invertible 2] (X Y Z : QuadraticModuleCat R),
  (CategoryTheory.forget₂ (QuadraticModuleCat R) (ModuleCat R)).map
      (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv =
    (CategoryTheory.MonoidalCategoryStruct.associator X.toModuleCat Y.toModuleCat Z.toModuleCat).inv