Lemma iseqrel_subgrhrel (A : gr) (B : @subgr A) : iseqrel (subgrhrel B). 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. rewrite <- (id_left (ZeroArrowFrom y)). set (Y := to_postmor_unel A Z (@ZeroArrowFrom A Z y)). + exact (to_quot_mor (@ZeroArrowFrom PA Z a)). apply ArrowsFromZero.