Definition ring_univalence_weq1 : ring ≃ ring'. Proof. use make_weq. - intros R. exact (make_ring' R). - use isweq_iso. + intros R'. exact (make_ring_from_ring' R'). + intros R. use idpath. + intros R'. use total2_paths_f. * use total2_paths_f. -- use idpath. -- use proofirrelevance. use isapropisrigops. * use proofirrelevance. use isapropinvstruct. Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.