proposition: Lemma is_precategory_Quotcategory_data : is_precategory Quotcategory_data.
proof: 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.
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