Definition to_isBinProduct {a b co : A} {i1 : a --> co} {i2 : b --> co} {p1 : co --> a} {p2 : co --> b} : isBinDirectSum a b co i1 i2 p1 p2 -> isBinProduct A a b co p1 p2. Proof. intros [e11 [e22 [e12 [e21 e]]]]. intros T f g. use unique_exists. - exact ((f · i1) + (g · i2)). - cbn beta. split. + assert (q := to_postmor_linear' (f · i1) (g · i2) p1). rewrite 2 rewrite_op in q. rewrite q. clear q. rewrite <- 2 assoc. rewrite e11. rewrite id_right. rewrite e21. rewrite to_premor_unel'. rewrite runax. reflexivity. + assert (q := to_postmor_linear' (f · i1) (g · i2) p2). rewrite 2 rewrite_op in q. rewrite q. clear q. rewrite <- 2 assoc. rewrite e22. rewrite id_right. rewrite e12. rewrite to_premor_unel'. rewrite lunax. reflexivity. - intros h. cbn beta. apply isapropdirprod;apply hs. - intros h. cbn beta. intros [p q]. rewrite <- p, <- q. rewrite <- 2 assoc. assert (Q := to_premor_linear' h (p1 · i1) (p2 · i2)). rewrite 2 rewrite_op in Q. rewrite <- Q. rewrite e. rewrite id_right. reflexivity. Defined.
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.