proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels