Library UniMath.CategoryTheory.limits.BinDirectSums

Direct definition of binary direct sum using preadditive categories.

Contents

  • Definition of binary direct sums (also known as biproducts)
  • Criteria for binary direct sums
  • Quotient has binary direct sums

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.

Local Open Scope cat.

BinDirectSum is at the same time product and coproduct of the underlying objects together with the following equalities
i1 · p1 = identity and i2 · p2 = identity i1 · p2 = unit and i2 · p1 = unit p1 · i1 + p2 · i2 = identity

Lemma rewrite_op {A:PreAdditive} (x y:A) :
  @to_binop (categoryWithAbgrops_precategoryWithBinOps (PreAdditive_categoryWithAbgrops A)) x y
  =
  @op (pr1monoid (grtomonoid (abgrtogr (@to_abgr (PreAdditive_categoryWithAbgrops A) x y)))).
Show proof.
  reflexivity.

Section def_bindirectsums.

  Variable A : PreAdditive.
  Context (hs := @to_has_homsets A : has_homsets A).

  Open Scope abgrcat.

Definition of binary direct sum.
  Definition isBinDirectSum (a b co : A) (i1 : a --> co) (i2 : b --> co)
             (p1 : co --> a) (p2 : co --> b) : hProp :=
    i1 · p1 = 1 ∧ i2 · p2 = 1 ∧
    i1 · p2 = 0 ∧ i2 · p1 = 0 ∧
    p1 · i1 + p2 · i2 = 1.

  Definition to_isBinCoproduct {a b co : A} {i1 : a --> co} {i2 : b --> co}
             {p1 : co --> a} {p2 : co --> b} :
    isBinDirectSum a b co i1 i2 p1 p2 -> isBinCoproduct A a b co i1 i2.
  Show proof.
    intros [e11 [e22 [e12 [e21 e]]]].
    intros T f g.
    use unique_exists.
    - exact ((p1 · f) + (p2 · g)).
    - cbn beta. split.
      +
        assert (q := to_premor_linear' i1 (p1 · f) (p2 · g)).
        rewrite 2 rewrite_op in q. rewrite q. clear q.
        rewrite 2 assoc. rewrite e11. rewrite id_left.
        rewrite e12. rewrite to_postmor_unel'. rewrite runax.
        reflexivity.
      + assert (q := to_premor_linear' i2 (p1 · f) (p2 · g)).
        rewrite 2 rewrite_op in q. rewrite q. clear q.
        rewrite 2 assoc. rewrite e22. rewrite id_left.
        rewrite e21. rewrite to_postmor_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_postmor_linear' (p1 · i1) (p2 · i2) h).
      rewrite 2 rewrite_op in Q. rewrite <- Q.
      rewrite e. rewrite id_left. reflexivity.

  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.
  Show 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.

  Definition to_IdIn1 {a b co : A} {i1 : a --> co} {i2 : b --> co} {p1 : co --> a} {p2 : co --> b}
             (B : isBinDirectSum a b co i1 i2 p1 p2) :
    i1 · p1 = identity a := pr1 B.

  Definition to_IdIn2 {a b co : A} {i1 : a --> co} {i2 : b --> co} {p1 : co --> a} {p2 : co --> b}
             (B : isBinDirectSum a b co i1 i2 p1 p2) :
    i2 · p2 = identity b := pr12 B.

  Definition to_Unel1 {a b co : A} {i1 : a --> co} {i2 : b --> co} {p1 : co --> a} {p2 : co --> b}
             (B : isBinDirectSum a b co i1 i2 p1 p2) :
    i1 · p2 = (to_unel a b) := pr122 B.

  Definition to_Unel2 {a b co : A} {i1 : a --> co} {i2 : b --> co} {p1 : co --> a} {p2 : co --> b}
             (B : isBinDirectSum a b co i1 i2 p1 p2) :
    i2 · p1 = (to_unel b a) := pr122 (pr2 B).

  Definition to_BinOpId {a b co : A} {i1 : a --> co} {i2 : b --> co} {p1 : co --> a} {p2 : co --> b}
             (B : isBinDirectSum a b co i1 i2 p1 p2) :
    (to_binop co co) (p1 · i1) (p2 · i2) = identity co := pr222 (pr2 B).

The following definition constructs isBinDirectSum from data.
  Definition make_isBinDirectSum (a b co : A)
             (i1 : a --> co) (i2 : b --> co) (p1 : co --> a) (p2 : co --> b)
             (H1 : i1 · p1 = identity a) (H2 : i2 · p2 = identity b)
             (H3 : i1 · p2 = (to_unel a b)) (H4 : i2 · p1 = (to_unel b a))
             (H5 : (to_binop co co) (p1 · i1) (p2 · i2) = identity co)
    : isBinDirectSum a b co i1 i2 p1 p2 := H1,,H2,,H3,,H4,,H5.

Definition of BinDirectSums.
  Definition BinDirectSum (a b : A) : UU :=
    ∑ coab : (∑ co : A, a --> co × b --> co × co --> a × co --> b),
             isBinDirectSum a b (pr1 coab) (pr1 (pr2 coab)) (pr1 (pr2 (pr2 coab)))
                                (pr1 (pr2 (pr2 (pr2 coab)))) (pr2 (pr2 (pr2 (pr2 coab)))).

Construction of BinDirectSum.
  Definition make_BinDirectSum (a b co : A) (i1 : a --> co) (i2 : b --> co)
             (p1 : co --> a) (p2 : co --> b) (H : isBinDirectSum a b co i1 i2 p1 p2) :
    BinDirectSum a b := tpair _ (tpair _ co (i1,,(i2,,(p1,,p2)))) H.

BinDirectSum in categories.
  Definition BinDirectSums : UU := ∏ (a b : A), BinDirectSum a b.

  Definition make_BinDirectSums (H : ∏ (a b : A), BinDirectSum a b) : BinDirectSums := H.

  Definition hasBinDirectSums : hProp.
  Show proof.
    exists (∏ (a b : A), ∥ BinDirectSum a b ∥).
    apply impred; intro p.
    apply impred; intro q.
    apply isapropishinh.

The direct sum object.
  Definition BinDirectSumOb {a b : A} (B : BinDirectSum a b) : A := pr1 (pr1 B).
  Coercion BinDirectSumOb : BinDirectSum >-> ob.

Accessor functions
  Definition to_In1 {a b : A} (B : BinDirectSum a b) : A⟦a, B⟧ := dirprod_pr1 (pr2 (pr1 B)).

  Definition to_In2 {a b : A} (B : BinDirectSum a b) : A⟦b, B⟧ :=
    dirprod_pr1 (dirprod_pr2 (pr2 (pr1 B))).

  Definition to_Pr1 {a b : A} (B : BinDirectSum a b) : A⟦B, a⟧ :=
    dirprod_pr1 (dirprod_pr2 (dirprod_pr2 (pr2 (pr1 B)))).

  Definition to_Pr2 {a b : A} (B : BinDirectSum a b) : A⟦B, b⟧ :=
    dirprod_pr2 (dirprod_pr2 (dirprod_pr2 (pr2 (pr1 B)))).

Another coercion
  Definition BinDirectSum_isBinDirectSum {a b : A} (B : BinDirectSum a b) :
    isBinDirectSum a b B (to_In1 B) (to_In2 B) (to_Pr1 B) (to_Pr2 B) := pr2 B.
  Coercion BinDirectSum_isBinDirectSum : BinDirectSum >-> hProptoType.

Construction of BinCoproduct and BinProduct from BinDirectSum.
  Definition BinDirectSum_BinCoproduct {a b : A} (B : BinDirectSum a b) :
    BinCoproduct a b.
  Show proof.
    use (make_BinCoproduct A a b B (to_In1 B) (to_In2 B)).
    exact (to_isBinCoproduct B).

  Definition BinDirectSum_BinProduct {a b : A} (B : BinDirectSum a b) : BinProduct A a b.
  Show proof.
    use (make_BinProduct A a b B (to_Pr1 B) (to_Pr2 B)).
    exact (to_isBinProduct B).

An arrow to BinDirectSum and arrow from BinDirectSum.
  Definition ToBinDirectSum {a b : A} (B : BinDirectSum a b) {c : A} (f : c --> a)
             (g : c --> b) : A⟦c, B⟧ := BinProductArrow A (BinDirectSum_BinProduct B) f g.

  Definition FromBinDirectSum {a b : A} (B : BinDirectSum a b) {c : A} (f : a --> c)
             (g : b --> c) : A⟦B, c⟧ := BinCoproductArrow (BinDirectSum_BinCoproduct B) f g.

Commutativity of BinDirectSum.
  Definition BinDirectSumIn1Commutes {a b : A} (B : BinDirectSum a b) :
    ∏ (c : A) (f : a --> c) (g : b --> c), (to_In1 B) · (FromBinDirectSum B f g) = f.
  Show proof.
    intros c f g.
    apply (BinCoproductIn1Commutes A a b (BinDirectSum_BinCoproduct B) c f g).

  Definition BinDirectSumIn2Commutes {a b : A} (B : BinDirectSum a b) :
    ∏ (c : A) (f : a --> c) (g : b --> c), (to_In2 B) · (FromBinDirectSum B f g) = g.
  Show proof.
    intros c f g.
    apply (BinCoproductIn2Commutes A a b (BinDirectSum_BinCoproduct B) c f g).

  Definition BinDirectSumPr1Commutes {a b : A} (B : BinDirectSum a b) :
    ∏ (c : A) (f : c --> a) (g : c --> b), (ToBinDirectSum B f g) · (to_Pr1 B) = f.
  Show proof.
    intros c f g.
    apply (BinProductPr1Commutes A a b (BinDirectSum_BinProduct B) c f g).

  Definition BinDirectSumPr2Commutes {a b : A} (B : BinDirectSum a b) :
    ∏ (c : A) (f : c --> a) (g : c --> b), (ToBinDirectSum B f g) · (to_Pr2 B) = g.
  Show proof.
    intros c f g.
    apply (BinProductPr2Commutes A a b (BinDirectSum_BinProduct B) c f g).

Uniqueness of arrow to and from BinDirectSum using the BinProduct and BinCoproduct structures.
  Definition ToBinDirectSumUnique {a b : A} (B : BinDirectSum a b) {c : A} (f : c --> a)
             (g : c --> b) (k : c --> B) :
    k · to_Pr1 B = f -> k · to_Pr2 B = g -> k = ToBinDirectSum B f g :=
    BinProductArrowUnique _ _ _ (BinDirectSum_BinProduct B) c f g k.

  Definition FromBinDirectSumUnique {a b : A} (B : BinDirectSum a b) {c : A} (f : a --> c)
             (g : b --> c) (k : B --> c) :
    to_In1 B · k = f -> to_In2 B · k = g -> k = FromBinDirectSum B f g :=
    BinCoproductArrowUnique _ _ _ (BinDirectSum_BinCoproduct B) c f g k.

Uniqueness of arrows to and from BinDirectSum
  Lemma ToBinDirectSumsEq {c d : A} (DS : BinDirectSum c d) {x : A} (k1 k2 : x --> DS) :
    k1 · to_Pr1 DS = k2 · to_Pr1 DS ->
    k1 · to_Pr2 DS = k2 · to_Pr2 DS -> k1 = k2.
  Show proof.
    intros H1 H2.
    rewrite (ToBinDirectSumUnique DS (k1 · to_Pr1 DS) (k1 · to_Pr2 DS) k1).
    apply pathsinv0.
    apply ToBinDirectSumUnique.
    - apply pathsinv0. apply H1.
    - apply pathsinv0. apply H2.
    - apply idpath.
    - apply idpath.

  Lemma FromBinDirectSumsEq {c d : A} (DS : BinDirectSum c d) {x : A} (k1 k2 : DS --> x) :
    to_In1 DS · k1 = to_In1 DS · k2 -> to_In2 DS · k1 = to_In2 DS · k2 -> k1 = k2.
  Show proof.
    intros H1 H2.
    rewrite (FromBinDirectSumUnique DS (to_In1 DS · k1) (to_In2 DS · k1) k1).
    apply pathsinv0.
    apply FromBinDirectSumUnique.
    - apply pathsinv0. apply H1.
    - apply pathsinv0. apply H2.
    - apply idpath.
    - apply idpath.

The following definitions give a formula for the unique morphisms to and from the BinDirectSum. These formulas are important when one uses bindirectsums. The formulas are
to bindirectsum unique arrow = f · in1 + g · in2 from bindirectsum unique arrow = pr1 · f + pr2 · g
  Definition ToBinDirectSumFormula {a b : A} (B : BinDirectSum a b) {c : A} (f : c --> a)
             (g : c --> b) : A⟦c, B⟧ := (to_binop c B) (f · to_In1 B) (g · to_In2 B).

  Definition FromBinDirectSumFormula {a b : A} (B : BinDirectSum a b) {c : A} (f : a --> c)
             (g : b --> c) : A⟦B, c⟧ := (to_binop B c) (to_Pr1 B · f) (to_Pr2 B · g).

Let us prove that these formulas indeed are the unique morphisms we claimed them to be.
  Lemma ToBinDirectSumFormulaUnique {a b : A} (B : BinDirectSum a b) {c : A} (f : c --> a)
        (g : c --> b) : ToBinDirectSumFormula B f g = ToBinDirectSum B f g.
  Show proof.
    apply ToBinDirectSumUnique.
    - unfold ToBinDirectSumFormula.
      unfold to_binop.
      use (pathscomp0 (to_postmor_linear c (to_Pr1 B) (f · to_In1 B) (g · to_In2 B))).
      unfold to_postmor. repeat rewrite <- assoc.
      rewrite (to_IdIn1 B).
      rewrite id_right.
      rewrite (to_Unel2 B).
      set (XX := to_premor_unel A a g).
      unfold to_premor in XX.
      unfold to_unel.
      rewrite XX.
      apply (to_runax c a).
    - unfold ToBinDirectSumFormula.
      unfold to_binop. cbn.
      use (pathscomp0 (to_postmor_linear c (to_Pr2 B) (f · to_In1 B) (g · to_In2 B))).
      unfold to_postmor. repeat rewrite <- assoc.
      rewrite (to_IdIn2 B). rewrite (to_Unel1 B). rewrite id_right.
      set (XX := to_premor_unel A b f).
      unfold PrecategoriesWithAbgrops.to_premor in XX.
      unfold PrecategoriesWithAbgrops.to_unel.
      rewrite XX. clear XX.
      apply (to_lunax c b).

  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.
  Show proof.
    unfold FromBinDirectSumFormula.
    apply FromBinDirectSumUnique.
    - use (pathscomp0 (to_premor_linear c (to_In1 B) (to_Pr1 B · f) (to_Pr2 B · g))).
      unfold to_premor. repeat rewrite assoc.
      rewrite (to_IdIn1 B). rewrite (to_Unel1 B). rewrite id_left.
      set (XX := to_postmor_unel A a g).
      unfold to_postmor in XX.
      unfold to_unel.
      rewrite XX.
      apply (to_runax a c).
    - use (pathscomp0 (to_premor_linear c (to_In2 B) (to_Pr1 B · f) (to_Pr2 B · g))).
      unfold to_premor. repeat rewrite assoc.
      rewrite (to_IdIn2 B). rewrite (to_Unel2 B). rewrite id_left.
      set (XX := to_postmor_unel A b f).
      unfold to_postmor in XX.
      unfold to_unel.
      rewrite XX.
      apply (to_lunax b c).

The following definitions give 2 ways to construct a morphisms a ⊕ c --> b ⊕ d from two morphisms f : a --> b and g : c --> d , by using the binary direct sums as a product and as a coproduct.
  Definition BinDirectSumIndAr {a b c d : A} (f : a --> b) (g : c --> d)
             (B1 : BinDirectSum a c) (B2 : BinDirectSum b d) :
    A⟦B1, B2⟧ := ToBinDirectSum B2 ((to_Pr1 B1) · f) ((to_Pr2 B1) · g).

  Definition BinDirectSumIndAr' {a b c d : A} (f : a --> b) (g : c --> d)
             (B1 : BinDirectSum a c) (B2 : BinDirectSum b d) :
    A⟦B1, B2⟧ := FromBinDirectSum B1 (f · (to_In1 B2)) (g · (to_In2 B2)).

Both of the above morphisms are given by the following formula.
  Definition BinDirectSumIndArFormula {a b c d: A} (f : a --> b) (g : c --> d)
             (B1 : BinDirectSum a c) (B2 : BinDirectSum b d) :
    A⟦B1, B2⟧ := (to_binop B1 B2) (to_Pr1 B1 · f · to_In1 B2) (to_Pr2 B1 · g · to_In2 B2).

  Lemma BinDirectSumIndArEq1 {a b c d : A} (f : a --> b) (g : c --> d)
             (B1 : BinDirectSum a c) (B2 : BinDirectSum b d) :
    BinDirectSumIndAr f g B1 B2 = BinDirectSumIndArFormula f g B1 B2.
  Show proof.
    unfold BinDirectSumIndAr.
    rewrite <- ToBinDirectSumFormulaUnique.
    unfold ToBinDirectSumFormula.
    unfold BinDirectSumIndArFormula.
    apply idpath.

  Lemma BinDirectSumIndArEq2 {a b c d : A} (f : a --> b) (g : c --> d)
             (B1 : BinDirectSum a c) (B2 : BinDirectSum b d) :
    BinDirectSumIndAr' f g B1 B2 = BinDirectSumIndArFormula f g B1 B2.
  Show proof.
    unfold BinDirectSumIndAr'.
    rewrite <- FromBinDirectSumFormulaUnique.
    unfold FromBinDirectSumFormula.
    unfold BinDirectSumIndArFormula.
    rewrite assoc. rewrite assoc.
    apply idpath.

Thus we have equality.
  Definition BinDirectSumIndArEq {a b c d : A} (f : a --> b) (g : c --> d)
             (B1 : BinDirectSum a c) (B2 : BinDirectSum b d) :
    BinDirectSumIndAr f g B1 B2 = BinDirectSumIndAr' f g B1 B2.
  Show proof.
    rewrite -> BinDirectSumIndArEq1.
    rewrite -> BinDirectSumIndArEq2.
    apply idpath.

Composition of IndAr

  Lemma BinDirectSumIndArComp {a b c d e f : A} (f1 : a --> b) (f2 : b --> c)
        (g1 : d --> e) (g2 : e --> f) (B1 : BinDirectSum a d) (B2 : BinDirectSum b e)
        (B3 : BinDirectSum c f) :
    BinDirectSumIndAr f1 g1 B1 B2 · BinDirectSumIndAr f2 g2 B2 B3 =
    BinDirectSumIndAr (f1 · f2) (g1 · g2) B1 B3.
  Show proof.
    rewrite BinDirectSumIndArEq1. rewrite (BinDirectSumIndArEq1 f2). rewrite (BinDirectSumIndArEq1 (f1 · f2)).
    unfold BinDirectSumIndArFormula.
    rewrite to_postmor_linear'.
    rewrite to_premor_linear'.
    rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc.
    rewrite <- (assoc _ (to_In1 B2)). rewrite <- (assoc _ (to_In1 B2)).
    rewrite (to_IdIn1 B2). rewrite id_right.
    rewrite (to_Unel1 B2). rewrite to_premor_unel'.
    rewrite to_postmor_unel'. rewrite to_postmor_unel'. rewrite to_runax'.
    rewrite to_premor_linear'.
    rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc.
    rewrite <- (assoc _ (to_In2 B2)). rewrite <- (assoc _ (to_In2 B2)).
    rewrite (to_IdIn2 B2). rewrite id_right.
    rewrite (to_Unel2 B2). rewrite to_premor_unel'.
    rewrite to_postmor_unel'. rewrite to_postmor_unel'.
    rewrite to_lunax'.
    apply idpath.

End def_bindirectsums.
Arguments BinDirectSumIndAr {_ _ _ _ _}.
Arguments BinDirectSumOb {_ _ _}.
Arguments BinDirectSum {_}.
Arguments to_Pr1 {_ _ _} _.
Arguments to_Pr2 {_ _ _} _.
Arguments to_In1 {_ _ _} _.
Arguments to_In2 {_ _ _} _.
Arguments to_BinOpId {_ _ _ _ _ _ _ _}.
Arguments to_IdIn1 {_ _ _ _ _ _ _ _}.
Arguments to_IdIn2 {_ _ _ _ _ _ _ _}.
Arguments to_Unel1 {_ _ _ _ _ _ _ _}.
Arguments to_Unel2 {_ _ _ _ _ _ _ _}.
Arguments ToBinDirectSum {_ _ _} _ {_}.
Arguments isBinDirectSum {_ _ _ _}.

In1 and In2 are monics, and Pr1 and Pr2 are epis.
Section bindirectsums_monics_and_epis.

  Variable A : PreAdditive.

  Lemma to_In1_isMonic {a b : A} (B : BinDirectSum a b) : isMonic (to_In1 B).
  Show proof.
    intros z f g H.
    apply (maponpaths (λ h : _, h · (to_Pr1 B))) in H.
    repeat rewrite <- assoc in H.
    set (X:= to_IdIn1 (A:=A) B).
    assert (X1 : to_In1 B · to_Pr1 B = 1%abgrcat).
    { apply (to_IdIn1 (A:=A) B). }
    apply (@pathscomp0 _ _ ( f · (to_In1 B · to_Pr1 B)) _).
    - apply pathsinv0.
      etrans. { apply maponpaths.
                apply X1. }
      apply id_right.
    - etrans. { apply H. }
      etrans. { apply maponpaths. apply X1. }
      apply id_right.

  Lemma to_In2_isMonic {a b : A} (B : BinDirectSum a b) : isMonic (to_In2 B).
  Show proof.
    intros z f g H.
    apply (maponpaths (λ h : _, h · (to_Pr2 B))) in H.
    repeat rewrite <- assoc in H.
    set (X:= to_IdIn2 (A:=A) B).
    assert (X1 : to_In2 B · to_Pr2 B = 1%abgrcat).
    { apply X. }
    apply (@pathscomp0 _ _ ( f · (to_In2 B · to_Pr2 B)) _).
    - apply pathsinv0.
      etrans. { apply maponpaths. apply X1. }
      apply id_right.
    - etrans. { apply H. }
      etrans. { apply maponpaths. apply X1. }
      apply id_right.

  Lemma to_Pr1_isEpi {a b : A} (B : BinDirectSum a b) : isEpi (to_Pr1 B).
  Show proof.
    intros z f g H.
    apply (maponpaths (λ h : _, (to_In1 B) · h)) in H.
    repeat rewrite assoc in H. rewrite (to_IdIn1 B) in H.
    repeat rewrite id_left in H. apply H.

  Lemma to_Pr2_isEpi {a b : A} (B : BinDirectSum a b) : isEpi (to_Pr2 B).
  Show 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.

End bindirectsums_monics_and_epis.

If a PreAdditive category has BinProducts, then it has all direct sums.
Section bindirectsums_criteria.

  Variable A : PreAdditive.
  Hypothesis hs : has_homsets A.
  Variable Z : Zero A.

  Definition BinDirectSums_from_binproduct_bincoproducts_eq1 {X Y : A} (P : BinProduct A X Y) :
    BinProductArrow A P (identity X) (ZeroArrow Z X Y) · BinProductPr1 A P = identity _ .
  Show proof.
    apply BinProductPr1Commutes.

  Definition BinDirectSums_from_binproduct_bincoproducts_eq2 {X Y : A} (P : BinProduct A X Y) :
    BinProductArrow A P (identity X) (ZeroArrow Z X Y) · BinProductPr2 A P = to_unel X Y.
  Show proof.
    rewrite (PreAdditive_unel_zero A Z).
    apply BinProductPr2Commutes.

  Definition BinDirectSums_from_binproduct_bincoproducts_eq3 {X Y : A} (P : BinProduct A X Y) :
    BinProductArrow A P (ZeroArrow Z Y X) (identity _ ) · BinProductPr1 A P = to_unel Y X.
  Show proof.
    rewrite (PreAdditive_unel_zero A Z).
    apply BinProductPr1Commutes.

  Definition BinDirectSums_from_binproduct_bincoproducts_eq4 {X Y : A} (P : BinProduct A X Y) :
    BinProductArrow A P (ZeroArrow Z Y X) (identity _ ) · BinProductPr2 A P = identity _ .
  Show proof.
    apply BinProductPr2Commutes.

  Definition BinDirectSums_from_binproduct_bincoproducts_eq5 {X Y : A} (P : BinProduct A X Y) :
    to_binop
      (BinProductObject A P) (BinProductObject A P)
      (BinProductPr1 A P · BinProductArrow A P(identity X) (ZeroArrow Z X Y))
      (BinProductPr2 A P · BinProductArrow A P (ZeroArrow Z Y X) (identity Y)) = identity _ .
  Show proof.
    apply BinProductArrowsEq.
    - rewrite to_postmor_linear'.
      rewrite <- assoc. rewrite <- assoc.
      rewrite BinProductPr1Commutes. rewrite BinProductPr1Commutes.
      rewrite id_right. rewrite ZeroArrow_comp_right.
      rewrite <- PreAdditive_unel_zero.
      rewrite id_left.
      apply to_runax.
    - rewrite to_postmor_linear'.
      rewrite <- assoc. rewrite <- assoc.
      rewrite BinProductPr2Commutes. rewrite BinProductPr2Commutes.
      rewrite id_right. rewrite ZeroArrow_comp_right.
      rewrite <- PreAdditive_unel_zero.
      rewrite id_left.
      apply to_lunax.

  Definition BinDirectSums_from_binproduct_bincoproducts_isCoproduct {X Y : A}
             (P : BinProduct A X Y) :
    isBinCoproduct A X Y (BinProductObject A P)
                         (BinProductArrow A P (identity X) (ZeroArrow Z X Y))
                         (BinProductArrow A P (ZeroArrow Z Y X) (identity Y)).
  Show proof.
    use (make_isBinCoproduct _ hs).
    intros c f g.
    use unique_exists.
    - exact (to_binop (BinProductObject A P) c (BinProductPr1 A P · f) (BinProductPr2 A P · g)).
    - split.
      + rewrite to_premor_linear'.
        rewrite assoc. rewrite assoc.
        rewrite BinProductPr1Commutes.
        rewrite BinProductPr2Commutes.
        rewrite ZeroArrow_comp_left.
        rewrite id_left.
        rewrite <- PreAdditive_unel_zero.
        apply to_runax.
      + rewrite to_premor_linear'.
        rewrite assoc. rewrite assoc.
        rewrite BinProductPr1Commutes.
        rewrite BinProductPr2Commutes.
        rewrite ZeroArrow_comp_left.
        rewrite id_left.
        rewrite <- PreAdditive_unel_zero.
        apply to_lunax.
    - intros y. apply isapropdirprod. apply hs. apply hs.
    - intros y H. induction H as [t p]. rewrite <- t. rewrite <- p.
      rewrite assoc. rewrite assoc.
      rewrite <- to_postmor_linear'.
      rewrite (BinDirectSums_from_binproduct_bincoproducts_eq5 P).
      rewrite id_left. apply idpath.

  Definition BinDirectSums_from_binproduct_bincoproducts_isProduct {X Y : A}
             (P : BinProduct A X Y) :
    isBinProduct A X Y (BinProductObject A P) (BinProductPr1 A P) (BinProductPr2 A P).
  Show proof.
    use (make_isBinProduct _ ).
    intros c f g.
    use unique_exists.
    - exact (BinProductArrow A P f g).
    - split.
      + apply BinProductPr1Commutes.
      + apply BinProductPr2Commutes.
    - intros y. apply isapropdirprod.
      + apply hs.
      + apply hs.
    - intros y H. induction H as [t p]. rewrite <- t. rewrite <- p.
      rewrite <- precompWithBinProductArrow.
      apply BinProductArrowsEq.
      + rewrite <- assoc. rewrite BinProductPr1Commutes. apply idpath.
      + rewrite <- assoc. rewrite BinProductPr2Commutes. apply idpath.

  Definition BinDirectSum_from_BinProduct {X Y : A} (P : BinProduct A X Y) :
    BinDirectSum X Y :=
    make_BinDirectSum
      A X Y
      (BinProductObject A P)
      (BinProductArrow A P (identity X) (ZeroArrow Z X Y))
      (BinProductArrow A P (ZeroArrow Z Y X) (identity Y))
      (BinProductPr1 A P)
      (BinProductPr2 A P)
      (make_isBinDirectSum
         _ _ _ _ _ _ _ _
         (BinDirectSums_from_binproduct_bincoproducts_eq1 P)
         (BinDirectSums_from_binproduct_bincoproducts_eq4 P)
         (BinDirectSums_from_binproduct_bincoproducts_eq2 P)
         (BinDirectSums_from_binproduct_bincoproducts_eq3 P)
         (BinDirectSums_from_binproduct_bincoproducts_eq5 P)).

  Definition BinDirectSums_from_BinProducts (BinProds : BinProducts A) : BinDirectSums A.
  Show proof.
    intros X Y.
    exact (BinDirectSum_from_BinProduct (BinProds X Y)).

End bindirectsums_criteria.

BinDirectSums in quotient of PreAdditive category

In this section we show that, if a PreAdditive A has BinDirectSums, then the quotient of the preadditive category has BinDirectSums. This is used to show that quotient of an CategoryWithAdditiveStructure is CategoryWithAdditiveStructure.
Section bindirectsums_in_quot.

  Variable A : PreAdditive.
  Hypothesis Z : Zero A.
  Hypothesis BD : BinDirectSums A.
  Hypothesis PAS : PreAdditiveSubabgrs A.
  Hypothesis PAC : PreAdditiveComps A PAS.

  Lemma Quotcategory_isBinCoproduct (x y : A) :
    isBinCoproduct (Quotcategory_PreAdditive A PAS PAC) x y (BD x y)
                         (to_quot_mor A PAS (to_In1 (BD x y)))
                         (to_quot_mor A PAS (to_In2 (BD x y))).
  Show proof.
    use make_isBinCoproduct.
    - apply has_homsets_Quotcategory.
    - intros c f g.
      set (f'' := @issurjsetquotpr (@to_abgr A x c) (binopeqrel_subgr_eqrel (PAS x c)) f).
      use (squash_to_prop f''). apply isapropiscontr. intros f'. clear f''.
      set (g'' := @issurjsetquotpr (@to_abgr A y c) (binopeqrel_subgr_eqrel (PAS y c)) 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 (FromBinDirectSum A (BD x y) f1 g1)).
      + cbn beta. split.
        * use (pathscomp0 (Quotcategory_comp_linear A PAS PAC _ _)).
          rewrite BinDirectSumIn1Commutes. exact f2.
        * use (pathscomp0 (Quotcategory_comp_linear A PAS PAC _ _)).
          rewrite BinDirectSumIn2Commutes. 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 (BD x y) c)
                                       (binopeqrel_subgr_eqrel (PAS (BD x y) c)) 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_left (Quotcategory_PreAdditive A PAS PAC) _ _
                              (setquotpr (binopeqrel_subgr_eqrel (PAS (BD x y) c)) y1)).
          rewrite <- (@id_left A _ _ (FromBinDirectSum A (BD x y) f1 g1)).
          rewrite <- (to_BinOpId (BD x y)). rewrite to_postmor_linear'.
          repeat rewrite <- assoc.
          rewrite BinDirectSumIn1Commutes.
          rewrite BinDirectSumIn2Commutes.
          rewrite <- f2 in T1. rewrite <- g2 in T2. unfold to_quot_mor.
          set (tmp := @setquotpr_linear A PAS PAC (BD x y) c). unfold to_quot_mor in tmp.
          rewrite tmp. clear tmp.
          set (tmp := @Quotcategory_comp_linear A PAS PAC (BD x y) x c).
          unfold to_quot_mor in tmp. rewrite <- tmp. clear tmp.
          rewrite <- T1.
          set (tmp := @Quotcategory_comp_linear A PAS PAC (BD x y) y c).
          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_postmor_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_postcomposition.
          apply idpath.

  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))).
  Show 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.

  Opaque Quotcategory_PreAdditive.   Lemma Quotcategory_isBinDirectSum (x y : A) :
    isBinDirectSum
      (A := Quotcategory_PreAdditive A PAS PAC)
      (to_quot_mor A PAS (to_In1 (BD x y))) (to_quot_mor A PAS (to_In2 (BD x y)))
      (to_quot_mor A PAS (to_Pr1 (BD x y))) (to_quot_mor A PAS (to_Pr2 (BD x y))).
  Show proof.
    use make_isBinDirectSum.
    - unfold to_quot_mor.
      rewrite <- comp_eq.
      set (tmp := @Quotcategory_comp_linear A PAS PAC x (BD x y) x).
      unfold to_quot_mor in tmp. rewrite tmp. clear tmp.
      rewrite (to_IdIn1 (BD x y)).
      apply idpath.
    - unfold to_quot_mor.
      rewrite <- comp_eq.
      set (tmp := @Quotcategory_comp_linear A PAS PAC y (BD x y) y).
      unfold to_quot_mor in tmp. rewrite tmp. clear tmp.
      rewrite (to_IdIn2 (BD x y)).
      apply idpath.
    - unfold to_quot_mor.
      rewrite <- comp_eq.
      set (tmp := @Quotcategory_comp_linear A PAS PAC x (BD x y) y).
      unfold to_quot_mor in tmp. rewrite tmp. clear tmp.
      rewrite (to_Unel1 (BD x y)).
      apply idpath.
    - unfold to_quot_mor.
      rewrite <- comp_eq.
      set (tmp := @Quotcategory_comp_linear A PAS PAC y (BD x y) x).
      unfold to_quot_mor in tmp. rewrite tmp. clear tmp.
      rewrite (to_Unel2 (BD x y)).
      apply idpath.
    - unfold to_quot_mor.
      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 (to_BinOpId (BD x y)).
      apply idpath.
  Transparent Quotcategory_PreAdditive.
  Definition Quotcategory_BinDirectSums : BinDirectSums (Quotcategory_PreAdditive A PAS PAC).
  Show proof.
    intros x y.
    use make_BinDirectSum.
    - exact (BD x y).
    - exact (to_quot_mor A PAS (to_In1 (BD x y))).
    - exact (to_quot_mor A PAS (to_In2 (BD x y))).
    - exact (to_quot_mor A PAS (to_Pr1 (BD x y))).
    - exact (to_quot_mor A PAS (to_Pr2 (BD x y))).
    - exact (Quotcategory_isBinDirectSum x y).

End bindirectsums_in_quot.

Notation "'π₁'" := (to_Pr1 _) : abgrcat.
Notation "'π₂'" := (to_Pr2 _) : abgrcat.
Notation "'ι₁'" := (to_In1 _) : abgrcat.
Notation "'ι₂'" := (to_In2 _) : abgrcat.
Local Open Scope abgrcat.

Definition reverseBinDirectSum {M:PreAdditive} {A B:M} : BinDirectSum A B -> BinDirectSum B A.
Show proof.
  intros AB.
  refine (make_BinDirectSum M B A (BinDirectSumOb AB) ι₂ ι₁ π₂ π₁ _).
  unfold isBinDirectSum.
  exists (to_IdIn2 (pr2 AB)).
  exists (to_IdIn1 (pr2 AB)).
  exists (to_Unel2 (pr2 AB)).
  exists (to_Unel1 (pr2 AB)).
  cbn. rewrite rewrite_op.
  exact (commax (to_abgr _ _) _ _ @ to_BinOpId (pr2 AB)).

Definition oppositeBinDirectSum {M:PreAdditive} {x y:M} :
  BinDirectSum x y -> BinDirectSum (A:=oppositePreAdditive M) x y.
Show proof.
  intros Q.
  use make_BinDirectSum.
  + exact (BinDirectSumOb Q).
  + exact (to_Pr1 Q).
  + exact (to_Pr2 Q).
  + exact (to_In1 Q).
  + exact (to_In2 Q).
  + exact (make_isBinDirectSum (oppositePreAdditive M) _ _ _ _ _ _ _
       (to_IdIn1 Q) (to_IdIn2 Q) (to_Unel2 Q) (to_Unel1 Q)
       (to_BinOpId Q)).

Definition isTrivialDirectSum {M : PreAdditive} (Z:Zero M) (A:M) : @isBinDirectSum M A Z A 1 0 1 0.
Show proof.
  repeat split; cbn.
  - apply id_right.
  - apply ArrowsToZero.
  - apply ArrowsToZero.
  - apply ArrowsFromZero.
  - rewrite id_right. rewrite to_premor_unel'. rewrite rewrite_op. rewrite runax. reflexivity.
Definition TrivialDirectSum {M : PreAdditive} (Z:Zero M) (A:M) : BinDirectSum A Z.
Show proof.
  exact (make_BinDirectSum _ _ _ _ _ _ _ _ (isTrivialDirectSum _ _)).
Definition isTrivialDirectSum' {M : PreAdditive} (Z:Zero M) (A:M) : @isBinDirectSum M Z A A 0 1 0 1.
Show proof.
  repeat split; cbn.
  - apply ArrowsToZero.
  - apply id_right.
  - apply ArrowsFromZero.
  - apply ArrowsToZero.
  - rewrite id_right. rewrite to_premor_unel'. rewrite rewrite_op. rewrite lunax. reflexivity.
Definition TrivialDirectSum' {M : PreAdditive} (Z:Zero M) (A:M) : BinDirectSum Z A.
Show proof.
  exact (make_BinDirectSum _ _ _ _ _ _ _ _ (isTrivialDirectSum' _ _)).
Definition replaceSum {M:PreAdditive} {A B C:M} (S:BinDirectSum A B) :
  z_iso C S -> BinDirectSum A B .
Show proof.
  intros r.
  exists (C,, ι₁ · z_iso_inv r,, ι₂ · z_iso_inv r,, r · π₁,, r · π₂).
  repeat split; cbn.
  + rewrite assoc'. rewrite (assoc _ r). rewrite z_iso_after_z_iso_inv, id_left. exact (to_IdIn1 S).
  + rewrite assoc'. rewrite (assoc _ r). rewrite z_iso_after_z_iso_inv, id_left. exact (to_IdIn2 S).
  + rewrite assoc'. rewrite (assoc _ r). rewrite z_iso_after_z_iso_inv, id_left. exact (to_Unel1 S).
  + rewrite assoc'. rewrite (assoc _ r). rewrite z_iso_after_z_iso_inv, id_left. exact (to_Unel2 S).
  + rewrite rewrite_op. rewrite 2 (assoc' r). rewrite 4 (assoc _ _ (inv_from_z_iso r)).
    rewrite <- leftDistribute. rewrite <- rightDistribute. rewrite wrap_inverse'.
    * reflexivity.
    * exact (to_BinOpId S).
Lemma DirectSumIn1Pr2 {M:PreAdditive} {a b:M} (S:BinDirectSum a b) : to_In1 S · to_Pr2 S = 0.
Show proof.
  exact (to_Unel1 S).
Lemma DirectSumIn2Pr1 {M:PreAdditive} {a b:M} (S:BinDirectSum a b) : to_In2 S · to_Pr1 S = 0.
Show proof.
  exact (to_Unel2 S).