∀ {R : Type u} [inst : CommRing R] (toModuleCat : ModuleCat R) (form : QuadraticForm R ↑toModuleCat)
  (toModuleCat_1 : ModuleCat R) (form_1 : QuadraticForm R ↑toModuleCat_1),
  ({ toModuleCat := toModuleCat, form := form } = { toModuleCat := toModuleCat_1, form := form_1 }) =
    (toModuleCat = toModuleCat_1 ∧ form ≍ form_1)