Definition rigfuncomp {X Y Z : rig} (f : rigfun X Y) (g : rigfun Y Z) : rigfun X Z. Proof. use rigfunconstr. - exact (g ∘ f). - use make_isrigfun. + exact (pr2 (monoidfuncomp (rigaddfun f) (rigaddfun g))). + exact (pr2 (monoidfuncomp (rigmultfun f) (rigmultfun g))). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.