(** * Semi-additive categories

    Categories with zero objects and biproducts, which automatically
    have commutative monoid structures on hom-sets. *)

From HoTT Require Import Basics.Overture Basics.PathGroupoids Basics.Tactics.
From HoTT.Classes.interfaces Require Import abstract_algebra.
From HoTT.Categories Require Import Category.Core.
From HoTT.Categories.Additive Require Import ZeroObjects Biproducts.

Local Open Scope morphism_scope.

(** This lets us use "+" for the [SgOp] instance and "0" for the [MonUnit]
    instance defined below. *)
Local Open Scope mc_add_scope.

(** ** Definition of semi-additive category *)

Class SemiAdditiveCategory := {
  cat : PreCategory;
  semiadditive_zero :: ZeroObject cat;
  semiadditive_biproduct :: forall (X Y : object cat),
    Biproduct semiadditive_zero X Y
}.

Coercion cat : SemiAdditiveCategory >-> PreCategory.

(** Notation for biproduct objects *)
Local Notation "X ⊕ Y" := (semiadditive_biproduct X Y).

(** ** Morphism addition via biproducts

    Addition is the codiagonal composed with the pairing morphism. *)

Section MorphismAddition.
  Context {C : SemiAdditiveCategory} {X Y : object C}.

  (** Codiagonal composed with pairing. *)
  #[export] Instance sgop_morphism : SgOp (morphism C X Y)
    := fun f g =>
        biproduct_codiagonal Y o biproduct_prod_mor (Y ⊕ Y) f g.

  (** The zero morphism is the unit for addition. *)
  #[export] Instance monunit_morphism : MonUnit (morphism C X Y)
    := zero_morphism X Y.

End MorphismAddition.

(** ** Identity laws for morphism addition *)

Section IdentityLaws.
  Context {C : SemiAdditiveCategory}.

  (** Zero is a left identity for morphism addition. *)
  Definition zero_left_identity {X Y : object C} (f : morphism C X Y)
    : 0 + f = f
    := biproduct_codiagonal_prod_zero_l f.

  (** Zero is a right identity for morphism addition. *)
  Definition zero_right_identity {X Y : object C} (f : morphism C X Y)
    : f + 0 = f
    := biproduct_codiagonal_prod_zero_r f.

End IdentityLaws.

(** ** Commutativity of morphism addition *)

Theorem morphism_addition_commutative {C : SemiAdditiveCategory}
  {X Y : object C}
  : Commutative (@sgop_morphism C X Y).
C: SemiAdditiveCategory
X, Y: C
Commutative sgop_morphism
Proof.
C: SemiAdditiveCategory
X, Y: C
Commutative sgop_morphism
  intros f g.
C: SemiAdditiveCategory
X, Y: C
f, g: morphism C X Y
sgop_morphism f g = sgop_morphism g f
  unfold sgop_morphism.
C: SemiAdditiveCategory
X, Y: C
f, g: morphism C X Y
biproduct_codiagonal Y o biproduct_prod_mor (Y ⊕ Y) f g =
biproduct_codiagonal Y o biproduct_prod_mor (Y ⊕ Y) g f
  rewrite (biproduct_prod_swap f g).
C: SemiAdditiveCategory
X, Y: C
f, g: morphism C X Y
biproduct_codiagonal Y o biproduct_prod_mor (Y ⊕ Y) f g =
biproduct_codiagonal Y o (biproduct_swap o biproduct_prod_mor (Y ⊕ Y) f g)
  rewrite <- associativity.
C: SemiAdditiveCategory
X, Y: C
f, g: morphism C X Y
biproduct_codiagonal Y o biproduct_prod_mor (Y ⊕ Y) f g =
biproduct_codiagonal Y o biproduct_swap o biproduct_prod_mor (Y ⊕ Y) f g
  rewrite biproduct_codiagonal_swap_invariant.
C: SemiAdditiveCategory
X, Y: C
f, g: morphism C X Y
biproduct_codiagonal Y o biproduct_prod_mor (Y ⊕ Y) f g =
biproduct_codiagonal Y o biproduct_prod_mor (Y ⊕ Y) f g
  reflexivity.
Qed.

(** ** Associativity of morphism addition *)

Section Associativity.
  Context {C : SemiAdditiveCategory}.

  (** Addition is natural in the domain. *)
  Lemma addition_precompose {X Y W : object C}
    (f g : morphism C X Y) (a : morphism C W X)
    : (f + g) o a = (f o a) + (g o a).
C: SemiAdditiveCategory
X, Y, W: C
f, g: morphism C X Y
a: morphism C W X
(f + g) o a = f o a + g o a
  Proof.
C: SemiAdditiveCategory
X, Y, W: C
f, g: morphism C X Y
a: morphism C W X
(f + g) o a = f o a + g o a
    unfold sg_op, sgop_morphism.
C: SemiAdditiveCategory
X, Y, W: C
f, g: morphism C X Y
a: morphism C W X
biproduct_codiagonal Y o biproduct_prod_mor (Y ⊕ Y) f g o a =
biproduct_codiagonal Y o biproduct_prod_mor (Y ⊕ Y) (f o a) (g o a)
    rewrite associativity.
C: SemiAdditiveCategory
X, Y, W: C
f, g: morphism C X Y
a: morphism C W X
biproduct_codiagonal Y o (biproduct_prod_mor (Y ⊕ Y) f g o a) =
biproduct_codiagonal Y o biproduct_prod_mor (Y ⊕ Y) (f o a) (g o a)
    apply ap, biproduct_prod_mor_nat.
  Qed.

  (** Addition is natural in the codomain. *)
  Lemma addition_postcompose {X Y Y' : object C}
    (f g : morphism C X Y) (a : morphism C Y Y')
    : a o (f + g) = (a o f) + (a o g).
C: SemiAdditiveCategory
X, Y, Y': C
f, g: morphism C X Y
a: morphism C Y Y'
a o (f + g) = a o f + a o g
  Proof.
C: SemiAdditiveCategory
X, Y, Y': C
f, g: morphism C X Y
a: morphism C Y Y'
a o (f + g) = a o f + a o g
    unfold sg_op, sgop_morphism.
C: SemiAdditiveCategory
X, Y, Y': C
f, g: morphism C X Y
a: morphism C Y Y'
a o (biproduct_codiagonal Y o biproduct_prod_mor (Y ⊕ Y) f g) =
biproduct_codiagonal Y' o biproduct_prod_mor (Y' ⊕ Y') (a o f) (a o g)
    rewrite <- associativity.
C: SemiAdditiveCategory
X, Y, Y': C
f, g: morphism C X Y
a: morphism C Y Y'
a o biproduct_codiagonal Y o biproduct_prod_mor (Y ⊕ Y) f g =
biproduct_codiagonal Y' o biproduct_prod_mor (Y' ⊕ Y') (a o f) (a o g)
    rewrite (biproduct_codiagonal_nat a).
C: SemiAdditiveCategory
X, Y, Y': C
f, g: morphism C X Y
a: morphism C Y Y'
biproduct_coprod_mor (Y ⊕ Y) Y' a a o biproduct_prod_mor (Y ⊕ Y) f g =
biproduct_codiagonal Y' o biproduct_prod_mor (Y' ⊕ Y') (a o f) (a o g)
    rewrite <- (biproduct_codiagonal_factor_through_sum_map a a).
C: SemiAdditiveCategory
X, Y, Y': C
f, g: morphism C X Y
a: morphism C Y Y'
biproduct_codiagonal Y' o biproduct_sum_map a a
o biproduct_prod_mor (Y ⊕ Y) f g =
biproduct_codiagonal Y' o biproduct_prod_mor (Y' ⊕ Y') (a o f) (a o g)
    rewrite associativity.
C: SemiAdditiveCategory
X, Y, Y': C
f, g: morphism C X Y
a: morphism C Y Y'
biproduct_codiagonal Y'
o (biproduct_sum_map a a o biproduct_prod_mor (Y ⊕ Y) f g) =
biproduct_codiagonal Y' o biproduct_prod_mor (Y' ⊕ Y') (a o f) (a o g)
    rewrite <- (biproduct_sum_map_prod a a f g).
C: SemiAdditiveCategory
X, Y, Y': C
f, g: morphism C X Y
a: morphism C Y Y'
biproduct_codiagonal Y' o biproduct_prod_mor (Y' ⊕ Y') (a o f) (a o g) =
biproduct_codiagonal Y' o biproduct_prod_mor (Y' ⊕ Y') (a o f) (a o g)
    reflexivity.
  Qed.

  (** Sum of pairings is the pairing of the sums. *)
  Lemma addition_of_pairs {X Y Y' : object C}
    (f1 f2 : morphism C X Y) (g1 g2 : morphism C X Y')
    : biproduct_prod_mor (Y ⊕ Y') f1 g1 + biproduct_prod_mor (Y ⊕ Y') f2 g2
      = biproduct_prod_mor (Y ⊕ Y') (f1 + f2) (g1 + g2).
C: SemiAdditiveCategory
X, Y, Y': C
f1, f2: morphism C X Y
g1, g2: morphism C X Y'
biproduct_prod_mor (Y ⊕ Y') f1 g1 + biproduct_prod_mor (Y ⊕ Y') f2 g2 =
biproduct_prod_mor (Y ⊕ Y') (f1 + f2) (g1 + g2)
  Proof.
C: SemiAdditiveCategory
X, Y, Y': C
f1, f2: morphism C X Y
g1, g2: morphism C X Y'
biproduct_prod_mor (Y ⊕ Y') f1 g1 + biproduct_prod_mor (Y ⊕ Y') f2 g2 =
biproduct_prod_mor (Y ⊕ Y') (f1 + f2) (g1 + g2)
    rapply biproduct_prod_unique.
C: SemiAdditiveCategory
X, Y, Y': C
f1, f2: morphism C X Y
g1, g2: morphism C X Y'
outl (Y ⊕ Y')
o (biproduct_prod_mor (Y ⊕ Y') f1 g1 + biproduct_prod_mor (Y ⊕ Y') f2 g2) =
f1 + f2
C: SemiAdditiveCategory
X, Y, Y': C
f1, f2: morphism C X Y
g1, g2: morphism C X Y'
outr (Y ⊕ Y')
o (biproduct_prod_mor (Y ⊕ Y') f1 g1 + biproduct_prod_mor (Y ⊕ Y') f2 g2) =
g1 + g2
    -
C: SemiAdditiveCategory
X, Y, Y': C
f1, f2: morphism C X Y
g1, g2: morphism C X Y'
outl (Y ⊕ Y')
o (biproduct_prod_mor (Y ⊕ Y') f1 g1 + biproduct_prod_mor (Y ⊕ Y') f2 g2) =
f1 + f2 rewrite addition_postcompose.
C: SemiAdditiveCategory
X, Y, Y': C
f1, f2: morphism C X Y
g1, g2: morphism C X Y'
outl (Y ⊕ Y') o biproduct_prod_mor (Y ⊕ Y') f1 g1 +
outl (Y ⊕ Y') o biproduct_prod_mor (Y ⊕ Y') f2 g2 = 
f1 + f2
      rewrite 2 biproduct_prod_beta_l.
C: SemiAdditiveCategory
X, Y, Y': C
f1, f2: morphism C X Y
g1, g2: morphism C X Y'
f1 + f2 = f1 + f2
      reflexivity.
    -
C: SemiAdditiveCategory
X, Y, Y': C
f1, f2: morphism C X Y
g1, g2: morphism C X Y'
outr (Y ⊕ Y')
o (biproduct_prod_mor (Y ⊕ Y') f1 g1 + biproduct_prod_mor (Y ⊕ Y') f2 g2) =
g1 + g2 rewrite addition_postcompose.
C: SemiAdditiveCategory
X, Y, Y': C
f1, f2: morphism C X Y
g1, g2: morphism C X Y'
outr (Y ⊕ Y') o biproduct_prod_mor (Y ⊕ Y') f1 g1 +
outr (Y ⊕ Y') o biproduct_prod_mor (Y ⊕ Y') f2 g2 = 
g1 + g2
      rewrite 2 biproduct_prod_beta_r.
C: SemiAdditiveCategory
X, Y, Y': C
f1, f2: morphism C X Y
g1, g2: morphism C X Y'
g1 + g2 = g1 + g2
      reflexivity.
  Qed.

  (** Associativity follows by functoriality of pairing and codiagonal. *)
  Theorem morphism_addition_associative {X Y : object C}
    (f g h : morphism C X Y)
    : f + (g + h) = (f + g) + h.
C: SemiAdditiveCategory
X, Y: C
f, g, h: morphism C X Y
f + (g + h) = f + g + h
  Proof.
C: SemiAdditiveCategory
X, Y: C
f, g, h: morphism C X Y
f + (g + h) = f + g + h
    lhs_V exact (ap (fun w => w + (g + h)) (zero_right_identity f)).
C: SemiAdditiveCategory
X, Y: C
f, g, h: morphism C X Y
f + 0 + (g + h) = f + g + h
    lhs_V exact (ap (fun p => biproduct_codiagonal Y o p)
                   (addition_of_pairs f 0 g h)).
C: SemiAdditiveCategory
X, Y: C
f, g, h: morphism C X Y
biproduct_codiagonal Y
o (biproduct_prod_mor (Y ⊕ Y) f g + biproduct_prod_mor (Y ⊕ Y) 0 h) =
f + g + h
    lhs napply addition_postcompose.
C: SemiAdditiveCategory
X, Y: C
f, g, h: morphism C X Y
biproduct_codiagonal Y o biproduct_prod_mor (Y ⊕ Y) f g +
biproduct_codiagonal Y o biproduct_prod_mor (Y ⊕ Y) 0 h = 
f + g + h
    exact (ap (fun w => (f + g) + w) (zero_left_identity h)).
  Qed.

End Associativity.

(** ** Main theorem: morphism sets form commutative monoids *)

#[export] Instance is_commutative_monoid_morphisms
  (C : SemiAdditiveCategory) (X Y : object C)
  : IsCommutativeMonoid (morphism C X Y).
C: SemiAdditiveCategory
X, Y: C
IsCommutativeMonoid (morphism C X Y)
Proof.
C: SemiAdditiveCategory
X, Y: C
IsCommutativeMonoid (morphism C X Y)
  repeat split.
C: SemiAdditiveCategory
X, Y: C
IsHSet (morphism C X Y)
C: SemiAdditiveCategory
X, Y: C
Associative sg_op
C: SemiAdditiveCategory
X, Y: C
LeftIdentity sg_op 0
C: SemiAdditiveCategory
X, Y: C
RightIdentity sg_op 0
C: SemiAdditiveCategory
X, Y: C
Commutative sg_op
  -
C: SemiAdditiveCategory
X, Y: C
IsHSet (morphism C X Y) exact _.
  -
C: SemiAdditiveCategory
X, Y: C
Associative sg_op exact morphism_addition_associative.
  -
C: SemiAdditiveCategory
X, Y: C
LeftIdentity sg_op 0 exact zero_left_identity.
  -
C: SemiAdditiveCategory
X, Y: C
RightIdentity sg_op 0 exact zero_right_identity.
  -
C: SemiAdditiveCategory
X, Y: C
Commutative sg_op exact morphism_addition_commutative.
Defined.

(** ** Uniqueness of the enrichment

    The canonical addition is the unique family of operations on hom-sets
    with units that distributes over composition.  Commutativity and
    associativity of [op] are not assumed; they follow from uniqueness. *)

Section EnrichmentUniqueness.
  Context {C : SemiAdditiveCategory}
    (op : forall (X Y : object C), morphism C X Y -> morphism C X Y -> morphism C X Y)
    (op_zero : forall (X Y : object C), morphism C X Y)
    (op_zero_l : forall (X Y : object C) (f : morphism C X Y),
      op X Y (op_zero X Y) f = f)
    (op_zero_r : forall (X Y : object C) (f : morphism C X Y),
      op X Y f (op_zero X Y) = f)
    (op_postcompose : forall (X Y Z : object C)
      (h : morphism C Y Z) (f g : morphism C X Y),
      h o op X Y f g = op X Z (h o f) (h o g))
    (op_precompose : forall (X Y Z : object C)
      (f g : morphism C Y Z) (h : morphism C X Y),
      op Y Z f g o h = op X Z (f o h) (g o h))
    (op_zero_postcompose : forall (X Y Z : object C) (h : morphism C Y Z),
      h o op_zero X Y = op_zero X Z).

  (** The unit of any such operation is the zero morphism. *)
  Lemma op_zero_unique (X Y : object C)
    : op_zero X Y = zero_morphism X Y.
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f = f
op_zero_r: forall (X0 Y0 : C) (f : morphism C X0 Y0), op X0 Y0 f (op_zero X0 Y0) = f
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f g : morphism C X0 Y0),
h o op X0 Y0 f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y0 Z : C) (f g : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
op_zero X Y = zero_morphism X Y
  Proof.
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f = f
op_zero_r: forall (X0 Y0 : C) (f : morphism C X0 Y0), op X0 Y0 f (op_zero X0 Y0) = f
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f g : morphism C X0 Y0),
h o op X0 Y0 f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y0 Z : C) (f g : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
op_zero X Y = zero_morphism X Y
    lhs_V apply (op_zero_postcompose X semiadditive_zero Y
      (zero_morphism semiadditive_zero Y)).
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f = f
op_zero_r: forall (X0 Y0 : C) (f : morphism C X0 Y0), op X0 Y0 f (op_zero X0 Y0) = f
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f g : morphism C X0 Y0),
h o op X0 Y0 f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y0 Z : C) (f g : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
zero_morphism semiadditive_zero Y o op_zero X semiadditive_zero =
zero_morphism X Y
    apply morphism_through_zero_is_zero.
  Qed.

  (** Any such operation decomposes the identity of a self-biproduct. *)
  Lemma op_decompose_id (X : object C)
    : op (X ⊕ X) (X ⊕ X)
        (inl (X ⊕ X) o outl (X ⊕ X))
        (inr (X ⊕ X) o outr (X ⊕ X))
      = 1.
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
op (X ⊕ X) (X ⊕ X) (inl (X ⊕ X) o outl (X ⊕ X)) (inr (X ⊕ X) o outr (X ⊕ X)) =
1
  Proof.
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
op (X ⊕ X) (X ⊕ X) (inl (X ⊕ X) o outl (X ⊕ X)) (inr (X ⊕ X) o outr (X ⊕ X)) =
1
    set (B := X ⊕ X).
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
op B B (inl B o outl B) (inr B o outr B) = 1
    transitivity (biproduct_prod_mor B (outl B) (outr B)).
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
op B B (inl B o outl B) (inr B o outr B) =
biproduct_prod_mor B (outl B) (outr B)
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
biproduct_prod_mor B (outl B) (outr B) = 1
    -
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
op B B (inl B o outl B) (inr B o outr B) =
biproduct_prod_mor B (outl B) (outr B) apply (biproduct_prod_unique B).
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
outl B o op B B (inl B o outl B) (inr B o outr B) = outl B
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
outr B o op B B (inl B o outl B) (inr B o outr B) = outr B
      +
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
outl B o op B B (inl B o outl B) (inr B o outr B) = outl B rewrite op_postcompose.
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
op B X (outl B o (inl B o outl B)) (outl B o (inr B o outr B)) = outl B
        rewrite <- !associativity.
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
op B X (outl B o inl B o outl B) (outl B o inr B o outr B) = outl B
        rewrite (beta_l (biproduct_is B)).
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
op B X (1 o outl B) (outl B o inr B o outr B) = outl B
        rewrite (mixed_l (biproduct_is B)).
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
op B X (1 o outl B) (zero_morphism X X o outr B) = outl B
        rewrite left_identity.
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
op B X (outl B) (zero_morphism X X o outr B) = outl B
        rewrite zero_morphism_left.
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
op B X (outl B) (zero_morphism B X) = outl B
        rewrite <- op_zero_unique.
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
op B X (outl B) (op_zero B X) = outl B
        apply op_zero_r.
      +
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
outr B o op B B (inl B o outl B) (inr B o outr B) = outr B rewrite op_postcompose.
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
op B X (outr B o (inl B o outl B)) (outr B o (inr B o outr B)) = outr B
        rewrite <- !associativity.
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
op B X (outr B o inl B o outl B) (outr B o inr B o outr B) = outr B
        rewrite (mixed_r (biproduct_is B)).
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
op B X (zero_morphism X X o outl B) (outr B o inr B o outr B) = outr B
        rewrite (beta_r (biproduct_is B)).
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
op B X (zero_morphism X X o outl B) (1 o outr B) = outr B
        rewrite left_identity.
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
op B X (zero_morphism X X o outl B) (outr B) = outr B
        rewrite zero_morphism_left.
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
op B X (zero_morphism B X) (outr B) = outr B
        rewrite <- op_zero_unique.
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
op B X (op_zero B X) (outr B) = outr B
        apply op_zero_l.
    -
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
biproduct_prod_mor B (outl B) (outr B) = 1 symmetry.
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
1 = biproduct_prod_mor B (outl B) (outr B)
      apply (biproduct_prod_unique B).
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
outl B o 1 = outl B
C: SemiAdditiveCategory
op: forall X0 Y : C, morphism C X0 Y -> morphism C X0 Y -> morphism C X0 Y
op_zero: forall X0 Y : C, morphism C X0 Y
op_zero_l: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y (op_zero X0 Y) f = f
op_zero_r: forall (X0 Y : C) (f : morphism C X0 Y), op X0 Y f (op_zero X0 Y) = f
op_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z) (f g : morphism C X0 Y),
h o op X0 Y f g = op X0 Z (h o f) (h o g)
op_precompose: forall (X0 Y Z : C) (f g : morphism C Y Z) (h : morphism C X0 Y),
op Y Z f g o h = op X0 Z (f o h) (g o h)
op_zero_postcompose: forall (X0 Y Z : C) (h : morphism C Y Z), h o op_zero X0 Y = op_zero X0 Z
X: C
B:= X ⊕ X: Biproduct semiadditive_zero X X
outr B o 1 = outr B
      all: apply right_identity.
  Qed.

  (** The canonical addition is the unique such operation. *)
  Theorem morphism_addition_unique {X Y : object C} (f g : morphism C X Y)
    : op X Y f g = f + g.
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
op X Y f g = f + g
  Proof.
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
op X Y f g = f + g
    symmetry.
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
f + g = op X Y f g
    unfold sg_op, sgop_morphism, biproduct_codiagonal.
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
biproduct_coprod_mor (Y ⊕ Y) Y 1 1 o biproduct_prod_mor (Y ⊕ Y) f g =
op X Y f g
    rewrite <- (left_identity C _ _
      (biproduct_prod_mor (Y ⊕ Y) f g)).
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
biproduct_coprod_mor (Y ⊕ Y) Y 1 1 o (1 o biproduct_prod_mor (Y ⊕ Y) f g) =
op X Y f g
    rewrite <- (op_decompose_id Y).
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
biproduct_coprod_mor (Y ⊕ Y) Y 1 1
o (op (Y ⊕ Y) (Y ⊕ Y) (inl (Y ⊕ Y) o outl (Y ⊕ Y))
     (inr (Y ⊕ Y) o outr (Y ⊕ Y))
   o biproduct_prod_mor (Y ⊕ Y) f g) =
op X Y f g
    rewrite <- associativity.
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
biproduct_coprod_mor (Y ⊕ Y) Y 1 1
o op (Y ⊕ Y) (Y ⊕ Y) (inl (Y ⊕ Y) o outl (Y ⊕ Y))
    (inr (Y ⊕ Y) o outr (Y ⊕ Y))
o biproduct_prod_mor (Y ⊕ Y) f g = op X Y f g
    rewrite op_postcompose.
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
op (Y ⊕ Y) Y
  (biproduct_coprod_mor (Y ⊕ Y) Y 1 1 o (inl (Y ⊕ Y) o outl (Y ⊕ Y)))
  (biproduct_coprod_mor (Y ⊕ Y) Y 1 1 o (inr (Y ⊕ Y) o outr (Y ⊕ Y)))
o biproduct_prod_mor (Y ⊕ Y) f g = op X Y f g
    rewrite op_precompose.
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
op X Y
  (biproduct_coprod_mor (Y ⊕ Y) Y 1 1 o (inl (Y ⊕ Y) o outl (Y ⊕ Y))
   o biproduct_prod_mor (Y ⊕ Y) f g)
  (biproduct_coprod_mor (Y ⊕ Y) Y 1 1 o (inr (Y ⊕ Y) o outr (Y ⊕ Y))
   o biproduct_prod_mor (Y ⊕ Y) f g) =
op X Y f g
    apply ap011.
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
biproduct_coprod_mor (Y ⊕ Y) Y 1 1 o (inl (Y ⊕ Y) o outl (Y ⊕ Y))
o biproduct_prod_mor (Y ⊕ Y) f g = f
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
biproduct_coprod_mor (Y ⊕ Y) Y 1 1 o (inr (Y ⊕ Y) o outr (Y ⊕ Y))
o biproduct_prod_mor (Y ⊕ Y) f g = g
    -
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
biproduct_coprod_mor (Y ⊕ Y) Y 1 1 o (inl (Y ⊕ Y) o outl (Y ⊕ Y))
o biproduct_prod_mor (Y ⊕ Y) f g = f rewrite !associativity.
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
biproduct_coprod_mor (Y ⊕ Y) Y 1 1
o (inl (Y ⊕ Y) o (outl (Y ⊕ Y) o biproduct_prod_mor (Y ⊕ Y) f g)) = f
      rewrite biproduct_prod_beta_l.
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
biproduct_coprod_mor (Y ⊕ Y) Y 1 1 o (inl (Y ⊕ Y) o f) = f
      rewrite <- associativity.
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
biproduct_coprod_mor (Y ⊕ Y) Y 1 1 o inl (Y ⊕ Y) o f = f
      rewrite biproduct_coprod_beta_l.
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
1 o f = f
      apply left_identity.
    -
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
biproduct_coprod_mor (Y ⊕ Y) Y 1 1 o (inr (Y ⊕ Y) o outr (Y ⊕ Y))
o biproduct_prod_mor (Y ⊕ Y) f g = g rewrite !associativity.
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
biproduct_coprod_mor (Y ⊕ Y) Y 1 1
o (inr (Y ⊕ Y) o (outr (Y ⊕ Y) o biproduct_prod_mor (Y ⊕ Y) f g)) = g
      rewrite biproduct_prod_beta_r.
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
biproduct_coprod_mor (Y ⊕ Y) Y 1 1 o (inr (Y ⊕ Y) o g) = g
      rewrite <- associativity.
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
biproduct_coprod_mor (Y ⊕ Y) Y 1 1 o inr (Y ⊕ Y) o g = g
      rewrite biproduct_coprod_beta_r.
C: SemiAdditiveCategory
op: forall X0 Y0 : C, morphism C X0 Y0 -> morphism C X0 Y0 -> morphism C X0 Y0
op_zero: forall X0 Y0 : C, morphism C X0 Y0
op_zero_l: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 (op_zero X0 Y0) f0 = f0
op_zero_r: forall (X0 Y0 : C) (f0 : morphism C X0 Y0), op X0 Y0 f0 (op_zero X0 Y0) = f0
op_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z) (f0 g0 : morphism C X0 Y0),
h o op X0 Y0 f0 g0 = op X0 Z (h o f0) (h o g0)
op_precompose: forall (X0 Y0 Z : C) (f0 g0 : morphism C Y0 Z) (h : morphism C X0 Y0),
op Y0 Z f0 g0 o h = op X0 Z (f0 o h) (g0 o h)
op_zero_postcompose: forall (X0 Y0 Z : C) (h : morphism C Y0 Z), h o op_zero X0 Y0 = op_zero X0 Z
X, Y: C
f, g: morphism C X Y
1 o g = g
      apply left_identity.
  Qed.

End EnrichmentUniqueness.