Lemma Quotcategory_comp_iscontr_PAS {A B C : PA} {t : pr1 (PAS A B)} {t' : pr1 (PAS B C)} {f1 f'1 : PA⟦A, B⟧} {g1 g'1 : PA⟦B, C⟧} (p : pr1 t = to_binop A B f'1 (grinv (to_abgr A B) f1)) (p' : pr1 t' = to_binop B C g'1 (grinv (to_abgr B C) g1)) : pr1 (PAS A C) (to_binop A C (f1 · g1) (grinv (to_abgr A C) (f'1 · g'1))). Proof. set (e1 := Quotcategory_comp_iscontr_PAS_eq p). set (e2 := Quotcategory_comp_iscontr_PAS_eq p'). rewrite e1. rewrite e2. clear e1 e2 p p'. cbn. rewrite to_premor_linear'. rewrite to_postmor_linear'. rewrite to_postmor_linear'. set (ac := assocax (to_abgr A C)). unfold isassoc in ac. cbn in ac. set (comm := commax (to_abgr A C)). unfold iscomm in comm. cbn in comm. rewrite (comm _ (f1 · g1)). rewrite <- (ac _ (f1 · g1) _). rewrite (comm _ (f1 · g1)). rewrite ac. rewrite ac. set (i := grinvop (to_abgr A C)). cbn in i. rewrite i. repeat rewrite <- ac. rewrite comm. rewrite <- ac. set (il := linvax _ (f1 · g1)). unfold to_inv in il. rewrite il. clear il. set (lu := to_lunax A C). unfold islunit in lu. cbn in lu. unfold to_unel. rewrite lu. set (tmp := pr2 (pr2 (PAS A C))). cbn in tmp. apply tmp. clear tmp. use to_op_elem. - use to_op_elem. + apply (dirprod_pr1 (PAC A B) C (pr1 t) (pr2 t) (pr1 t')). + apply (dirprod_pr2 (PAC A B) C f1 (pr1 t') (pr2 t')). - apply (dirprod_pr1 (PAC A B) C (pr1 t) (pr2 t) g1). 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.