Lemma isapropmultinvpair ( X : commring ) ( a : X ) : isaprop ( multinvpair X a ). Proof. intros. unfold isaprop. intros b c. assert ( b = c ) as f. { destruct b as [ b b' ]. destruct c as [ c c']. assert ( b = c ) as f0. { rewrite <- ( @ringrunax2 X b ). change ( b * @ringunel2 X ) with ( b * 1 )%multmonoid. rewrite <- ( pr2 c' ). change ( ( b * ( a * c ) )%ring = c ). rewrite <- ( ringassoc2 X ). change ( b * a )%ring with ( b * a )%multmonoid. rewrite ( pr1 b' ). change ( ( @ringunel2 X ) * c = c )%ring. apply ringlunax2. } apply (total2_paths2_f f0 ). assert ( isaprop ( c * a = ( @ringunel2 X ) × a * c = ( @ringunel2 X ) ) ) as is. { apply isofhleveldirprod. - apply ( setproperty X ). - apply ( setproperty X ). } apply is. } split with f. intros g. assert ( isaset ( multinvpair X a ) ) as is. { unfold multinvpair. unfold invpair. change isaset with ( isofhlevel 2 ). apply isofhleveltotal2. - apply ( pr2 ( pr1 ( pr1 ( rigmultmonoid X ) ) ) ). - intros. apply isofhleveldirprod. + apply hlevelntosn. apply ( setproperty X ). + apply hlevelntosn. apply (setproperty X ). } apply is. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Algebra.Monoids.