Require Import Basics Types Truncations.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat.
Require Import HSet.
Require Import AbelianGroup.
Require Import Modalities.ReflectiveSubuniverse.

Local Open Scope mc_add_scope.

(** * Biproducts of abelian groups *)

Definition ab_biprod@{u} (A B : AbGroup@{u}) : AbGroup@{u}.
A, B: AbGroup
AbGroup
Proof.
A, B: AbGroup
AbGroup
  rapply (Build_AbGroup (grp_prod A B)).
A, B: AbGroup
Commutative group_sgop
  intros [a b] [a' b'].
A, B: AbGroup
a: A
b: B
a': A
b': B
group_sgop (a, b) (a', b') =
group_sgop (a', b') (a, b)
  apply path_prod; simpl; apply commutativity.
Defined.

(** These inherit [IsEmbedding] instances from their [grp_prod] versions. *)
Definition ab_biprod_inl {A B : AbGroup} : A $-> ab_biprod A B := grp_prod_inl.
Definition ab_biprod_inr {A B : AbGroup} : B $-> ab_biprod A B := grp_prod_inr.

(** These inherit [IsSurjection] instances from their [grp_prod] versions. *)
Definition ab_biprod_pr1 {A B : AbGroup} : ab_biprod A B $-> A := grp_prod_pr1.
Definition ab_biprod_pr2 {A B : AbGroup} : ab_biprod A B $-> B := grp_prod_pr2.

(** Recursion principle *)
Proposition ab_biprod_rec {A B Y : AbGroup}
            (f : A $-> Y) (g : B $-> Y)
  : (ab_biprod A B) $-> Y.
A, B, Y: AbGroup
f: A $-> Y
g: B $-> Y
ab_biprod A B $-> Y
Proof.
A, B, Y: AbGroup
f: A $-> Y
g: B $-> Y
ab_biprod A B $-> Y
  snrapply Build_GroupHomomorphism.
A, B, Y: AbGroup
f: A $-> Y
g: B $-> Y
ab_biprod A B -> Y
A, B, Y: AbGroup
f: A $-> Y
g: B $-> Y
IsSemiGroupPreserving ?f
  -
A, B, Y: AbGroup
f: A $-> Y
g: B $-> Y
ab_biprod A B -> Y intros [a b]; exact (f a + g b).
  -
A, B, Y: AbGroup
f: A $-> Y
g: B $-> Y
IsSemiGroupPreserving
  (fun X : ab_biprod A B =>
   (fun (a : A) (b : B) => f a + g b) (fst X) (snd X)) intros [a b] [a' b']; simpl.
A, B, Y: AbGroup
f: A $-> Y
g: B $-> Y
a: A
b: B
a': A
b': B
f (a + a') + g (b + b') = f a + g b + (f a' + g b')
    rewrite (grp_homo_op f).
A, B, Y: AbGroup
f: A $-> Y
g: B $-> Y
a: A
b: B
a': A
b': B
f a + f a' + g (b + b') = f a + g b + (f a' + g b')
    rewrite (grp_homo_op g).
A, B, Y: AbGroup
f: A $-> Y
g: B $-> Y
a: A
b: B
a': A
b': B
f a + f a' + (g b + g b') = f a + g b + (f a' + g b')
    rewrite (associativity _ (g b) _).
A, B, Y: AbGroup
f: A $-> Y
g: B $-> Y
a: A
b: B
a': A
b': B
f a + f a' + g b + g b' = f a + g b + (f a' + g b')
    rewrite <- (associativity _ (f a') _).
A, B, Y: AbGroup
f: A $-> Y
g: B $-> Y
a: A
b: B
a': A
b': B
f a + (f a' + g b) + g b' = f a + g b + (f a' + g b')
    rewrite (commutativity (f a') _).
A, B, Y: AbGroup
f: A $-> Y
g: B $-> Y
a: A
b: B
a': A
b': B
f a + (g b + f a') + g b' = f a + g b + (f a' + g b')
    rewrite (associativity _ (g b) _).
A, B, Y: AbGroup
f: A $-> Y
g: B $-> Y
a: A
b: B
a': A
b': B
f a + g b + f a' + g b' = f a + g b + (f a' + g b')
    exact (associativity _ (f a') _)^.
Defined.

Corollary ab_biprod_rec_uncurried {A B Y : AbGroup}
  : (A $-> Y) * (B $-> Y)
    -> (ab_biprod A B) $-> Y.
A, B, Y: AbGroup
(A $-> Y) * (B $-> Y) -> ab_biprod A B $-> Y
Proof.
A, B, Y: AbGroup
(A $-> Y) * (B $-> Y) -> ab_biprod A B $-> Y
  intros [f g].
A, B, Y: AbGroup
f: A $-> Y
g: B $-> Y
ab_biprod A B $-> Y exact (ab_biprod_rec f g).
Defined.

Proposition ab_biprod_rec_eta {A B Y : AbGroup}
            (u : ab_biprod A B $-> Y)
  : ab_biprod_rec (u $o ab_biprod_inl) (u $o ab_biprod_inr) == u.
A, B, Y: AbGroup
u: ab_biprod A B $-> Y
ab_biprod_rec (u $o ab_biprod_inl)
  (u $o ab_biprod_inr) == u
Proof.
A, B, Y: AbGroup
u: ab_biprod A B $-> Y
ab_biprod_rec (u $o ab_biprod_inl)
  (u $o ab_biprod_inr) == u
  intros [a b]; simpl.
A, B, Y: AbGroup
u: ab_biprod A B $-> Y
a: A
b: B
u (a, group_unit) + u (group_unit, b) = u (a, b)
  refine ((grp_homo_op u _ _)^ @ ap u _).
A, B, Y: AbGroup
u: ab_biprod A B $-> Y
a: A
b: B
(a, group_unit) + (group_unit, b) = (a, b)
  apply path_prod.
A, B, Y: AbGroup
u: ab_biprod A B $-> Y
a: A
b: B
fst ((a, group_unit) + (group_unit, b)) = fst (a, b)
A, B, Y: AbGroup
u: ab_biprod A B $-> Y
a: A
b: B
snd ((a, group_unit) + (group_unit, b)) = snd (a, b)
  -
A, B, Y: AbGroup
u: ab_biprod A B $-> Y
a: A
b: B
fst ((a, group_unit) + (group_unit, b)) = fst (a, b) exact (right_identity a).
  -
A, B, Y: AbGroup
u: ab_biprod A B $-> Y
a: A
b: B
snd ((a, group_unit) + (group_unit, b)) = snd (a, b) exact (left_identity b).
Defined.

Proposition ab_biprod_rec_inl_beta {A B Y : AbGroup}
            (a : A $-> Y) (b : B $-> Y)
  : (ab_biprod_rec a b) $o ab_biprod_inl == a.
A, B, Y: AbGroup
a: A $-> Y
b: B $-> Y
ab_biprod_rec a b $o ab_biprod_inl == a
Proof.
A, B, Y: AbGroup
a: A $-> Y
b: B $-> Y
ab_biprod_rec a b $o ab_biprod_inl == a
  intro x; simpl.
A, B, Y: AbGroup
a: A $-> Y
b: B $-> Y
x: A
a x + b group_unit = a x
  rewrite (grp_homo_unit b).
A, B, Y: AbGroup
a: A $-> Y
b: B $-> Y
x: A
a x + mon_unit = a x
  exact (right_identity (a x)).
Defined.

Proposition ab_biprod_rec_inr_beta {A B Y : AbGroup}
            (a : A $-> Y) (b : B $-> Y)
  : (ab_biprod_rec a b) $o ab_biprod_inr == b.
A, B, Y: AbGroup
a: A $-> Y
b: B $-> Y
ab_biprod_rec a b $o ab_biprod_inr == b
Proof.
A, B, Y: AbGroup
a: A $-> Y
b: B $-> Y
ab_biprod_rec a b $o ab_biprod_inr == b
  intro y; simpl.
A, B, Y: AbGroup
a: A $-> Y
b: B $-> Y
y: B
a group_unit + b y = b y
  rewrite (grp_homo_unit a).
A, B, Y: AbGroup
a: A $-> Y
b: B $-> Y
y: B
mon_unit + b y = b y
  exact (left_identity (b y)).
Defined.

Theorem isequiv_ab_biprod_rec `{Funext} {A B Y : AbGroup}
  : IsEquiv (@ab_biprod_rec_uncurried A B Y).
H: Funext
A, B, Y: AbGroup
IsEquiv ab_biprod_rec_uncurried
Proof.
H: Funext
A, B, Y: AbGroup
IsEquiv ab_biprod_rec_uncurried
  srapply isequiv_adjointify.
H: Funext
A, B, Y: AbGroup
(ab_biprod A B $-> Y) -> (A $-> Y) * (B $-> Y)
H: Funext
A, B, Y: AbGroup
ab_biprod_rec_uncurried o ?g == idmap
H: Funext
A, B, Y: AbGroup
?g o ab_biprod_rec_uncurried == idmap
  -
H: Funext
A, B, Y: AbGroup
(ab_biprod A B $-> Y) -> (A $-> Y) * (B $-> Y) intro phi.
H: Funext
A, B, Y: AbGroup
phi: ab_biprod A B $-> Y
(A $-> Y) * (B $-> Y)
    exact (phi $o ab_biprod_inl, phi $o ab_biprod_inr).
  -
H: Funext
A, B, Y: AbGroup
ab_biprod_rec_uncurried
o (fun phi : ab_biprod A B $-> Y =>
   (phi $o ab_biprod_inl, phi $o ab_biprod_inr)) ==
idmap intro phi.
H: Funext
A, B, Y: AbGroup
phi: ab_biprod A B $-> Y
ab_biprod_rec_uncurried
  (phi $o ab_biprod_inl, phi $o ab_biprod_inr) = phi
    apply equiv_path_grouphomomorphism.
H: Funext
A, B, Y: AbGroup
phi: ab_biprod A B $-> Y
ab_biprod_rec_uncurried
  (phi $o ab_biprod_inl, phi $o ab_biprod_inr) == phi
    exact (ab_biprod_rec_eta phi).
  -
H: Funext
A, B, Y: AbGroup
(fun phi : ab_biprod A B $-> Y =>
 (phi $o ab_biprod_inl, phi $o ab_biprod_inr))
o ab_biprod_rec_uncurried == idmap intros [a b].
H: Funext
A, B, Y: AbGroup
a: A $-> Y
b: B $-> Y
(ab_biprod_rec_uncurried (a, b) $o ab_biprod_inl,
ab_biprod_rec_uncurried (a, b) $o ab_biprod_inr) =
(a, b)
    apply path_prod.
H: Funext
A, B, Y: AbGroup
a: A $-> Y
b: B $-> Y
fst
  (ab_biprod_rec_uncurried (a, b) $o ab_biprod_inl,
  ab_biprod_rec_uncurried (a, b) $o ab_biprod_inr) =
fst (a, b)
H: Funext
A, B, Y: AbGroup
a: A $-> Y
b: B $-> Y
snd
  (ab_biprod_rec_uncurried (a, b) $o ab_biprod_inl,
  ab_biprod_rec_uncurried (a, b) $o ab_biprod_inr) =
snd (a, b)
    +
H: Funext
A, B, Y: AbGroup
a: A $-> Y
b: B $-> Y
fst
  (ab_biprod_rec_uncurried (a, b) $o ab_biprod_inl,
  ab_biprod_rec_uncurried (a, b) $o ab_biprod_inr) =
fst (a, b) apply equiv_path_grouphomomorphism.
H: Funext
A, B, Y: AbGroup
a: A $-> Y
b: B $-> Y
fst
  (ab_biprod_rec_uncurried (a, b) $o ab_biprod_inl,
  ab_biprod_rec_uncurried (a, b) $o ab_biprod_inr) ==
fst (a, b)
      apply ab_biprod_rec_inl_beta.
    +
H: Funext
A, B, Y: AbGroup
a: A $-> Y
b: B $-> Y
snd
  (ab_biprod_rec_uncurried (a, b) $o ab_biprod_inl,
  ab_biprod_rec_uncurried (a, b) $o ab_biprod_inr) =
snd (a, b) apply equiv_path_grouphomomorphism.
H: Funext
A, B, Y: AbGroup
a: A $-> Y
b: B $-> Y
snd
  (ab_biprod_rec_uncurried (a, b) $o ab_biprod_inl,
  ab_biprod_rec_uncurried (a, b) $o ab_biprod_inr) ==
snd (a, b)
      apply ab_biprod_rec_inr_beta.
Defined.

(** Corecursion principle, inherited from Groups/Group.v. *)
Definition ab_biprod_corec {A B X : AbGroup} (f : X $-> A) (g : X $-> B)
  : X $-> ab_biprod A B
  := grp_prod_corec f g.

Definition ab_corec_eta {X Y A B : AbGroup} (f : X $-> Y) (g0 : Y $-> A) (g1 : Y $-> B)
  : ab_biprod_corec g0 g1 $o f $== ab_biprod_corec (g0 $o f) (g1 $o f)
  := fun _ => idpath.

(** *** Functoriality of [ab_biprod] *)

Definition functor_ab_biprod {A A' B B' : AbGroup} (f : A $-> A') (g: B $-> B')
  : ab_biprod A B $-> ab_biprod A' B'
  := (ab_biprod_corec (f $o ab_biprod_pr1) (g $o ab_biprod_pr2)).

Definition ab_biprod_functor_beta {Z X Y A B : AbGroup} (f0 : Z $-> X) (f1 : Z $-> Y)
           (g0 : X $-> A) (g1 : Y $-> B)
  : functor_ab_biprod g0 g1 $o ab_biprod_corec f0 f1
                      $== ab_biprod_corec (g0 $o f0) (g1 $o f1)
  := fun _ => idpath.

Definition isequiv_functor_ab_biprod {A A' B B' : AbGroup}
           (f : A $-> A') (g : B $-> B') `{IsEquiv _ _ f} `{IsEquiv _ _ g}
  : IsEquiv (functor_ab_biprod f g).
A, A', B, B': AbGroup
f: A $-> A'
g: B $-> B'
H: IsEquiv f
H0: IsEquiv g
IsEquiv (functor_ab_biprod f g)
Proof.
A, A', B, B': AbGroup
f: A $-> A'
g: B $-> B'
H: IsEquiv f
H0: IsEquiv g
IsEquiv (functor_ab_biprod f g)
  srapply isequiv_adjointify.
A, A', B, B': AbGroup
f: A $-> A'
g: B $-> B'
H: IsEquiv f
H0: IsEquiv g
ab_biprod A' B' -> ab_biprod A B
A, A', B, B': AbGroup
f: A $-> A'
g: B $-> B'
H: IsEquiv f
H0: IsEquiv g
functor_ab_biprod f g o ?g == idmap
A, A', B, B': AbGroup
f: A $-> A'
g: B $-> B'
H: IsEquiv f
H0: IsEquiv g
?g o functor_ab_biprod f g == idmap
  1: {
A, A', B, B': AbGroup
f: A $-> A'
g: B $-> B'
H: IsEquiv f
H0: IsEquiv g
ab_biprod A' B' -> ab_biprod A B rapply functor_ab_biprod;
       apply grp_iso_inverse.
A, A', B, B': AbGroup
f: A $-> A'
g: B $-> B'
H: IsEquiv f
H0: IsEquiv g
GroupIsomorphism A A'
A, A', B, B': AbGroup
f: A $-> A'
g: B $-> B'
H: IsEquiv f
H0: IsEquiv g
GroupIsomorphism B B'
       +
A, A', B, B': AbGroup
f: A $-> A'
g: B $-> B'
H: IsEquiv f
H0: IsEquiv g
GroupIsomorphism A A' exact (Build_GroupIsomorphism _ _ f _).
       +
A, A', B, B': AbGroup
f: A $-> A'
g: B $-> B'
H: IsEquiv f
H0: IsEquiv g
GroupIsomorphism B B' exact (Build_GroupIsomorphism _ _ g _). }
A, A', B, B': AbGroup
f: A $-> A'
g: B $-> B'
H: IsEquiv f
H0: IsEquiv g
functor_ab_biprod f g
o functor_ab_biprod
    (let X :=
       fun H : GroupIsomorphism A A' =>
       grp_iso_homo A' A (grp_iso_inverse H) in
     X {| grp_iso_homo := f; isequiv_group_iso := H |})
    (let X :=
       fun H : GroupIsomorphism B B' =>
       grp_iso_homo B' B (grp_iso_inverse H) in
     X
       {|
         grp_iso_homo := g; isequiv_group_iso := H0
       |}) == idmap
A, A', B, B': AbGroup
f: A $-> A'
g: B $-> B'
H: IsEquiv f
H0: IsEquiv g
functor_ab_biprod
  (let X :=
     fun H : GroupIsomorphism A A' =>
     grp_iso_homo A' A (grp_iso_inverse H) in
   X {| grp_iso_homo := f; isequiv_group_iso := H |})
  (let X :=
     fun H : GroupIsomorphism B B' =>
     grp_iso_homo B' B (grp_iso_inverse H) in
   X {| grp_iso_homo := g; isequiv_group_iso := H0 |})
o functor_ab_biprod f g == idmap
  all: intros [a b]; simpl.
A, A', B, B': AbGroup
f: A $-> A'
g: B $-> B'
H: IsEquiv f
H0: IsEquiv g
a: A'
b: B'
(f (f^-1 a), g (g^-1 b)) = (a, b)
A, A', B, B': AbGroup
f: A $-> A'
g: B $-> B'
H: IsEquiv f
H0: IsEquiv g
a: A
b: B
(f^-1 (f a), g^-1 (g b)) = (a, b)
  all: apply path_prod'.
A, A', B, B': AbGroup
f: A $-> A'
g: B $-> B'
H: IsEquiv f
H0: IsEquiv g
a: A'
b: B'
f (f^-1 a) = a
A, A', B, B': AbGroup
f: A $-> A'
g: B $-> B'
H: IsEquiv f
H0: IsEquiv g
a: A'
b: B'
g (g^-1 b) = b
A, A', B, B': AbGroup
f: A $-> A'
g: B $-> B'
H: IsEquiv f
H0: IsEquiv g
a: A
b: B
f^-1 (f a) = a
A, A', B, B': AbGroup
f: A $-> A'
g: B $-> B'
H: IsEquiv f
H0: IsEquiv g
a: A
b: B
g^-1 (g b) = b
  1,2: apply eisretr.
A, A', B, B': AbGroup
f: A $-> A'
g: B $-> B'
H: IsEquiv f
H0: IsEquiv g
a: A
b: B
f^-1 (f a) = a
A, A', B, B': AbGroup
f: A $-> A'
g: B $-> B'
H: IsEquiv f
H0: IsEquiv g
a: A
b: B
g^-1 (g b) = b
  all: apply eissect.
Defined.

Definition equiv_functor_ab_biprod {A A' B B' : AbGroup}
           (f : A $-> A') (g : B $-> B') `{IsEquiv _ _ f} `{IsEquiv _ _ g}
  : GroupIsomorphism (ab_biprod A B) (ab_biprod A' B')
  := Build_GroupIsomorphism _ _ _ (isequiv_functor_ab_biprod f g).

(** Biproducts preserve embeddings. *)
Definition functor_ab_biprod_embedding {A A' B B' : AbGroup}
           (i : A $-> B) (i' : A' $-> B')
           `{IsEmbedding i} `{IsEmbedding i'}
  : IsEmbedding (functor_ab_biprod i i').
A, A', B, B': AbGroup
i: A $-> B
i': A' $-> B'
IsEmbedding0: IsEmbedding i
IsEmbedding1: IsEmbedding i'
IsEmbedding (functor_ab_biprod i i')
Proof.
A, A', B, B': AbGroup
i: A $-> B
i': A' $-> B'
IsEmbedding0: IsEmbedding i
IsEmbedding1: IsEmbedding i'
IsEmbedding (functor_ab_biprod i i')
  intros [b b'].
A, A', B, B': AbGroup
i: A $-> B
i': A' $-> B'
IsEmbedding0: IsEmbedding i
IsEmbedding1: IsEmbedding i'
b: B
b': B'
IsHProp (hfiber (functor_ab_biprod i i') (b, b'))
  apply hprop_allpath.
A, A', B, B': AbGroup
i: A $-> B
i': A' $-> B'
IsEmbedding0: IsEmbedding i
IsEmbedding1: IsEmbedding i'
b: B
b': B'
forall x y : hfiber (functor_ab_biprod i i') (b, b'),
x = y
  intros [[a0 a0'] p] [[a1 a1'] p']; cbn in p, p'.
A, A', B, B': AbGroup
i: A $-> B
i': A' $-> B'
IsEmbedding0: IsEmbedding i
IsEmbedding1: IsEmbedding i'
b: B
b': B'
a0: A
a0': A'
p: (i a0, i' a0') = (b, b')
a1: A
a1': A'
p': (i a1, i' a1') = (b, b')
((a0, a0'); p) = ((a1, a1'); p')
  rapply path_sigma_hprop; cbn.
A, A', B, B': AbGroup
i: A $-> B
i': A' $-> B'
IsEmbedding0: IsEmbedding i
IsEmbedding1: IsEmbedding i'
b: B
b': B'
a0: A
a0': A'
p: (i a0, i' a0') = (b, b')
a1: A
a1': A'
p': (i a1, i' a1') = (b, b')
(a0, a0') = (a1, a1')
  pose (q := (equiv_path_prod _ _)^-1 p); cbn in q.
A, A', B, B': AbGroup
i: A $-> B
i': A' $-> B'
IsEmbedding0: IsEmbedding i
IsEmbedding1: IsEmbedding i'
b: B
b': B'
a0: A
a0': A'
p: (i a0, i' a0') = (b, b')
a1: A
a1': A'
p': (i a1, i' a1') = (b, b')
q:= (ap fst p, ap snd p): (i a0 = b) * (i' a0' = b')
(a0, a0') = (a1, a1')
  pose (q' := (equiv_path_prod _ _)^-1 p'); cbn in q'.
A, A', B, B': AbGroup
i: A $-> B
i': A' $-> B'
IsEmbedding0: IsEmbedding i
IsEmbedding1: IsEmbedding i'
b: B
b': B'
a0: A
a0': A'
p: (i a0, i' a0') = (b, b')
a1: A
a1': A'
p': (i a1, i' a1') = (b, b')
q:= (ap fst p, ap snd p): (i a0 = b) * (i' a0' = b')
q':= (ap fst p', ap snd p'): (i a1 = b) * (i' a1' = b')
(a0, a0') = (a1, a1')
  destruct q as [q0 q1], q' as [q0' q1'].
A, A', B, B': AbGroup
i: A $-> B
i': A' $-> B'
IsEmbedding0: IsEmbedding i
IsEmbedding1: IsEmbedding i'
b: B
b': B'
a0: A
a0': A'
p: (i a0, i' a0') = (b, b')
a1: A
a1': A'
p': (i a1, i' a1') = (b, b')
q0: i a0 = b
q1: i' a0' = b'
q0': i a1 = b
q1': i' a1' = b'
(a0, a0') = (a1, a1')
  apply path_prod; rapply isinj_embedding; cbn.
A, A', B, B': AbGroup
i: A $-> B
i': A' $-> B'
IsEmbedding0: IsEmbedding i
IsEmbedding1: IsEmbedding i'
b: B
b': B'
a0: A
a0': A'
p: (i a0, i' a0') = (b, b')
a1: A
a1': A'
p': (i a1, i' a1') = (b, b')
q0: i a0 = b
q1: i' a0' = b'
q0': i a1 = b
q1': i' a1' = b'
i a0 = i a1
A, A', B, B': AbGroup
i: A $-> B
i': A' $-> B'
IsEmbedding0: IsEmbedding i
IsEmbedding1: IsEmbedding i'
b: B
b': B'
a0: A
a0': A'
p: (i a0, i' a0') = (b, b')
a1: A
a1': A'
p': (i a1, i' a1') = (b, b')
q0: i a0 = b
q1: i' a0' = b'
q0': i a1 = b
q1': i' a1' = b'
i' a0' = i' a1'
  -
A, A', B, B': AbGroup
i: A $-> B
i': A' $-> B'
IsEmbedding0: IsEmbedding i
IsEmbedding1: IsEmbedding i'
b: B
b': B'
a0: A
a0': A'
p: (i a0, i' a0') = (b, b')
a1: A
a1': A'
p': (i a1, i' a1') = (b, b')
q0: i a0 = b
q1: i' a0' = b'
q0': i a1 = b
q1': i' a1' = b'
i a0 = i a1 exact (q0 @ q0'^).
  -
A, A', B, B': AbGroup
i: A $-> B
i': A' $-> B'
IsEmbedding0: IsEmbedding i
IsEmbedding1: IsEmbedding i'
b: B
b': B'
a0: A
a0': A'
p: (i a0, i' a0') = (b, b')
a1: A
a1': A'
p': (i a1, i' a1') = (b, b')
q0: i a0 = b
q1: i' a0' = b'
q0': i a1 = b
q1': i' a1' = b'
i' a0' = i' a1' exact (q1 @ q1'^).
Defined.

(** Products preserve surjections. *)
Definition functor_ab_biprod_surjection `{Funext} {A A' B B' : AbGroup}
           (p : A $-> B) (p' : A' $-> B')
           `{S : IsSurjection p} `{S' : IsSurjection p'}
  : IsSurjection (functor_ab_biprod p p').
H: Funext
A, A', B, B': AbGroup
p: A $-> B
p': A' $-> B'
S: IsConnMap (Tr (-1)) p
S': IsConnMap (Tr (-1)) p'
IsConnMap (Tr (-1)) (functor_ab_biprod p p')
Proof.
H: Funext
A, A', B, B': AbGroup
p: A $-> B
p': A' $-> B'
S: IsConnMap (Tr (-1)) p
S': IsConnMap (Tr (-1)) p'
IsConnMap (Tr (-1)) (functor_ab_biprod p p')
  intros [b b'].
H: Funext
A, A', B, B': AbGroup
p: A $-> B
p': A' $-> B'
S: IsConnMap (Tr (-1)) p
S': IsConnMap (Tr (-1)) p'
b: B
b': B'
IsConnected (Tr (-1))
  (hfiber (functor_ab_biprod p p') (b, b'))
  pose proof (a := S b); pose proof (a' := S' b').
H: Funext
A, A', B, B': AbGroup
p: A $-> B
p': A' $-> B'
S: IsConnMap (Tr (-1)) p
S': IsConnMap (Tr (-1)) p'
b: B
b': B'
a: IsConnected (Tr (-1)) (hfiber p b)
a': IsConnected (Tr (-1)) (hfiber p' b')
IsConnected (Tr (-1))
  (hfiber (functor_ab_biprod p p') (b, b'))
  apply center in a, a'.
H: Funext
A, A', B, B': AbGroup
p: A $-> B
p': A' $-> B'
S: IsConnMap (Tr (-1)) p
S': IsConnMap (Tr (-1)) p'
b: B
b': B'
a: Tr (-1) (hfiber p b)
a': Tr (-1) (hfiber p' b')
IsConnected (Tr (-1))
  (hfiber (functor_ab_biprod p p') (b, b'))
  strip_truncations.
H: Funext
A, A', B, B': AbGroup
p: A $-> B
p': A' $-> B'
S: IsConnMap (Tr (-1)) p
S': IsConnMap (Tr (-1)) p'
b: B
b': B'
a': hfiber p' b'
a: hfiber p b
IsConnected (Tr (-1))
  (hfiber (functor_ab_biprod p p') (b, b'))
  rapply contr_inhabited_hprop.
H: Funext
A, A', B, B': AbGroup
p: A $-> B
p': A' $-> B'
S: IsConnMap (Tr (-1)) p
S': IsConnMap (Tr (-1)) p'
b: B
b': B'
a': hfiber p' b'
a: hfiber p b
Tr (-1) (hfiber (functor_ab_biprod p p') (b, b'))
  apply tr.
H: Funext
A, A', B, B': AbGroup
p: A $-> B
p': A' $-> B'
S: IsConnMap (Tr (-1)) p
S': IsConnMap (Tr (-1)) p'
b: B
b': B'
a': hfiber p' b'
a: hfiber p b
hfiber (functor_ab_biprod p p') (b, b')
  exists (ab_biprod_inl a.1 + ab_biprod_inr a'.1); cbn.
H: Funext
A, A', B, B': AbGroup
p: A $-> B
p': A' $-> B'
S: IsConnMap (Tr (-1)) p
S': IsConnMap (Tr (-1)) p'
b: B
b': B'
a': hfiber p' b'
a: hfiber p b
(p (a.1 + group_unit), p' (group_unit + a'.1)) =
(b, b')
  apply path_prod;
    refine (grp_homo_op _ _ _ @ _);
    rewrite (grp_homo_unit _);
    cbn.
H: Funext
A, A', B, B': AbGroup
p: A $-> B
p': A' $-> B'
S: IsConnMap (Tr (-1)) p
S': IsConnMap (Tr (-1)) p'
b: B
b': B'
a': hfiber p' b'
a: hfiber p b
p a.1 + mon_unit = b
H: Funext
A, A', B, B': AbGroup
p: A $-> B
p': A' $-> B'
S: IsConnMap (Tr (-1)) p
S': IsConnMap (Tr (-1)) p'
b: B
b': B'
a': hfiber p' b'
a: hfiber p b
mon_unit + p' a'.1 = b'
  -
H: Funext
A, A', B, B': AbGroup
p: A $-> B
p': A' $-> B'
S: IsConnMap (Tr (-1)) p
S': IsConnMap (Tr (-1)) p'
b: B
b': B'
a': hfiber p' b'
a: hfiber p b
p a.1 + mon_unit = b exact (right_identity _ @ a.2).
  -
H: Funext
A, A', B, B': AbGroup
p: A $-> B
p': A' $-> B'
S: IsConnMap (Tr (-1)) p
S': IsConnMap (Tr (-1)) p'
b: B
b': B'
a': hfiber p' b'
a: hfiber p b
mon_unit + p' a'.1 = b' exact (left_identity _ @ a'.2).
Defined.

(** *** Lemmas for working with biproducts *)

Lemma ab_biprod_decompose {B A : AbGroup} (a : A) (b : B)
  : (a, b) = ((a, group_unit) : ab_biprod A B) + (group_unit, b).
B, A: AbGroup
a: A
b: B
(a, b) =
((a, group_unit) : ab_biprod A B) + (group_unit, b)
Proof.
B, A: AbGroup
a: A
b: B
(a, b) =
((a, group_unit) : ab_biprod A B) + (group_unit, b)
  apply path_prod; cbn.
B, A: AbGroup
a: A
b: B
a = a + group_unit
B, A: AbGroup
a: A
b: B
b = group_unit + b
  -
B, A: AbGroup
a: A
b: B
a = a + group_unit exact (right_identity _)^.
  -
B, A: AbGroup
a: A
b: B
b = group_unit + b exact (left_identity _)^.
Defined.

Lemma ab_biprod_corec_eta' {A B X : AbGroup} (f g : ab_biprod A B $-> X)
  : (f $o ab_biprod_inl $== g $o ab_biprod_inl)
  -> (f $o ab_biprod_inr $== g $o ab_biprod_inr)
  -> f $== g.
A, B, X: AbGroup
f, g: ab_biprod A B $-> X
f $o ab_biprod_inl $== g $o ab_biprod_inl ->
f $o ab_biprod_inr $== g $o ab_biprod_inr -> f $== g
Proof.
A, B, X: AbGroup
f, g: ab_biprod A B $-> X
f $o ab_biprod_inl $== g $o ab_biprod_inl ->
f $o ab_biprod_inr $== g $o ab_biprod_inr -> f $== g
  intros h k.
A, B, X: AbGroup
f, g: ab_biprod A B $-> X
h: f $o ab_biprod_inl $== g $o ab_biprod_inl
k: f $o ab_biprod_inr $== g $o ab_biprod_inr
f $== g
  intros [a b].
A, B, X: AbGroup
f, g: ab_biprod A B $-> X
h: f $o ab_biprod_inl $== g $o ab_biprod_inl
k: f $o ab_biprod_inr $== g $o ab_biprod_inr
a: A
b: B
f (a, b) = g (a, b)
  refine (ap f (ab_biprod_decompose _ _) @ _ @ ap g (ab_biprod_decompose _ _)^).
A, B, X: AbGroup
f, g: ab_biprod A B $-> X
h: f $o ab_biprod_inl $== g $o ab_biprod_inl
k: f $o ab_biprod_inr $== g $o ab_biprod_inr
a: A
b: B
f ((a, group_unit) + (group_unit, b)) =
g ((a, group_unit) + (group_unit, b))
  refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^).
A, B, X: AbGroup
f, g: ab_biprod A B $-> X
h: f $o ab_biprod_inl $== g $o ab_biprod_inl
k: f $o ab_biprod_inr $== g $o ab_biprod_inr
a: A
b: B
f (a, group_unit) + f (group_unit, b) =
g (a, group_unit) + g (group_unit, b)
  exact (ap011 (+) (h a) (k b)).
Defined.

(* Maps out of biproducts are determined on the two inclusions. *)
Lemma equiv_path_biprod_corec `{Funext} {A B X : AbGroup} (phi psi : ab_biprod A B $-> X)
  : ((phi $o ab_biprod_inl == psi $o ab_biprod_inl) * (phi $o ab_biprod_inr == psi $o ab_biprod_inr))
      <~> phi == psi.
H: Funext
A, B, X: AbGroup
phi, psi: ab_biprod A B $-> X
(phi $o ab_biprod_inl == psi $o ab_biprod_inl) *
(phi $o ab_biprod_inr == psi $o ab_biprod_inr) <~>
phi == psi
Proof.
H: Funext
A, B, X: AbGroup
phi, psi: ab_biprod A B $-> X
(phi $o ab_biprod_inl == psi $o ab_biprod_inl) *
(phi $o ab_biprod_inr == psi $o ab_biprod_inr) <~>
phi == psi
  apply equiv_iff_hprop.
H: Funext
A, B, X: AbGroup
phi, psi: ab_biprod A B $-> X
(phi $o ab_biprod_inl == psi $o ab_biprod_inl) *
(phi $o ab_biprod_inr == psi $o ab_biprod_inr) ->
phi == psi
H: Funext
A, B, X: AbGroup
phi, psi: ab_biprod A B $-> X
phi == psi ->
(phi $o ab_biprod_inl == psi $o ab_biprod_inl) *
(phi $o ab_biprod_inr == psi $o ab_biprod_inr)
  -
H: Funext
A, B, X: AbGroup
phi, psi: ab_biprod A B $-> X
(phi $o ab_biprod_inl == psi $o ab_biprod_inl) *
(phi $o ab_biprod_inr == psi $o ab_biprod_inr) ->
phi == psi intros [h k].
H: Funext
A, B, X: AbGroup
phi, psi: ab_biprod A B $-> X
h: phi $o ab_biprod_inl == psi $o ab_biprod_inl
k: phi $o ab_biprod_inr == psi $o ab_biprod_inr
phi == psi
    apply ab_biprod_corec_eta'; assumption.
  -
H: Funext
A, B, X: AbGroup
phi, psi: ab_biprod A B $-> X
phi == psi ->
(phi $o ab_biprod_inl == psi $o ab_biprod_inl) *
(phi $o ab_biprod_inr == psi $o ab_biprod_inr) intro h.
H: Funext
A, B, X: AbGroup
phi, psi: ab_biprod A B $-> X
h: phi == psi
(phi $o ab_biprod_inl == psi $o ab_biprod_inl) *
(phi $o ab_biprod_inr == psi $o ab_biprod_inr)
    exact (fun a => h _, fun b => h _).
Defined.

(** The swap isomorphism of the biproduct of two groups. *)
Definition direct_sum_swap {A B : AbGroup}
  : ab_biprod A B $<~> ab_biprod B A.
A, B: AbGroup
ab_biprod A B $<~> ab_biprod B A
Proof.
A, B: AbGroup
ab_biprod A B $<~> ab_biprod B A
  snrapply Build_GroupIsomorphism'.
A, B: AbGroup
ab_biprod A B <~> ab_biprod B A
A, B: AbGroup
IsSemiGroupPreserving ?f
  -
A, B: AbGroup
ab_biprod A B <~> ab_biprod B A apply equiv_prod_symm.
  -
A, B: AbGroup
IsSemiGroupPreserving (equiv_prod_symm A B) intro; reflexivity.
Defined.

(** Addition [+] is a group homomorphism [A+A -> A]. *)
Definition ab_codiagonal {A : AbGroup} : ab_biprod A A $-> A
  := ab_biprod_rec grp_homo_id grp_homo_id.

Definition ab_codiagonal_natural {A B : AbGroup} (f : A $-> B)
  : f $o ab_codiagonal $== ab_codiagonal $o functor_ab_biprod f f
  := fun a => grp_homo_op f _ _.

Definition ab_diagonal {A : AbGroup} : A $-> ab_biprod A A
  := ab_biprod_corec grp_homo_id grp_homo_id.

(** Given two abelian group homomorphisms [f] and [g], their pairing [(f, g) : B -> A + A] can be written as a composite. Note that [ab_biprod_corec] is an alias for [grp_prod_corec]. *)
Lemma ab_biprod_corec_diagonal `{Funext} {A B : AbGroup} (f g : B $-> A)
  : ab_biprod_corec f g = (functor_ab_biprod f g) $o ab_diagonal.
H: Funext
A, B: AbGroup
f, g: B $-> A
ab_biprod_corec f g =
functor_ab_biprod f g $o ab_diagonal
Proof.
H: Funext
A, B: AbGroup
f, g: B $-> A
ab_biprod_corec f g =
functor_ab_biprod f g $o ab_diagonal
  apply equiv_path_grouphomomorphism; reflexivity.
Defined.

(** Precomposing the codiagonal with the swap map has no effect. *)
Lemma ab_codiagonal_swap `{Funext} {A : AbGroup}
  : (@ab_codiagonal A) $o direct_sum_swap = ab_codiagonal.
H: Funext
A: AbGroup
ab_codiagonal $o direct_sum_swap = ab_codiagonal
Proof.
H: Funext
A: AbGroup
ab_codiagonal $o direct_sum_swap = ab_codiagonal
  apply equiv_path_grouphomomorphism.
H: Funext
A: AbGroup
ab_codiagonal $o direct_sum_swap == ab_codiagonal
  intro a; cbn.
H: Funext
A: AbGroup
a: ab_biprod A A
snd a + fst a = fst a + snd a
  exact (abgroup_commutative _ _ _).
Defined.

(** The corresponding result for the diagonal is true definitionally, so it isn't strictly necessary to state it, but we record it anyways. *)
Definition ab_diagonal_swap {A : AbGroup}
  : direct_sum_swap $o (@ab_diagonal A) = ab_diagonal
  := idpath.

(** The biproduct is associative. *)
Lemma ab_biprod_assoc {A B C : AbGroup}
  : ab_biprod A (ab_biprod B C) $<~> ab_biprod (ab_biprod A B) C.
A, B, C: AbGroup
ab_biprod A (ab_biprod B C) $<~>
ab_biprod (ab_biprod A B) C
Proof.
A, B, C: AbGroup
ab_biprod A (ab_biprod B C) $<~>
ab_biprod (ab_biprod A B) C
  snrapply Build_GroupIsomorphism'.
A, B, C: AbGroup
ab_biprod A (ab_biprod B C) <~>
ab_biprod (ab_biprod A B) C
A, B, C: AbGroup
IsSemiGroupPreserving ?f
  -
A, B, C: AbGroup
ab_biprod A (ab_biprod B C) <~>
ab_biprod (ab_biprod A B) C apply equiv_prod_assoc.
  -
A, B, C: AbGroup
IsSemiGroupPreserving (equiv_prod_assoc A B C) unfold IsSemiGroupPreserving; reflexivity.
Defined.

(** The iterated diagonals [(ab_diagonal + id) o ab_diagonal] and [(id + ab_diagonal) o ab_diagonal] agree, after reassociating the direct sum. *)
Definition ab_commute_id_diagonal {A : AbGroup}
  : (functor_ab_biprod (@ab_diagonal A) grp_homo_id) $o ab_diagonal
    = ab_biprod_assoc $o (functor_ab_biprod grp_homo_id ab_diagonal) $o ab_diagonal
  := idpath.

(** A similar result for the codiagonal. *)
Lemma ab_commute_id_codiagonal `{Funext} {A : AbGroup}
  : (@ab_codiagonal A) $o (functor_ab_biprod ab_codiagonal grp_homo_id) $o ab_biprod_assoc
    = ab_codiagonal $o (functor_ab_biprod grp_homo_id ab_codiagonal).
H: Funext
A: AbGroup
ab_codiagonal $o
functor_ab_biprod ab_codiagonal grp_homo_id $o
ab_biprod_assoc =
ab_codiagonal $o
functor_ab_biprod grp_homo_id ab_codiagonal
Proof.
H: Funext
A: AbGroup
ab_codiagonal $o
functor_ab_biprod ab_codiagonal grp_homo_id $o
ab_biprod_assoc =
ab_codiagonal $o
functor_ab_biprod grp_homo_id ab_codiagonal
  apply equiv_path_grouphomomorphism.
H: Funext
A: AbGroup
ab_codiagonal $o
functor_ab_biprod ab_codiagonal grp_homo_id $o
ab_biprod_assoc ==
ab_codiagonal $o
functor_ab_biprod grp_homo_id ab_codiagonal
  intro a; cbn.
H: Funext
A: AbGroup
a: ab_biprod A (ab_biprod A A)
fst a + fst (snd a) + snd (snd a) =
fst a + (fst (snd a) + snd (snd a))
  exact (grp_assoc _ _ _)^.
Defined.

(** The next few results are used to prove associativity of the Baer sum. *)

(** A "twist" isomorphism [(A + B) + C <~> (C + B) + A]. *)
Lemma ab_biprod_twist {A B C : AbGroup@{u}}
  : ab_biprod (ab_biprod A B) C $<~> ab_biprod (ab_biprod C B) A.
A, B, C: AbGroup
ab_biprod (ab_biprod A B) C $<~>
ab_biprod (ab_biprod C B) A
Proof.
A, B, C: AbGroup
ab_biprod (ab_biprod A B) C $<~>
ab_biprod (ab_biprod C B) A
  snrapply Build_GroupIsomorphism.
A, B, C: AbGroup
GroupHomomorphism (ab_biprod (ab_biprod A B) C)
  (ab_biprod (ab_biprod C B) A)
A, B, C: AbGroup
IsEquiv ?grp_iso_homo
  -
A, B, C: AbGroup
GroupHomomorphism (ab_biprod (ab_biprod A B) C)
  (ab_biprod (ab_biprod C B) A) snrapply Build_GroupHomomorphism.
A, B, C: AbGroup
ab_biprod (ab_biprod A B) C ->
ab_biprod (ab_biprod C B) A
A, B, C: AbGroup
IsSemiGroupPreserving ?f
    +
A, B, C: AbGroup
ab_biprod (ab_biprod A B) C ->
ab_biprod (ab_biprod C B) A intros [[a b] c].
A, B, C: AbGroup
a: A
b: B
c: C
ab_biprod (ab_biprod C B) A
      exact ((c,b),a).
    +
A, B, C: AbGroup
IsSemiGroupPreserving
  (fun X : ab_biprod (ab_biprod A B) C =>
   (fun fst : ab_biprod A B =>
    (fun (a : A) (b : B) (c : C) => (c, b, a))
      (Overture.fst fst) (snd fst)) (fst X) (snd X)) unfold IsSemiGroupPreserving.
A, B, C: AbGroup
forall x y : ab_biprod (ab_biprod A B) C,
(snd (x + y), snd (fst (x + y)), fst (fst (x + y))) =
(snd x, snd (fst x), fst (fst x)) +
(snd y, snd (fst y), fst (fst y)) reflexivity.
  -
A, B, C: AbGroup
IsEquiv
  (Build_GroupHomomorphism
     (fun X : ab_biprod (ab_biprod A B) C =>
      (fun fst : ab_biprod A B =>
       (fun (a : A) (b : B) (c : C) => (c, b, a))
         (Overture.fst fst) (snd fst)) (fst X) (snd X))) snrapply isequiv_adjointify.
A, B, C: AbGroup
ab_biprod (ab_biprod C B) A ->
ab_biprod (ab_biprod A B) C
A, B, C: AbGroup
Build_GroupHomomorphism
  (fun X : ab_biprod (ab_biprod A B) C =>
   (fun fst : ab_biprod A B =>
    (fun (a : A) (b : B) (c : C) => (c, b, a))
      (Overture.fst fst) (snd fst)) (fst X) (snd X))
o ?g == idmap
A, B, C: AbGroup
?g
o Build_GroupHomomorphism
    (fun X : ab_biprod (ab_biprod A B) C =>
     (fun fst : ab_biprod A B =>
      (fun (a : A) (b : B) (c : C) => (c, b, a))
        (Overture.fst fst) (snd fst)) (fst X) (snd X)) ==
idmap
    +
A, B, C: AbGroup
ab_biprod (ab_biprod C B) A ->
ab_biprod (ab_biprod A B) C intros [[c b] a].
A, B, C: AbGroup
c: C
b: B
a: A
ab_biprod (ab_biprod A B) C
      exact ((a,b),c).
    +
A, B, C: AbGroup
Build_GroupHomomorphism
  (fun X : ab_biprod (ab_biprod A B) C =>
   (fun fst : ab_biprod A B =>
    (fun (a : A) (b : B) (c : C) => (c, b, a))
      (Overture.fst fst) (snd fst)) (fst X) (snd X))
o (fun X : ab_biprod (ab_biprod C B) A =>
   (fun fst : ab_biprod C B =>
    (fun (c : C) (b : B) (a : A) => (a, b, c))
      (Overture.fst fst) (snd fst)) (fst X) (snd X)) ==
idmap reflexivity.
    +
A, B, C: AbGroup
(fun X : ab_biprod (ab_biprod C B) A =>
 (fun fst : ab_biprod C B =>
  (fun (c : C) (b : B) (a : A) => (a, b, c))
    (Overture.fst fst) (snd fst)) (fst X) (snd X))
o Build_GroupHomomorphism
    (fun X : ab_biprod (ab_biprod A B) C =>
     (fun fst : ab_biprod A B =>
      (fun (a : A) (b : B) (c : C) => (c, b, a))
        (Overture.fst fst) (snd fst)) (fst X) (snd X)) ==
idmap reflexivity.
Defined.

(** The triagonal and cotriagonal homomorphisms. *)
Definition ab_triagonal {A : AbGroup} : A $-> ab_biprod (ab_biprod A A) A
  := (functor_ab_biprod ab_diagonal grp_homo_id) $o ab_diagonal.

Definition ab_cotriagonal {A : AbGroup} : ab_biprod (ab_biprod A A) A $-> A
  := ab_codiagonal $o (functor_ab_biprod ab_codiagonal grp_homo_id).

(** For an abelian group [A], precomposing the triagonal on [A] with the twist map on [A] has no effect. *)
Definition ab_triagonal_twist {A : AbGroup}
  : ab_biprod_twist $o @ab_triagonal A = ab_triagonal
  := idpath.

(** A similar result for the cotriagonal. *)
Definition ab_cotriagonal_twist `{Funext} {A : AbGroup}
  : @ab_cotriagonal A $o ab_biprod_twist = ab_cotriagonal.
H: Funext
A: AbGroup
ab_cotriagonal $o ab_biprod_twist = ab_cotriagonal
Proof.
H: Funext
A: AbGroup
ab_cotriagonal $o ab_biprod_twist = ab_cotriagonal
  apply equiv_path_grouphomomorphism.
H: Funext
A: AbGroup
ab_cotriagonal $o ab_biprod_twist == ab_cotriagonal
  intro x.
H: Funext
A: AbGroup
x: ab_biprod (ab_biprod A A) A
(ab_cotriagonal $o ab_biprod_twist) x =
ab_cotriagonal x cbn.
H: Funext
A: AbGroup
x: ab_biprod (ab_biprod A A) A
snd x + snd (fst x) + fst (fst x) =
fst (fst x) + snd (fst x) + snd x
  refine ((grp_assoc _ _ _)^ @ _).
H: Funext
A: AbGroup
x: ab_biprod (ab_biprod A A) A
snd x + (snd (fst x) + fst (fst x)) =
fst (fst x) + snd (fst x) + snd x
  refine (abgroup_commutative _ _ _ @ _).
H: Funext
A: AbGroup
x: ab_biprod (ab_biprod A A) A
group_sgop (snd (fst x) + fst (fst x)) (snd x) =
fst (fst x) + snd (fst x) + snd x
  exact (ap (fun a =>  a + snd x) (abgroup_commutative _ _ _)).
Defined.