Lemma isbinopeqrel_subgr_eqrel {A : abgr} (B : @subabgr A) : isbinophrel (make_eqrel (subgrhrel B) (iseqrel_subgrhrel A B)). Proof. use isbinophrelif. - apply (pr2 (pr2 A)). - intros a b c X. cbn in *. unfold ishinh_UU in *. use (squash_to_prop X (propproperty _)). intros X''. use hinhpr. use tpair. + exact (pr1 X''). + cbn. set (tmp := pr2 X''). cbn in tmp. rewrite tmp. clear tmp. clear X''. rewrite grinvop. rewrite (commax A c). rewrite (assocax A). rewrite (commax A c). rewrite (assocax A). rewrite grlinvax. rewrite runax. 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.