(** * Biproducts in categories with zero objects

    Objects that are simultaneously products and coproducts, fundamental
    to additive category theory.
*)

From HoTT Require Import Basics.Overture Basics.Tactics.
From HoTT.Categories Require Import Category.Core.
From HoTT.Categories.Additive Require Import ZeroObjects.

Local Notation fst_type := Basics.Overture.fst.
Local Notation snd_type := Basics.Overture.snd.

Local Open Scope morphism_scope.

(** * Biproduct structures *)

(** ** Biproduct data

    The data of a biproduct consists of an object together with injection
    and projection morphisms.
*)

Record BiproductData {C : PreCategory} (X Y : object C) := {
  biproduct_obj : object C;

  (* Coproduct structure: injections *)
  inl : morphism C X biproduct_obj;
  inr : morphism C Y biproduct_obj;

  (* Product structure: projections *)
  outl : morphism C biproduct_obj X;
  outr : morphism C biproduct_obj Y
}.

Coercion biproduct_obj : BiproductData >-> object.

Arguments biproduct_obj {C X Y} b : rename.
Arguments inl {C X Y} b : rename.
Arguments inr {C X Y} b : rename.
Arguments outl {C X Y} b : rename.
Arguments outr {C X Y} b : rename.

(** ** Biproduct axioms

    The axioms that make biproduct data into an actual biproduct.
    These ensure the projection-injection pairs behave correctly.
*)

Record IsBiproduct {C : PreCategory} `{Z : ZeroObject C} {X Y : object C}
                   (B : BiproductData X Y) := {
  (* Projection-injection identities *)
  beta_l : outl B o inl B = 1;
  beta_r : outr B o inr B = 1;

  (* Mixed terms are zero *)
  mixed_l : outl B o inr B = zero_morphism Y X;
  mixed_r : outr B o inl B = zero_morphism X Y
}.

Arguments beta_l {C Z X Y B} i : rename.
Arguments beta_r {C Z X Y B} i : rename.
Arguments mixed_l {C Z X Y B} i : rename.
Arguments mixed_r {C Z X Y B} i : rename.

(** ** Universal property of biproducts

    The universal property states that morphisms into/out of the biproduct
    are uniquely determined by their components.
*)

Record HasBiproductUniversal {C : PreCategory} {X Y : object C}
  (B : BiproductData X Y) := {
  (* Universal property as a coproduct *)
  coprod_universal : forall (W : object C)
    (f : morphism C X W) (g : morphism C Y W),
    Contr {h : morphism C B W &
           ((h o inl B = f) * (h o inr B = g))};

  (* Universal property as a product *)
  prod_universal : forall (W : object C)
    (f : morphism C W X) (g : morphism C W Y),
    Contr {h : morphism C W B &
           ((outl B o h = f) * (outr B o h = g))}
}.

Arguments coprod_universal {C X Y B} u W f g : rename.
Arguments prod_universal {C X Y B} u W f g : rename.

(** ** Complete biproduct structure

    A biproduct is biproduct data together with the proof that it satisfies
    the biproduct axioms and universal property.  The zero object is an
    explicit argument so that instances can be written [Biproduct Z X Y].
*)

Class Biproduct {C : PreCategory} (Z : ZeroObject C) (X Y : object C) := {
  biproduct_data : BiproductData X Y;
  biproduct_is : IsBiproduct biproduct_data;
  biproduct_universal : HasBiproductUniversal biproduct_data
}.

Coercion biproduct_data : Biproduct >-> BiproductData.

Arguments biproduct_data {C Z X Y} b : rename.
Arguments biproduct_is {C Z X Y} b : rename.
Arguments biproduct_universal {C Z X Y} b : rename.

(** * Biproduct operations *)

Section BiproductOperations.
  Context {C : PreCategory} {Z : ZeroObject C} {X Y : object C}.
  Variable (B : Biproduct Z X Y).

  (** ** Uniqueness from universal property *)

  (** The coproduct universal morphism and its properties. *)
  Definition biproduct_coprod_universal (W : object C)
    (f : morphism C X W) (g : morphism C Y W)
    : {h : morphism C B W & ((h o inl B = f) * (h o inr B = g))}
    := @center _ (coprod_universal (biproduct_universal B) W f g).

  (** Extract the unique morphism from the coproduct universal property. *)
  Definition biproduct_coprod_mor (W : object C)
    (f : morphism C X W) (g : morphism C Y W)
    : morphism C B W
    := (biproduct_coprod_universal W f g).1.

  Definition biproduct_coprod_beta_l (W : object C)
    (f : morphism C X W) (g : morphism C Y W)
    : biproduct_coprod_mor W f g o inl B = f
    := fst_type (biproduct_coprod_universal W f g).2.

  Definition biproduct_coprod_beta_r (W : object C)
    (f : morphism C X W) (g : morphism C Y W)
    : biproduct_coprod_mor W f g o inr B = g
    := snd_type (biproduct_coprod_universal W f g).2.

  Definition biproduct_coprod_unique (W : object C)
    (f : morphism C X W) (g : morphism C Y W)
    (h : morphism C B W)
    (Hl : h o inl B = f)
    (Hr : h o inr B = g)
    : h = biproduct_coprod_mor W f g
    := ap pr1 (contr (h; (Hl, Hr)))^.

  (** The product universal morphism and its properties. *)
  Definition biproduct_prod_universal (W : object C)
    (f : morphism C W X) (g : morphism C W Y)
    : {h : morphism C W B & ((outl B o h = f) * (outr B o h = g))}
    := @center _ (prod_universal (biproduct_universal B) W f g).

  (** Extract the unique morphism from the product universal property. *)
  Definition biproduct_prod_mor (W : object C)
    (f : morphism C W X) (g : morphism C W Y)
    : morphism C W B
    := (biproduct_prod_universal W f g).1.

  Definition biproduct_prod_beta_l (W : object C)
    (f : morphism C W X) (g : morphism C W Y)
    : outl B o biproduct_prod_mor W f g = f
    := fst_type (biproduct_prod_universal W f g).2.

  Definition biproduct_prod_beta_r (W : object C)
    (f : morphism C W X) (g : morphism C W Y)
    : outr B o biproduct_prod_mor W f g = g
    := snd_type (biproduct_prod_universal W f g).2.

  Definition biproduct_prod_unique (W : object C)
    (f : morphism C W X) (g : morphism C W Y)
    (h : morphism C W B)
    (Hl : outl B o h = f)
    (Hr : outr B o h = g)
    : h = biproduct_prod_mor W f g
    := ap pr1 (contr (h; (Hl, Hr)))^.

  (** Pairing with zero on the right is the left injection composed. *)
  Lemma biproduct_prod_zero_r (W : object C) (h : morphism C W X)
    : biproduct_prod_mor W h (zero_morphism W Y)
      = inl B o h.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W X
biproduct_prod_mor W h (zero_morphism W Y) = inl B o h
  Proof.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W X
biproduct_prod_mor W h (zero_morphism W Y) = inl B o h
    symmetry.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W X
inl B o h = biproduct_prod_mor W h (zero_morphism W Y)
    rapply biproduct_prod_unique.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W X
outl B o (inl B o h) = h
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W X
outr B o (inl B o h) = zero_morphism W Y
    -
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W X
outl B o (inl B o h) = h rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W X
outl B o inl B o h = h
      rewrite (beta_l (biproduct_is B)).
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W X
1 o h = h
      apply left_identity.
    -
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W X
outr B o (inl B o h) = zero_morphism W Y rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W X
outr B o inl B o h = zero_morphism W Y
      rewrite (mixed_r (biproduct_is B)).
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W X
zero_morphism X Y o h = zero_morphism W Y
      apply zero_morphism_left.
  Qed.

  (** Pairing with zero on the left is the right injection composed. *)
  Lemma biproduct_prod_zero_l (W : object C) (h : morphism C W Y)
    : biproduct_prod_mor W (zero_morphism W X) h
      = inr B o h.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W Y
biproduct_prod_mor W (zero_morphism W X) h = inr B o h
  Proof.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W Y
biproduct_prod_mor W (zero_morphism W X) h = inr B o h
    symmetry.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W Y
inr B o h = biproduct_prod_mor W (zero_morphism W X) h
    rapply biproduct_prod_unique.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W Y
outl B o (inr B o h) = zero_morphism W X
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W Y
outr B o (inr B o h) = h
    -
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W Y
outl B o (inr B o h) = zero_morphism W X rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W Y
outl B o inr B o h = zero_morphism W X
      rewrite (mixed_l (biproduct_is B)).
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W Y
zero_morphism Y X o h = zero_morphism W X
      apply zero_morphism_left.
    -
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W Y
outr B o (inr B o h) = h rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W Y
outr B o inr B o h = h
      rewrite (beta_r (biproduct_is B)).
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W: C
h: morphism C W Y
1 o h = h
      apply left_identity.
  Qed.

  (** Pairing is natural in the domain. *)
  Lemma biproduct_prod_mor_nat (V W : object C)
    (f : morphism C W X) (g : morphism C W Y) (h : morphism C V W)
    : biproduct_prod_mor W f g o h
      = biproduct_prod_mor V (f o h) (g o h).
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
V, W: C
f: morphism C W X
g: morphism C W Y
h: morphism C V W
biproduct_prod_mor W f g o h = biproduct_prod_mor V (f o h) (g o h)
  Proof.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
V, W: C
f: morphism C W X
g: morphism C W Y
h: morphism C V W
biproduct_prod_mor W f g o h = biproduct_prod_mor V (f o h) (g o h)
    rapply biproduct_prod_unique.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
V, W: C
f: morphism C W X
g: morphism C W Y
h: morphism C V W
outl B o (biproduct_prod_mor W f g o h) = f o h
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
V, W: C
f: morphism C W X
g: morphism C W Y
h: morphism C V W
outr B o (biproduct_prod_mor W f g o h) = g o h
    -
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
V, W: C
f: morphism C W X
g: morphism C W Y
h: morphism C V W
outl B o (biproduct_prod_mor W f g o h) = f o h rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
V, W: C
f: morphism C W X
g: morphism C W Y
h: morphism C V W
outl B o biproduct_prod_mor W f g o h = f o h
      rewrite biproduct_prod_beta_l.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
V, W: C
f: morphism C W X
g: morphism C W Y
h: morphism C V W
f o h = f o h
      reflexivity.
    -
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
V, W: C
f: morphism C W X
g: morphism C W Y
h: morphism C V W
outr B o (biproduct_prod_mor W f g o h) = g o h rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
V, W: C
f: morphism C W X
g: morphism C W Y
h: morphism C V W
outr B o biproduct_prod_mor W f g o h = g o h
      rewrite biproduct_prod_beta_r.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
V, W: C
f: morphism C W X
g: morphism C W Y
h: morphism C V W
g o h = g o h
      reflexivity.
  Qed.

  (** Copairing is natural in the codomain. *)
  Lemma biproduct_coprod_mor_nat (W V : object C)
    (f : morphism C X W) (g : morphism C Y W) (h : morphism C W V)
    : h o biproduct_coprod_mor W f g
      = biproduct_coprod_mor V (h o f) (h o g).
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W, V: C
f: morphism C X W
g: morphism C Y W
h: morphism C W V
h o biproduct_coprod_mor W f g = biproduct_coprod_mor V (h o f) (h o g)
  Proof.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W, V: C
f: morphism C X W
g: morphism C Y W
h: morphism C W V
h o biproduct_coprod_mor W f g = biproduct_coprod_mor V (h o f) (h o g)
    rapply biproduct_coprod_unique.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W, V: C
f: morphism C X W
g: morphism C Y W
h: morphism C W V
h o biproduct_coprod_mor W f g o inl B = h o f
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W, V: C
f: morphism C X W
g: morphism C Y W
h: morphism C W V
h o biproduct_coprod_mor W f g o inr B = h o g
    -
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W, V: C
f: morphism C X W
g: morphism C Y W
h: morphism C W V
h o biproduct_coprod_mor W f g o inl B = h o f rewrite associativity.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W, V: C
f: morphism C X W
g: morphism C Y W
h: morphism C W V
h o (biproduct_coprod_mor W f g o inl B) = h o f
      rewrite biproduct_coprod_beta_l.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W, V: C
f: morphism C X W
g: morphism C Y W
h: morphism C W V
h o f = h o f
      reflexivity.
    -
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W, V: C
f: morphism C X W
g: morphism C Y W
h: morphism C W V
h o biproduct_coprod_mor W f g o inr B = h o g rewrite associativity.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W, V: C
f: morphism C X W
g: morphism C Y W
h: morphism C W V
h o (biproduct_coprod_mor W f g o inr B) = h o g
      rewrite biproduct_coprod_beta_r.
C: PreCategory
Z: ZeroObject C
X, Y: C
B: Biproduct Z X Y
W, V: C
f: morphism C X W
g: morphism C Y W
h: morphism C W V
h o g = h o g
      reflexivity.
  Qed.

End BiproductOperations.

Arguments biproduct_prod_mor {C Z X Y} B {W} f g.

(** * Functoriality of biproducts *)

Section BiproductFunctoriality.
  Context {C : PreCategory} {Z : ZeroObject C} {X Y X' Y' : object C}
    {BXY : Biproduct Z X Y} {BX'Y' : Biproduct Z X' Y'}.

  (** The morphism between biproducts induced by morphisms of the summands. *)
  Definition biproduct_sum_map
    (a : morphism C X X') (b : morphism C Y Y')
    : morphism C BXY BX'Y'
    := biproduct_prod_mor BX'Y' (a o outl BXY) (b o outr BXY).

  (** The biproduct map composed with the left injection is the left
      summand map. *)
  Lemma biproduct_sum_map_inl
    (a : morphism C X X') (b : morphism C Y Y')
    : biproduct_sum_map a b o inl BXY
      = inl BX'Y' o a.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
biproduct_sum_map a b o inl BXY = inl BX'Y' o a
  Proof.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
biproduct_sum_map a b o inl BXY = inl BX'Y' o a
    rhs_V apply (biproduct_prod_zero_r BX'Y').
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
biproduct_sum_map a b o inl BXY =
biproduct_prod_mor BX'Y' a (zero_morphism X Y')
    rapply (biproduct_prod_unique BX'Y').
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
outl BX'Y' o (biproduct_sum_map a b o inl BXY) = a
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
outr BX'Y' o (biproduct_sum_map a b o inl BXY) = zero_morphism X Y'
    -
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
outl BX'Y' o (biproduct_sum_map a b o inl BXY) = a rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
outl BX'Y' o biproduct_sum_map a b o inl BXY = a
      unfold biproduct_sum_map.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
outl BX'Y' o biproduct_prod_mor BX'Y' (a o outl BXY) (b o outr BXY) o inl BXY =
a
      rewrite (biproduct_prod_beta_l BX'Y').
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
a o outl BXY o inl BXY = a
      rewrite associativity.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
a o (outl BXY o inl BXY) = a
      rewrite (beta_l (biproduct_is BXY)).
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
a o 1 = a
      apply right_identity.
    -
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
outr BX'Y' o (biproduct_sum_map a b o inl BXY) = zero_morphism X Y' rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
outr BX'Y' o biproduct_sum_map a b o inl BXY = zero_morphism X Y'
      unfold biproduct_sum_map.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
outr BX'Y' o biproduct_prod_mor BX'Y' (a o outl BXY) (b o outr BXY) o inl BXY =
zero_morphism X Y'
      rewrite (biproduct_prod_beta_r BX'Y').
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
b o outr BXY o inl BXY = zero_morphism X Y'
      rewrite associativity.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
b o (outr BXY o inl BXY) = zero_morphism X Y'
      rewrite (mixed_r (biproduct_is BXY)).
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
b o zero_morphism X Y = zero_morphism X Y'
      apply zero_morphism_right.
  Qed.

  (** The biproduct map composed with the right injection is the right
      summand map. *)
  Lemma biproduct_sum_map_inr
    (a : morphism C X X') (b : morphism C Y Y')
    : biproduct_sum_map a b o inr BXY
      = inr BX'Y' o b.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
biproduct_sum_map a b o inr BXY = inr BX'Y' o b
  Proof.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
biproduct_sum_map a b o inr BXY = inr BX'Y' o b
    rhs_V apply (biproduct_prod_zero_l BX'Y').
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
biproduct_sum_map a b o inr BXY =
biproduct_prod_mor BX'Y' (zero_morphism Y X') b
    rapply (biproduct_prod_unique BX'Y').
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
outl BX'Y' o (biproduct_sum_map a b o inr BXY) = zero_morphism Y X'
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
outr BX'Y' o (biproduct_sum_map a b o inr BXY) = b
    -
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
outl BX'Y' o (biproduct_sum_map a b o inr BXY) = zero_morphism Y X' rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
outl BX'Y' o biproduct_sum_map a b o inr BXY = zero_morphism Y X'
      unfold biproduct_sum_map.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
outl BX'Y' o biproduct_prod_mor BX'Y' (a o outl BXY) (b o outr BXY) o inr BXY =
zero_morphism Y X'
      rewrite (biproduct_prod_beta_l BX'Y').
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
a o outl BXY o inr BXY = zero_morphism Y X'
      rewrite associativity.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
a o (outl BXY o inr BXY) = zero_morphism Y X'
      rewrite (mixed_l (biproduct_is BXY)).
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
a o zero_morphism Y X = zero_morphism Y X'
      apply zero_morphism_right.
    -
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
outr BX'Y' o (biproduct_sum_map a b o inr BXY) = b rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
outr BX'Y' o biproduct_sum_map a b o inr BXY = b
      unfold biproduct_sum_map.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
outr BX'Y' o biproduct_prod_mor BX'Y' (a o outl BXY) (b o outr BXY) o inr BXY =
b
      rewrite (biproduct_prod_beta_r BX'Y').
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
b o outr BXY o inr BXY = b
      rewrite associativity.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
b o (outr BXY o inr BXY) = b
      rewrite (beta_r (biproduct_is BXY)).
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
a: morphism C X X'
b: morphism C Y Y'
b o 1 = b
      apply right_identity.
  Qed.

  (** Biproduct maps commute with pairing. *)
  Lemma biproduct_sum_map_prod {W : object C}
    (a : morphism C X X') (b : morphism C Y Y')
    (f : morphism C W X) (g : morphism C W Y)
    : biproduct_prod_mor BX'Y' (a o f) (b o g)
      = biproduct_sum_map a b o biproduct_prod_mor BXY f g.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
a: morphism C X X'
b: morphism C Y Y'
f: morphism C W X
g: morphism C W Y
biproduct_prod_mor BX'Y' (a o f) (b o g) =
biproduct_sum_map a b o biproduct_prod_mor BXY f g
  Proof.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
a: morphism C X X'
b: morphism C Y Y'
f: morphism C W X
g: morphism C W Y
biproduct_prod_mor BX'Y' (a o f) (b o g) =
biproduct_sum_map a b o biproduct_prod_mor BXY f g
    symmetry.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
a: morphism C X X'
b: morphism C Y Y'
f: morphism C W X
g: morphism C W Y
biproduct_sum_map a b o biproduct_prod_mor BXY f g =
biproduct_prod_mor BX'Y' (a o f) (b o g)
    rapply (biproduct_prod_unique BX'Y').
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
a: morphism C X X'
b: morphism C Y Y'
f: morphism C W X
g: morphism C W Y
outl BX'Y' o (biproduct_sum_map a b o biproduct_prod_mor BXY f g) = a o f
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
a: morphism C X X'
b: morphism C Y Y'
f: morphism C W X
g: morphism C W Y
outr BX'Y' o (biproduct_sum_map a b o biproduct_prod_mor BXY f g) = b o g
    -
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
a: morphism C X X'
b: morphism C Y Y'
f: morphism C W X
g: morphism C W Y
outl BX'Y' o (biproduct_sum_map a b o biproduct_prod_mor BXY f g) = a o f rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
a: morphism C X X'
b: morphism C Y Y'
f: morphism C W X
g: morphism C W Y
outl BX'Y' o biproduct_sum_map a b o biproduct_prod_mor BXY f g = a o f
      unfold biproduct_sum_map.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
a: morphism C X X'
b: morphism C Y Y'
f: morphism C W X
g: morphism C W Y
outl BX'Y' o biproduct_prod_mor BX'Y' (a o outl BXY) (b o outr BXY)
o biproduct_prod_mor BXY f g = a o f
      rewrite (biproduct_prod_beta_l BX'Y').
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
a: morphism C X X'
b: morphism C Y Y'
f: morphism C W X
g: morphism C W Y
a o outl BXY o biproduct_prod_mor BXY f g = a o f
      rewrite associativity.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
a: morphism C X X'
b: morphism C Y Y'
f: morphism C W X
g: morphism C W Y
a o (outl BXY o biproduct_prod_mor BXY f g) = a o f
      rewrite (biproduct_prod_beta_l BXY).
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
a: morphism C X X'
b: morphism C Y Y'
f: morphism C W X
g: morphism C W Y
a o f = a o f
      reflexivity.
    -
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
a: morphism C X X'
b: morphism C Y Y'
f: morphism C W X
g: morphism C W Y
outr BX'Y' o (biproduct_sum_map a b o biproduct_prod_mor BXY f g) = b o g rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
a: morphism C X X'
b: morphism C Y Y'
f: morphism C W X
g: morphism C W Y
outr BX'Y' o biproduct_sum_map a b o biproduct_prod_mor BXY f g = b o g
      unfold biproduct_sum_map.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
a: morphism C X X'
b: morphism C Y Y'
f: morphism C W X
g: morphism C W Y
outr BX'Y' o biproduct_prod_mor BX'Y' (a o outl BXY) (b o outr BXY)
o biproduct_prod_mor BXY f g = b o g
      rewrite (biproduct_prod_beta_r BX'Y').
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
a: morphism C X X'
b: morphism C Y Y'
f: morphism C W X
g: morphism C W Y
b o outr BXY o biproduct_prod_mor BXY f g = b o g
      rewrite associativity.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
a: morphism C X X'
b: morphism C Y Y'
f: morphism C W X
g: morphism C W Y
b o (outr BXY o biproduct_prod_mor BXY f g) = b o g
      rewrite (biproduct_prod_beta_r BXY).
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
a: morphism C X X'
b: morphism C Y Y'
f: morphism C W X
g: morphism C W Y
b o g = b o g
      reflexivity.
  Qed.

  (** Copairing is natural in the domain with respect to biproduct maps. *)
  Lemma biproduct_coprod_sum_map_nat {W : object C}
    (f : morphism C X' W) (g : morphism C Y' W)
    (a : morphism C X X') (b : morphism C Y Y')
    : biproduct_coprod_mor BX'Y' W f g o biproduct_sum_map a b
      = biproduct_coprod_mor BXY W (f o a) (g o b).
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
f: morphism C X' W
g: morphism C Y' W
a: morphism C X X'
b: morphism C Y Y'
biproduct_coprod_mor BX'Y' W f g o biproduct_sum_map a b =
biproduct_coprod_mor BXY W (f o a) (g o b)
  Proof.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
f: morphism C X' W
g: morphism C Y' W
a: morphism C X X'
b: morphism C Y Y'
biproduct_coprod_mor BX'Y' W f g o biproduct_sum_map a b =
biproduct_coprod_mor BXY W (f o a) (g o b)
    rapply (biproduct_coprod_unique BXY).
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
f: morphism C X' W
g: morphism C Y' W
a: morphism C X X'
b: morphism C Y Y'
biproduct_coprod_mor BX'Y' W f g o biproduct_sum_map a b o inl BXY = f o a
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
f: morphism C X' W
g: morphism C Y' W
a: morphism C X X'
b: morphism C Y Y'
biproduct_coprod_mor BX'Y' W f g o biproduct_sum_map a b o inr BXY = g o b
    -
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
f: morphism C X' W
g: morphism C Y' W
a: morphism C X X'
b: morphism C Y Y'
biproduct_coprod_mor BX'Y' W f g o biproduct_sum_map a b o inl BXY = f o a rewrite associativity.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
f: morphism C X' W
g: morphism C Y' W
a: morphism C X X'
b: morphism C Y Y'
biproduct_coprod_mor BX'Y' W f g o (biproduct_sum_map a b o inl BXY) = f o a
      rewrite biproduct_sum_map_inl.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
f: morphism C X' W
g: morphism C Y' W
a: morphism C X X'
b: morphism C Y Y'
biproduct_coprod_mor BX'Y' W f g o (inl BX'Y' o a) = f o a
      rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
f: morphism C X' W
g: morphism C Y' W
a: morphism C X X'
b: morphism C Y Y'
biproduct_coprod_mor BX'Y' W f g o inl BX'Y' o a = f o a
      rewrite biproduct_coprod_beta_l.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
f: morphism C X' W
g: morphism C Y' W
a: morphism C X X'
b: morphism C Y Y'
f o a = f o a
      reflexivity.
    -
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
f: morphism C X' W
g: morphism C Y' W
a: morphism C X X'
b: morphism C Y Y'
biproduct_coprod_mor BX'Y' W f g o biproduct_sum_map a b o inr BXY = g o b rewrite associativity.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
f: morphism C X' W
g: morphism C Y' W
a: morphism C X X'
b: morphism C Y Y'
biproduct_coprod_mor BX'Y' W f g o (biproduct_sum_map a b o inr BXY) = g o b
      rewrite biproduct_sum_map_inr.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
f: morphism C X' W
g: morphism C Y' W
a: morphism C X X'
b: morphism C Y Y'
biproduct_coprod_mor BX'Y' W f g o (inr BX'Y' o b) = g o b
      rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
f: morphism C X' W
g: morphism C Y' W
a: morphism C X X'
b: morphism C Y Y'
biproduct_coprod_mor BX'Y' W f g o inr BX'Y' o b = g o b
      rewrite biproduct_coprod_beta_r.
C: PreCategory
Z: ZeroObject C
X, Y, X', Y': C
BXY: Biproduct Z X Y
BX'Y': Biproduct Z X' Y'
W: C
f: morphism C X' W
g: morphism C Y' W
a: morphism C X X'
b: morphism C Y Y'
g o b = g o b
      reflexivity.
  Qed.

End BiproductFunctoriality.

(** * Symmetry of biproducts *)

Section BiproductSymmetry.
  Context {C : PreCategory} {Z : ZeroObject C} {X Y : object C}
    {BXY : Biproduct Z X Y} {BYX : Biproduct Z Y X}.

  (** The swap morphism exchanges the two summands of a biproduct. *)
  Definition biproduct_swap
    : morphism C BXY BYX
    := biproduct_prod_mor BYX (outr BXY) (outl BXY).

  (** Swapping the components of a pairing. *)
  Lemma biproduct_prod_swap {W : object C}
    (f : morphism C W X) (g : morphism C W Y)
    : biproduct_prod_mor BYX g f
      = biproduct_swap o biproduct_prod_mor BXY f g.
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
W: C
f: morphism C W X
g: morphism C W Y
biproduct_prod_mor BYX g f = biproduct_swap o biproduct_prod_mor BXY f g
  Proof.
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
W: C
f: morphism C W X
g: morphism C W Y
biproduct_prod_mor BYX g f = biproduct_swap o biproduct_prod_mor BXY f g
    symmetry.
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
W: C
f: morphism C W X
g: morphism C W Y
biproduct_swap o biproduct_prod_mor BXY f g = biproduct_prod_mor BYX g f
    rapply (biproduct_prod_unique BYX).
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
W: C
f: morphism C W X
g: morphism C W Y
outl BYX o (biproduct_swap o biproduct_prod_mor BXY f g) = g
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
W: C
f: morphism C W X
g: morphism C W Y
outr BYX o (biproduct_swap o biproduct_prod_mor BXY f g) = f
    -
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
W: C
f: morphism C W X
g: morphism C W Y
outl BYX o (biproduct_swap o biproduct_prod_mor BXY f g) = g rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
W: C
f: morphism C W X
g: morphism C W Y
outl BYX o biproduct_swap o biproduct_prod_mor BXY f g = g
      unfold biproduct_swap.
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
W: C
f: morphism C W X
g: morphism C W Y
outl BYX o biproduct_prod_mor BYX (outr BXY) (outl BXY)
o biproduct_prod_mor BXY f g = g
      rewrite (biproduct_prod_beta_l BYX).
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
W: C
f: morphism C W X
g: morphism C W Y
outr BXY o biproduct_prod_mor BXY f g = g
      apply (biproduct_prod_beta_r BXY).
    -
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
W: C
f: morphism C W X
g: morphism C W Y
outr BYX o (biproduct_swap o biproduct_prod_mor BXY f g) = f rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
W: C
f: morphism C W X
g: morphism C W Y
outr BYX o biproduct_swap o biproduct_prod_mor BXY f g = f
      unfold biproduct_swap.
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
W: C
f: morphism C W X
g: morphism C W Y
outr BYX o biproduct_prod_mor BYX (outr BXY) (outl BXY)
o biproduct_prod_mor BXY f g = f
      rewrite (biproduct_prod_beta_r BYX).
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
W: C
f: morphism C W X
g: morphism C W Y
outl BXY o biproduct_prod_mor BXY f g = f
      apply (biproduct_prod_beta_l BXY).
  Qed.

  (** Swapping after the left injection gives the right injection. *)
  Lemma biproduct_swap_inl
    : biproduct_swap o inl BXY = inr BYX.
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
biproduct_swap o inl BXY = inr BYX
  Proof.
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
biproduct_swap o inl BXY = inr BYX
    unfold biproduct_swap.
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
biproduct_prod_mor BYX (outr BXY) (outl BXY) o inl BXY = inr BYX
    rewrite (biproduct_prod_mor_nat BYX).
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
biproduct_prod_mor BYX (outr BXY o inl BXY) (outl BXY o inl BXY) = inr BYX
    rewrite (mixed_r (biproduct_is BXY)).
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
biproduct_prod_mor BYX (zero_morphism X Y) (outl BXY o inl BXY) = inr BYX
    rewrite (beta_l (biproduct_is BXY)).
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
biproduct_prod_mor BYX (zero_morphism X Y) 1 = inr BYX
    rewrite (biproduct_prod_zero_l BYX).
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
inr BYX o 1 = inr BYX
    apply right_identity.
  Qed.

  (** Swapping after the right injection gives the left injection. *)
  Lemma biproduct_swap_inr
    : biproduct_swap o inr BXY = inl BYX.
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
biproduct_swap o inr BXY = inl BYX
  Proof.
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
biproduct_swap o inr BXY = inl BYX
    unfold biproduct_swap.
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
biproduct_prod_mor BYX (outr BXY) (outl BXY) o inr BXY = inl BYX
    rewrite (biproduct_prod_mor_nat BYX).
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
biproduct_prod_mor BYX (outr BXY o inr BXY) (outl BXY o inr BXY) = inl BYX
    rewrite (beta_r (biproduct_is BXY)).
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
biproduct_prod_mor BYX 1 (outl BXY o inr BXY) = inl BYX
    rewrite (mixed_l (biproduct_is BXY)).
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
biproduct_prod_mor BYX 1 (zero_morphism Y X) = inl BYX
    rewrite (biproduct_prod_zero_r BYX).
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
inl BYX o 1 = inl BYX
    apply right_identity.
  Qed.

End BiproductSymmetry.

(** Swapping twice is the identity, so [BXY] and [BYX] are isomorphic:
    the biproduct is commutative. *)
Lemma biproduct_swap_swap {C : PreCategory} {Z : ZeroObject C}
  {X Y : object C} {BXY : Biproduct Z X Y} {BYX : Biproduct Z Y X}
  : biproduct_swap (BXY:=BYX) (BYX:=BXY) o biproduct_swap = 1.
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
biproduct_swap o biproduct_swap = 1
Proof.
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
biproduct_swap o biproduct_swap = 1
  transitivity (biproduct_prod_mor BXY (outl BXY) (outr BXY)).
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
biproduct_swap o biproduct_swap =
biproduct_prod_mor BXY (outl BXY) (outr BXY)
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
biproduct_prod_mor BXY (outl BXY) (outr BXY) = 1
  -
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
biproduct_swap o biproduct_swap =
biproduct_prod_mor BXY (outl BXY) (outr BXY) rapply (biproduct_prod_unique BXY).
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
outl BXY o (biproduct_swap o biproduct_swap) = outl BXY
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
outr BXY o (biproduct_swap o biproduct_swap) = outr BXY
    +
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
outl BXY o (biproduct_swap o biproduct_swap) = outl BXY rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
outl BXY o biproduct_swap o biproduct_swap = outl BXY
      unfold biproduct_swap at 1.
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
outl BXY o biproduct_prod_mor BXY (outr BYX) (outl BYX) o biproduct_swap =
outl BXY
      rewrite (biproduct_prod_beta_l BXY).
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
outr BYX o biproduct_swap = outl BXY
      apply (biproduct_prod_beta_r BYX).
    +
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
outr BXY o (biproduct_swap o biproduct_swap) = outr BXY rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
outr BXY o biproduct_swap o biproduct_swap = outr BXY
      unfold biproduct_swap at 1.
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
outr BXY o biproduct_prod_mor BXY (outr BYX) (outl BYX) o biproduct_swap =
outr BXY
      rewrite (biproduct_prod_beta_r BXY).
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
outl BYX o biproduct_swap = outr BXY
      apply (biproduct_prod_beta_l BYX).
  -
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
biproduct_prod_mor BXY (outl BXY) (outr BXY) = 1 symmetry.
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
1 = biproduct_prod_mor BXY (outl BXY) (outr BXY)
    rapply (biproduct_prod_unique BXY).
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
outl BXY o 1 = outl BXY
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
outr BXY o 1 = outr BXY
    +
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
outl BXY o 1 = outl BXY apply right_identity.
    +
C: PreCategory
Z: ZeroObject C
X, Y: C
BXY: Biproduct Z X Y
BYX: Biproduct Z Y X
outr BXY o 1 = outr BXY apply right_identity.
Qed.

(** * Self-biproducts *)

Section SelfBiproducts.
  Context {C : PreCategory} {Z : ZeroObject C}.

  (** The codiagonal of a self-biproduct. *)
  Definition biproduct_codiagonal (Y : object C)
    {BYY : Biproduct Z Y Y}
    : morphism C BYY Y
    := biproduct_coprod_mor BYY Y 1 1.

  (** The codiagonal is natural in the codomain. *)
  Lemma biproduct_codiagonal_nat {Y Y' : object C}
    {BYY : Biproduct Z Y Y}
    (a : morphism C Y Y')
    : a o biproduct_codiagonal Y
      = biproduct_coprod_mor BYY Y' a a.
C: PreCategory
Z: ZeroObject C
Y, Y': C
BYY: Biproduct Z Y Y
a: morphism C Y Y'
a o biproduct_codiagonal Y = biproduct_coprod_mor BYY Y' a a
  Proof.
C: PreCategory
Z: ZeroObject C
Y, Y': C
BYY: Biproduct Z Y Y
a: morphism C Y Y'
a o biproduct_codiagonal Y = biproduct_coprod_mor BYY Y' a a
    unfold biproduct_codiagonal.
C: PreCategory
Z: ZeroObject C
Y, Y': C
BYY: Biproduct Z Y Y
a: morphism C Y Y'
a o biproduct_coprod_mor BYY Y 1 1 = biproduct_coprod_mor BYY Y' a a
    rewrite biproduct_coprod_mor_nat.
C: PreCategory
Z: ZeroObject C
Y, Y': C
BYY: Biproduct Z Y Y
a: morphism C Y Y'
biproduct_coprod_mor BYY Y' (a o 1) (a o 1) = biproduct_coprod_mor BYY Y' a a
    repeat rewrite right_identity.
C: PreCategory
Z: ZeroObject C
Y, Y': C
BYY: Biproduct Z Y Y
a: morphism C Y Y'
biproduct_coprod_mor BYY Y' a a = biproduct_coprod_mor BYY Y' a a
    reflexivity.
  Qed.

  (** The codiagonal of a biproduct map is the corresponding copairing. *)
  Lemma biproduct_codiagonal_factor_through_sum_map {Y Y' : object C}
    {BYY : Biproduct Z Y Y} {BYY' : Biproduct Z Y' Y'}
    (a b : morphism C Y Y')
    : biproduct_codiagonal Y' o biproduct_sum_map a b
      = biproduct_coprod_mor BYY Y' a b.
C: PreCategory
Z: ZeroObject C
Y, Y': C
BYY: Biproduct Z Y Y
BYY': Biproduct Z Y' Y'
a, b: morphism C Y Y'
biproduct_codiagonal Y' o biproduct_sum_map a b =
biproduct_coprod_mor BYY Y' a b
  Proof.
C: PreCategory
Z: ZeroObject C
Y, Y': C
BYY: Biproduct Z Y Y
BYY': Biproduct Z Y' Y'
a, b: morphism C Y Y'
biproduct_codiagonal Y' o biproduct_sum_map a b =
biproduct_coprod_mor BYY Y' a b
    unfold biproduct_codiagonal.
C: PreCategory
Z: ZeroObject C
Y, Y': C
BYY: Biproduct Z Y Y
BYY': Biproduct Z Y' Y'
a, b: morphism C Y Y'
biproduct_coprod_mor BYY' Y' 1 1 o biproduct_sum_map a b =
biproduct_coprod_mor BYY Y' a b
    rewrite biproduct_coprod_sum_map_nat.
C: PreCategory
Z: ZeroObject C
Y, Y': C
BYY: Biproduct Z Y Y
BYY': Biproduct Z Y' Y'
a, b: morphism C Y Y'
biproduct_coprod_mor BYY Y' (1 o a) (1 o b) = biproduct_coprod_mor BYY Y' a b
    rewrite !left_identity.
C: PreCategory
Z: ZeroObject C
Y, Y': C
BYY: Biproduct Z Y Y
BYY': Biproduct Z Y' Y'
a, b: morphism C Y Y'
biproduct_coprod_mor BYY Y' a b = biproduct_coprod_mor BYY Y' a b
    reflexivity.
  Qed.

  (** The codiagonal of a pairing with zero on the right recovers the
      left map. *)
  Lemma biproduct_codiagonal_prod_zero_r {X Y : object C}
    {BYY : Biproduct Z Y Y}
    (f : morphism C X Y)
    : biproduct_codiagonal Y
       o biproduct_prod_mor BYY f (zero_morphism X Y) = f.
C: PreCategory
Z: ZeroObject C
X, Y: C
BYY: Biproduct Z Y Y
f: morphism C X Y
biproduct_codiagonal Y o biproduct_prod_mor BYY f (zero_morphism X Y) = f
  Proof.
C: PreCategory
Z: ZeroObject C
X, Y: C
BYY: Biproduct Z Y Y
f: morphism C X Y
biproduct_codiagonal Y o biproduct_prod_mor BYY f (zero_morphism X Y) = f
    unfold biproduct_codiagonal.
C: PreCategory
Z: ZeroObject C
X, Y: C
BYY: Biproduct Z Y Y
f: morphism C X Y
biproduct_coprod_mor BYY Y 1 1 o biproduct_prod_mor BYY f (zero_morphism X Y) =
f
    rewrite biproduct_prod_zero_r.
C: PreCategory
Z: ZeroObject C
X, Y: C
BYY: Biproduct Z Y Y
f: morphism C X Y
biproduct_coprod_mor BYY Y 1 1 o (inl BYY o f) = f
    rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y: C
BYY: Biproduct Z Y Y
f: morphism C X Y
biproduct_coprod_mor BYY Y 1 1 o inl BYY o f = f
    rewrite biproduct_coprod_beta_l.
C: PreCategory
Z: ZeroObject C
X, Y: C
BYY: Biproduct Z Y Y
f: morphism C X Y
1 o f = f
    apply left_identity.
  Qed.

  (** The codiagonal of a pairing with zero on the left recovers the
      right map. *)
  Lemma biproduct_codiagonal_prod_zero_l {X Y : object C}
    {BYY : Biproduct Z Y Y}
    (f : morphism C X Y)
    : biproduct_codiagonal Y
       o biproduct_prod_mor BYY (zero_morphism X Y) f = f.
C: PreCategory
Z: ZeroObject C
X, Y: C
BYY: Biproduct Z Y Y
f: morphism C X Y
biproduct_codiagonal Y o biproduct_prod_mor BYY (zero_morphism X Y) f = f
  Proof.
C: PreCategory
Z: ZeroObject C
X, Y: C
BYY: Biproduct Z Y Y
f: morphism C X Y
biproduct_codiagonal Y o biproduct_prod_mor BYY (zero_morphism X Y) f = f
    unfold biproduct_codiagonal.
C: PreCategory
Z: ZeroObject C
X, Y: C
BYY: Biproduct Z Y Y
f: morphism C X Y
biproduct_coprod_mor BYY Y 1 1 o biproduct_prod_mor BYY (zero_morphism X Y) f =
f
    rewrite biproduct_prod_zero_l.
C: PreCategory
Z: ZeroObject C
X, Y: C
BYY: Biproduct Z Y Y
f: morphism C X Y
biproduct_coprod_mor BYY Y 1 1 o (inr BYY o f) = f
    rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y: C
BYY: Biproduct Z Y Y
f: morphism C X Y
biproduct_coprod_mor BYY Y 1 1 o inr BYY o f = f
    rewrite biproduct_coprod_beta_r.
C: PreCategory
Z: ZeroObject C
X, Y: C
BYY: Biproduct Z Y Y
f: morphism C X Y
1 o f = f
    apply left_identity.
  Qed.

  (** The codiagonal is invariant under swapping the two summands. *)
  Lemma biproduct_codiagonal_swap_invariant {Y : object C}
    {BYY : Biproduct Z Y Y}
    : biproduct_codiagonal Y o biproduct_swap
      = biproduct_codiagonal Y.
C: PreCategory
Z: ZeroObject C
Y: C
BYY: Biproduct Z Y Y
biproduct_codiagonal Y o biproduct_swap = biproduct_codiagonal Y
  Proof.
C: PreCategory
Z: ZeroObject C
Y: C
BYY: Biproduct Z Y Y
biproduct_codiagonal Y o biproduct_swap = biproduct_codiagonal Y
    rapply (biproduct_coprod_unique BYY Y 1 1).
C: PreCategory
Z: ZeroObject C
Y: C
BYY: Biproduct Z Y Y
biproduct_codiagonal Y o biproduct_swap o inl BYY = 1
C: PreCategory
Z: ZeroObject C
Y: C
BYY: Biproduct Z Y Y
biproduct_codiagonal Y o biproduct_swap o inr BYY = 1
    -
C: PreCategory
Z: ZeroObject C
Y: C
BYY: Biproduct Z Y Y
biproduct_codiagonal Y o biproduct_swap o inl BYY = 1 rewrite associativity.
C: PreCategory
Z: ZeroObject C
Y: C
BYY: Biproduct Z Y Y
biproduct_codiagonal Y o (biproduct_swap o inl BYY) = 1
      rewrite biproduct_swap_inl.
C: PreCategory
Z: ZeroObject C
Y: C
BYY: Biproduct Z Y Y
biproduct_codiagonal Y o inr BYY = 1
      apply biproduct_coprod_beta_r.
    -
C: PreCategory
Z: ZeroObject C
Y: C
BYY: Biproduct Z Y Y
biproduct_codiagonal Y o biproduct_swap o inr BYY = 1 rewrite associativity.
C: PreCategory
Z: ZeroObject C
Y: C
BYY: Biproduct Z Y Y
biproduct_codiagonal Y o (biproduct_swap o inr BYY) = 1
      rewrite biproduct_swap_inr.
C: PreCategory
Z: ZeroObject C
Y: C
BYY: Biproduct Z Y Y
biproduct_codiagonal Y o inl BYY = 1
      apply biproduct_coprod_beta_l.
  Qed.

End SelfBiproducts.

(** * Export hints *)

Hint Resolve
  biproduct_coprod_beta_l biproduct_coprod_beta_r
  biproduct_prod_beta_l biproduct_prod_beta_r
  : biproduct.

Hint Rewrite
  @zero_morphism_left @zero_morphism_right
  : biproduct_simplify.