Definition rig_univalence_weq1 (X Y : rig) : (X = Y) ≃ (X ╝ Y) := total2_paths_equiv _ _ _.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.