Lemma rig_univalence_isweq (X Y : rig) : isweq (rig_univlalence_map X Y). 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. refine (weqcomp_to_funcomp_app @ _). exact weqcomp_to_funcomp_app. - use weqproperty. Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.