Lemma isapropinvstruct {X : hSet} {opp : binop X} (is : ismonoidop opp) : isaprop (invstruct opp is). Proof. apply isofhlevelsn. intro is0. set (un0 := pr1 (pr2 is)). assert (int : ∏ (i : X → X), isaprop ((∏ x : X, opp (i x) x = un0) × (∏ x : X, 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 (is ,, is0) x0))). simpl. rewrite (pr1 ax1 x0). rewrite (pr1 ax2 x0). apply idpath. Defined.