Definition rig_univalence_weq3 (X Y : rig) : (rigiso' X Y) ≃ (rigiso X Y). Proof. use make_weq. - intros i'. use make_rigiso. + exact (pr1 (pr1 i')). + use make_isrigfun. * use make_ismonoidfun. -- use make_isbinopfun. exact (dirprod_pr1 (pr2 (pr1 i'))). -- exact (dirprod_pr1 (pr2 i')). * use make_ismonoidfun. -- use make_isbinopfun. exact (dirprod_pr2 (pr2 (pr1 i'))). -- exact (dirprod_pr2 (pr2 i')). - use isweq_iso. + intros i. use make_rigiso'. * exact (pr1rigiso _ _ i). * use make_istwobinopfun. -- exact (ismonoidfunisbinopfun (isrigfunisaddmonoidfun (rigisoisrigfun i))). -- exact (ismonoidfunisbinopfun (isrigfunismultmonoidfun (rigisoisrigfun i))). * exact (ismonoidfununel (isrigfunisaddmonoidfun (rigisoisrigfun i))). * exact (ismonoidfununel (isrigfunismultmonoidfun (rigisoisrigfun i))). + intros x. use idpath. + intros x. use idpath. Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.