Lemma is_precategory_Quotcategory_data : is_precategory Quotcategory_data. Proof. split. - split. + intros a b f. apply pathsinv0. cbn. unfold Quotcategory_comp. set (f'' := @issurjsetquotpr (to_abgr a b) (binopeqrel_subgr_eqrel (PAS a b)) f). use (squash_to_prop f''). apply isasetsetquot. intros f'. clear f''. induction f' as [f1 f2]. rewrite <- f2. cbn in f1, a, b. eapply pathscomp0. * apply maponpaths. exact (! (id_left f1)). * apply (pr2 (pr1 (Quotcategory_comp_iscontr (setquotpr (binopeqrel_subgr_eqrel (PAS a a)) (@identity PA a)) (setquotpr (binopeqrel_subgr_eqrel (PAS a b)) f1)))). -- apply idpath. -- apply idpath. + intros a b f. apply pathsinv0. cbn. unfold Quotcategory_comp. set (f'' := @issurjsetquotpr (to_abgr a b) (binopeqrel_subgr_eqrel (PAS a b)) f). use (squash_to_prop f''). apply isasetsetquot. intros f'. clear f''. induction f' as [f1 f2]. rewrite <- f2. cbn in f1, a, b. eapply pathscomp0. * apply maponpaths. exact (! (id_right f1)). * apply (pr2 (pr1 (Quotcategory_comp_iscontr (setquotpr (binopeqrel_subgr_eqrel (PAS a b)) f1) (setquotpr (binopeqrel_subgr_eqrel (PAS b b)) (@identity PA b))))). -- apply idpath. -- apply idpath. - split. + intros a b c d f g h. cbn. set (f'' := @issurjsetquotpr (to_abgr a b) (binopeqrel_subgr_eqrel (PAS a b)) f). use (squash_to_prop f''). apply isasetsetquot. intros f'. clear f''. set (g'' := @issurjsetquotpr (to_abgr b c) (binopeqrel_subgr_eqrel (PAS b c)) g). use (squash_to_prop g''). apply isasetsetquot. intros g'. clear g''. set (h'' := @issurjsetquotpr (to_abgr c d) (binopeqrel_subgr_eqrel (PAS c d)) h). use (squash_to_prop h''). apply isasetsetquot. intros h'. clear h''. induction f' as [f1 f2]. induction g' as [g1 g2]. induction h' as [h1 h2]. cbn in f1, g1, h1. rewrite (Quot_assoc1 f g h f1 f2 g1 g2 h1 h2). rewrite <- (Quot_assoc2 f g h f1 f2 g1 g2 h1 h2). rewrite assoc. apply idpath. + intros a b c d f g h. cbn. set (f'' := @issurjsetquotpr (to_abgr a b) (binopeqrel_subgr_eqrel (PAS a b)) f). use (squash_to_prop f''). apply isasetsetquot. intros f'. clear f''. set (g'' := @issurjsetquotpr (to_abgr b c) (binopeqrel_subgr_eqrel (PAS b c)) g). use (squash_to_prop g''). apply isasetsetquot. intros g'. clear g''. set (h'' := @issurjsetquotpr (to_abgr c d) (binopeqrel_subgr_eqrel (PAS c d)) h). use (squash_to_prop h''). apply isasetsetquot. intros h'. clear h''. induction f' as [f1 f2]. induction g' as [g1 g2]. induction h' as [h1 h2]. cbn in f1, g1, h1. rewrite (Quot_assoc1 f g h f1 f2 g1 g2 h1 h2). rewrite <- (Quot_assoc2 f g h f1 f2 g1 g2 h1 h2). rewrite assoc'. apply idpath. Defined.
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.