Definition commring_univalence_map (X Y : commring) : (X = Y) → (ringiso X Y). Proof. intros e. induction e. exact (idrigiso X). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.