Lemma Quotcategory_isZero : isZero (C:=Quotcategory) Z. Proof. use make_isZero. - intros a. use tpair. + exact (to_quot_mor (@ZeroArrowFrom PA Z a)). + cbn beta. intros t. set (t'1 := @issurjsetquotpr (to_abgr Z a) (binopeqrel_subgr_eqrel (PAS Z a)) t). use (squash_to_prop t'1). apply has_homsets_Quotcategory. intros t1. clear t'1. induction t1 as [t1 t2]. rewrite <- t2. unfold to_quot_mor. apply maponpaths. apply ArrowsFromZero. - intros a. use tpair. + exact (to_quot_mor (@ZeroArrowTo PA Z a)). + cbn beta. intros t. set (t'1 := @issurjsetquotpr (to_abgr a Z) (binopeqrel_subgr_eqrel (PAS a Z)) t). use (squash_to_prop t'1). apply has_homsets_Quotcategory. intros t1. clear t'1. induction t1 as [t1 t2]. rewrite <- t2. unfold to_quot_mor. apply maponpaths. apply ArrowsToZero. 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.