fact: Definition BuildOperations (T : Type) `{Plus T} `{Mult T} `{Zero T} `{One T} `{Negate T} : Operations := exist _ T (plus,mult,zero,one,negate).
imports: HoTT.Types.Arrow HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.rings