Lemma Quotcategory_isBinProduct (x y : A) : isBinProduct (Quotcategory_PreAdditive A PAS PAC) x y (BD x y) (to_quot_mor A PAS (to_Pr1 (BD x y))) (to_quot_mor A PAS (to_Pr2 (BD x y))). Proof. use make_isBinProduct. - intros c f g. set (f'' := @issurjsetquotpr (@to_abgr A c x) (binopeqrel_subgr_eqrel (PAS c x)) f). use (squash_to_prop f''). apply isapropiscontr. intros f'. clear f''. set (g'' := @issurjsetquotpr (@to_abgr A c y) (binopeqrel_subgr_eqrel (PAS c y)) g). use (squash_to_prop g''). apply isapropiscontr. intros g'. clear g''. induction f' as [f1 f2]. induction g' as [g1 g2]. cbn in f1, g1. use unique_exists. + exact (to_quot_mor A PAS (ToBinDirectSum (BD x y) f1 g1)). + cbn beta. split. * use (pathscomp0 (Quotcategory_comp_linear A PAS PAC _ _)). rewrite BinDirectSumPr1Commutes. exact f2. * use (pathscomp0 (Quotcategory_comp_linear A PAS PAC _ _)). rewrite BinDirectSumPr2Commutes. exact g2. + intros y0. apply isapropdirprod; apply has_homsets_Quotcategory. + intros y0 T. cbn beta in T. induction T as [T1 T2]. * set (y'' := @issurjsetquotpr (@to_abgr A c (BD x y)) (binopeqrel_subgr_eqrel (PAS c (BD x y))) y0). use (squash_to_prop y''). apply has_homsets_Quotcategory. intros y'. clear y''. induction y' as [y1 y2]. rewrite <- y2. rewrite <- y2 in T1. rewrite <- y2 in T2. cbn in y1. rewrite <- (@id_right (Quotcategory_PreAdditive A PAS PAC) _ _ (setquotpr (binopeqrel_subgr_eqrel (PAS c (BD x y))) y1)). rewrite <- (@id_right A _ _ (ToBinDirectSum (BD x y) f1 g1)). rewrite <- (to_BinOpId (BD x y)). rewrite to_premor_linear'. repeat rewrite assoc. rewrite BinDirectSumPr1Commutes. rewrite BinDirectSumPr2Commutes. rewrite <- f2 in T1. rewrite <- g2 in T2. unfold to_quot_mor. set (tmp := @setquotpr_linear A PAS PAC c (BD x y)). unfold to_quot_mor in tmp. rewrite tmp. clear tmp. set (tmp := @Quotcategory_comp_linear A PAS PAC c x (BD x y)). unfold to_quot_mor in tmp. rewrite <- tmp. clear tmp. rewrite <- T1. set (tmp := @Quotcategory_comp_linear A PAS PAC c y (BD x y)). unfold to_quot_mor in tmp. rewrite <- tmp. clear tmp. rewrite <- T2. unfold to_quot_mor. rewrite comp_eq. rewrite comp_eq. rewrite <- assoc. rewrite <- assoc. rewrite <- to_premor_linear'. repeat rewrite <- comp_eq. set (tmp := @Quotcategory_comp_linear A PAS PAC (BD x y) x (BD x y)). unfold to_quot_mor in tmp. rewrite tmp. clear tmp. set (tmp := @Quotcategory_comp_linear A PAS PAC (BD x y) y (BD x y)). unfold to_quot_mor in tmp. rewrite tmp. clear tmp. set (tmp := @setquotpr_linear A PAS PAC (BD x y) (BD x y)). unfold to_quot_mor in tmp. rewrite <- tmp. clear tmp. rewrite comp_eq. rewrite (to_BinOpId (BD x y)). rewrite comp_eq. apply cancel_precomposition. apply idpath. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Monoids. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Definition FromBinDirectSum {a b : A} (B : BinDirectSum a b) {c : A} (f : a --> c) ∏ (c : A) (f : a --> c) (g : b --> c), (to_In1 B) · (FromBinDirectSum B f g) = f. ∏ (c : A) (f : a --> c) (g : b --> c), (to_In2 B) · (FromBinDirectSum B f g) = g. Definition FromBinDirectSumUnique {a b : A} (B : BinDirectSum a b) {c : A} (f : a --> c) to_In1 B · k = f -> to_In2 B · k = g -> k = FromBinDirectSum B f g := Lemma FromBinDirectSumsEq {c d : A} (DS : BinDirectSum c d) {x : A} (k1 k2 : DS --> x) : rewrite (FromBinDirectSumUnique DS (to_In1 DS · k1) (to_In2 DS · k1) k1). apply FromBinDirectSumUnique. Definition FromBinDirectSumFormula {a b : A} (B : BinDirectSum a b) {c : A} (f : a --> c) Lemma FromBinDirectSumFormulaUnique {a b : A} (B : BinDirectSum a b) {c : A} (f : a --> c) (g : b --> c) : FromBinDirectSumFormula B f g = FromBinDirectSum B f g. unfold FromBinDirectSumFormula. apply FromBinDirectSumUnique. A⟦B1, B2⟧ := FromBinDirectSum B1 (f · (to_In1 B2)) (g · (to_In2 B2)). rewrite <- FromBinDirectSumFormulaUnique. unfold FromBinDirectSumFormula. + exact (to_quot_mor A PAS (FromBinDirectSum A (BD x y) f1 g1)). rewrite <- (@id_left A _ _ (FromBinDirectSum A (BD x y) f1 g1)). - apply ArrowsFromZero. - apply ArrowsFromZero.