proposition: Lemma isapropisrigfun {X Y : rig} (f : X -> Y) : isaprop (isrigfun f).
proof: Proof. use isapropdirprod. - use isapropismonoidfun. - use isapropismonoidfun. Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids