Lemma to_Pr2_isEpi {a b : A} (B : BinDirectSum a b) : isEpi (to_Pr2 B). Proof. intros z f g H. apply (maponpaths (λ h : _, (to_In2 B) · h)) in H. repeat rewrite assoc in H. rewrite (to_IdIn2 B) in H. repeat rewrite id_left in H. apply H. 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.