proposition: Lemma rig_univalence_isweq (X Y : rig) : isweq (rig_univlalence_map X Y).
proof: Proof. use isweqhomot. - exact (weqcomp (rig_univalence_weq1 X Y) (weqcomp (rig_univalence_weq2 X Y) (rig_univalence_weq3 X Y))). - intros e. induction e. use (pathscomp0 weqcomp_to_funcomp_app). use weqcomp_to_funcomp_app. - use weqproperty. Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids