∀ {R : Type u} [inst : CommRing R] {M N U : QuadraticModuleCat R} (f : M ⟶ N) (g : N ⟶ U),
  QuadraticModuleCat.Hom.toIsometry (CategoryTheory.CategoryStruct.comp f g) =
    (QuadraticModuleCat.Hom.toIsometry g).comp (QuadraticModuleCat.Hom.toIsometry f)