Lemma Quotcategory_comp_linear {x y z : ob PA} (f : PA⟦x, y⟧) (g : PA⟦y, z⟧) : Quotcategory_comp (to_quot_mor f) (to_quot_mor g) = to_quot_mor (f · g). Proof. unfold to_quot_mor. unfold Quotcategory_comp. apply pathsinv0. use (pr2 (pr1 (Quotcategory_comp_iscontr (setquotpr (binopeqrel_subgr_eqrel (PAS x y)) f) (setquotpr (binopeqrel_subgr_eqrel (PAS y z)) g)))). - apply idpath. - 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.