proposition: Lemma iseqrel_subgrhrel (A : gr) (B : @subgr A) : iseqrel (subgrhrel B).
proof: Proof. unfold subgrhrel. unfold subgrhrel_hprop. use iseqrelconstr. - intros x1 x2 x3 y1 y2. cbn in *. unfold ishinh_UU in *. use (squash_to_prop y1 (propproperty _)). intros Y1. clear y1. use (squash_to_prop y2 (propproperty _)). intros Y2. clear y2. use hinhpr. induction Y1 as [t p]. induction Y2 as [t0 p0]. use tpair. + use tpair. * exact (op (pr1 t) (pr1 t0)). * exact (pr2subsetswithbinop B t t0). + cbn. rewrite p. rewrite p0. rewrite <- (assocax A). apply maponpaths_2. rewrite assocax. rewrite grlinvax. rewrite runax. apply idpath. - intros x. use hinhpr. use tpair. + exact (unel B). + cbn. apply pathsinv0. apply (grrinvax A). - intros x y. cbn. unfold ishinh_UU. intros H. use (squash_to_prop H (propproperty _)). intros H'. clear H. use hinhpr. induction H' as [t p]. use tpair. + exact (grinv B t). + cbn. rewrite p. clear p. rewrite grinvop. rewrite grinvinv. apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels