Lemma isinvoncarrier {X : gr} (A : subgr X) : isinv (@op A) (unel A) (λ a : A, make_carrier _ ((pr1 a)^-1) (pr2 (pr2 A) (pr1 a) (pr2 a))). Proof. split. - intro a. apply (invmaponpathsincl _ (isinclpr1carrier A)). simpl. apply (grlinvax X (pr1 a)). - intro a. apply (invmaponpathsincl _ (isinclpr1carrier A)). simpl. apply (grrinvax X (pr1 a)). Defined.
Require Import UniMath.MoreFoundations.Subtypes.