fact: Definition isrigfun {X Y : rig} (f : X -> Y) : UU := dirprod (@ismonoidfun (rigaddabmonoid X) (rigaddabmonoid Y) f) (@ismonoidfun (rigmultmonoid X) (rigmultmonoid Y) f).
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids