proposition: Lemma isapropinvstruct {X : hSet} {opp : binop X} (is : ismonoidop opp) : isaprop (invstruct opp is).
proof: Proof. apply isofhlevelsn. intro is0. set (un0 := pr1 (pr2 is)). assert (int : ∏ (i : X -> X), isaprop (dirprod (∏ x : X, paths (opp (i x) x) un0) (∏ x : X, paths (opp x (i x)) un0))). { intro i. apply (isofhleveldirprod 1). - apply impred. intro x. simpl. apply (setproperty X). - apply impred. intro x. simpl. apply (setproperty X). } apply (isapropsubtype (λ i : _, make_hProp _ (int i))). intros inv1 inv2. simpl. intro ax1. intro ax2. apply funextfun. intro x0. apply (invmaponpathsweq (make_weq _ (isweqrmultingr_is (tpair _ is is0) x0))). simpl. rewrite (pr1 ax1 x0). rewrite (pr1 ax2 x0). apply idpath. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions