From HoTT Require Import Basics Types Truncations.Core.From HoTT Require Import Basics Types Truncations.Core.
From HoTT.WildCat Require Import Core Equiv Bifunctor.
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 sg_op
  intros [a b] [a' b'].
A, B: AbGroup
a: A
b: B
a': A
b': B
(a, b) + (a', b') = (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.

Definition ab_biprod_ind {A B : AbGroup}
  (P : ab_biprod A B -> Type)
  (Hinl : forall a, P (ab_biprod_inl a))
  (Hinr : forall b, P (ab_biprod_inr b))
  (Hop : forall x y, P x -> P y -> P (x + y))
  : forall x, P x.
A, B: AbGroup
P: ab_biprod A B -> Type
Hinl: forall a : A, P (ab_biprod_inl a)
Hinr: forall b : B, P (ab_biprod_inr b)
Hop: forall x y : ab_biprod A B, P x -> P y -> P (x + y)
forall x : ab_biprod A B, P x
Proof.
A, B: AbGroup
P: ab_biprod A B -> Type
Hinl: forall a : A, P (ab_biprod_inl a)
Hinr: forall b : B, P (ab_biprod_inr b)
Hop: forall x y : ab_biprod A B, P x -> P y -> P (x + y)
forall x : ab_biprod A B, P x
  intros [a b].
A, B: AbGroup
P: ab_biprod A B -> Type
Hinl: forall a0 : A, P (ab_biprod_inl a0)
Hinr: forall b0 : B, P (ab_biprod_inr b0)
Hop: forall x y : ab_biprod A B, P x -> P y -> P (x + y)
a: A
b: B
P (a, b)
  snapply ((grp_prod_decompose a b)^ # _).
A, B: AbGroup
P: ab_biprod A B -> Type
Hinl: forall a0 : A, P (ab_biprod_inl a0)
Hinr: forall b0 : B, P (ab_biprod_inr b0)
Hop: forall x y : ab_biprod A B, P x -> P y -> P (x + y)
a: A
b: B
P (((a, 0) : grp_prod A B) + (0, b))
  apply Hop.
A, B: AbGroup
P: ab_biprod A B -> Type
Hinl: forall a0 : A, P (ab_biprod_inl a0)
Hinr: forall b0 : B, P (ab_biprod_inr b0)
Hop: forall x y : ab_biprod A B, P x -> P y -> P (x + y)
a: A
b: B
P (a, 0)
A, B: AbGroup
P: ab_biprod A B -> Type
Hinl: forall a0 : A, P (ab_biprod_inl a0)
Hinr: forall b0 : B, P (ab_biprod_inr b0)
Hop: forall x y : ab_biprod A B, P x -> P y -> P (x + y)
a: A
b: B
P (0, b)
  -
A, B: AbGroup
P: ab_biprod A B -> Type
Hinl: forall a0 : A, P (ab_biprod_inl a0)
Hinr: forall b0 : B, P (ab_biprod_inr b0)
Hop: forall x y : ab_biprod A B, P x -> P y -> P (x + y)
a: A
b: B
P (a, 0) exact (Hinl a).
  -
A, B: AbGroup
P: ab_biprod A B -> Type
Hinl: forall a0 : A, P (ab_biprod_inl a0)
Hinr: forall b0 : B, P (ab_biprod_inr b0)
Hop: forall x y : ab_biprod A B, P x -> P y -> P (x + y)
a: A
b: B
P (0, b) exact (Hinr b).
Defined.

Definition ab_biprod_ind_homotopy {A B C : AbGroup}
  {f g : ab_biprod A B $-> C}
  (Hinl : f $o ab_biprod_inl $== g $o ab_biprod_inl)
  (Hinr : f $o ab_biprod_inr $== g $o ab_biprod_inr)
  : f $== g.
A, B, C: AbGroup
f, g: ab_biprod A B $-> C
Hinl: f $o ab_biprod_inl $== g $o ab_biprod_inl
Hinr: f $o ab_biprod_inr $== g $o ab_biprod_inr
f $== g
Proof.
A, B, C: AbGroup
f, g: ab_biprod A B $-> C
Hinl: f $o ab_biprod_inl $== g $o ab_biprod_inl
Hinr: f $o ab_biprod_inr $== g $o ab_biprod_inr
f $== g
  rapply ab_biprod_ind.
A, B, C: AbGroup
f, g: ab_biprod A B $-> C
Hinl: f $o ab_biprod_inl $== g $o ab_biprod_inl
Hinr: f $o ab_biprod_inr $== g $o ab_biprod_inr
forall a : A, f (ab_biprod_inl a) = g (ab_biprod_inl a)
A, B, C: AbGroup
f, g: ab_biprod A B $-> C
Hinl: f $o ab_biprod_inl $== g $o ab_biprod_inl
Hinr: f $o ab_biprod_inr $== g $o ab_biprod_inr
forall b : B, f (ab_biprod_inr b) = g (ab_biprod_inr b)
A, B, C: AbGroup
f, g: ab_biprod A B $-> C
Hinl: f $o ab_biprod_inl $== g $o ab_biprod_inl
Hinr: f $o ab_biprod_inr $== g $o ab_biprod_inr
forall x y : ab_biprod A B, f x = g x -> f y = g y -> f (x + y) = g (x + y)
  -
A, B, C: AbGroup
f, g: ab_biprod A B $-> C
Hinl: f $o ab_biprod_inl $== g $o ab_biprod_inl
Hinr: f $o ab_biprod_inr $== g $o ab_biprod_inr
forall a : A, f (ab_biprod_inl a) = g (ab_biprod_inl a) exact Hinl.
  -
A, B, C: AbGroup
f, g: ab_biprod A B $-> C
Hinl: f $o ab_biprod_inl $== g $o ab_biprod_inl
Hinr: f $o ab_biprod_inr $== g $o ab_biprod_inr
forall b : B, f (ab_biprod_inr b) = g (ab_biprod_inr b) exact Hinr.
  -
A, B, C: AbGroup
f, g: ab_biprod A B $-> C
Hinl: f $o ab_biprod_inl $== g $o ab_biprod_inl
Hinr: f $o ab_biprod_inr $== g $o ab_biprod_inr
forall x y : ab_biprod A B, f x = g x -> f y = g y -> f (x + y) = g (x + y) intros x y p q.
A, B, C: AbGroup
f, g: ab_biprod A B $-> C
Hinl: f $o ab_biprod_inl $== g $o ab_biprod_inl
Hinr: f $o ab_biprod_inr $== g $o ab_biprod_inr
x, y: ab_biprod A B
p: f x = g x
q: f y = g y
f (x + y) = g (x + y)
    lhs napply grp_homo_op.
A, B, C: AbGroup
f, g: ab_biprod A B $-> C
Hinl: f $o ab_biprod_inl $== g $o ab_biprod_inl
Hinr: f $o ab_biprod_inr $== g $o ab_biprod_inr
x, y: ab_biprod A B
p: f x = g x
q: f y = g y
f x + f y = g (x + y)
    rhs napply grp_homo_op.
A, B, C: AbGroup
f, g: ab_biprod A B $-> C
Hinl: f $o ab_biprod_inl $== g $o ab_biprod_inl
Hinr: f $o ab_biprod_inr $== g $o ab_biprod_inr
x, y: ab_biprod A B
p: f x = g x
q: f y = g y
f x + f y = g x + g y
    f_ap.
Defined.

(* Maps out of biproducts are determined on the two inclusions. *)
Definition equiv_ab_biprod_ind_homotopy `{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 exact (uncurry ab_biprod_ind_homotopy).
  -
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) exact (fun h => (fun a => h _, fun b => h _)).
Defined.

(** 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
  snapply 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 ?grp_homo_map
  -
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_beta_inl {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 + 0 = a x
  exact (right_identity (a x)).
Defined.

Proposition ab_biprod_rec_beta_inr {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
0 + 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_beta_inl.
    +
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_beta_inr.
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.

(** *** 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.

Instance is0bifunctor_ab_biprod : Is0Bifunctor ab_biprod.
Is0Bifunctor ab_biprod
Proof.
Is0Bifunctor ab_biprod
  srapply Build_Is0Bifunctor'.
Is0Functor (uncurry ab_biprod)
  snapply Build_Is0Functor.
forall a b : AbGroup * AbGroup,
(a $-> b) -> uncurry ab_biprod a $-> uncurry ab_biprod b
  intros [A B] [A' B'] [f g].
A, B, A', B': AbGroup
f: fst (A, B) $-> fst (A', B')
g: snd (A, B) $-> snd (A', B')
uncurry ab_biprod (A, B) $-> uncurry ab_biprod (A', B')
  exact (functor_ab_biprod f g).
Defined.

Instance is1bifunctor_ab_biprod : Is1Bifunctor ab_biprod.
Is1Bifunctor ab_biprod
Proof.
Is1Bifunctor ab_biprod
  snapply Build_Is1Bifunctor'.
Is1Functor (uncurry ab_biprod)
  snapply Build_Is1Functor.
forall (a b : AbGroup * AbGroup) (f g : a $-> b),
f $== g -> fmap (uncurry ab_biprod) f $== fmap (uncurry ab_biprod) g
forall a : AbGroup * AbGroup,
fmap (uncurry ab_biprod) (Id a) $== Id (uncurry ab_biprod a)
forall (a b c : AbGroup * AbGroup) (f : a $-> b) (g : b $-> c),
fmap (uncurry ab_biprod) (g $o f) $==
fmap (uncurry ab_biprod) g $o fmap (uncurry ab_biprod) f
  -
forall (a b : AbGroup * AbGroup) (f g : a $-> b),
f $== g -> fmap (uncurry ab_biprod) f $== fmap (uncurry ab_biprod) g intros [A B] [A' B'] [f g] [f' g'] [p q] [a b].
A, B, A', B': AbGroup
f: fst (A, B) $-> fst (A', B')
g: snd (A, B) $-> snd (A', B')
f': fst (A, B) $-> fst (A', B')
g': snd (A, B) $-> snd (A', B')
p: fst (f, g) $-> fst (f', g')
q: snd (f, g) $-> snd (f', g')
a: fst (A, B)
b: snd (A, B)
fmap (uncurry ab_biprod) (f, g) (a, b) =
fmap (uncurry ab_biprod) (f', g') (a, b)
    snapply equiv_path_prod.
A, B, A', B': AbGroup
f: fst (A, B) $-> fst (A', B')
g: snd (A, B) $-> snd (A', B')
f': fst (A, B) $-> fst (A', B')
g': snd (A, B) $-> snd (A', B')
p: fst (f, g) $-> fst (f', g')
q: snd (f, g) $-> snd (f', g')
a: fst (A, B)
b: snd (A, B)
(fst (fmap (uncurry ab_biprod) (f, g) (a, b)) =
 fst (fmap (uncurry ab_biprod) (f', g') (a, b))) *
(snd (fmap (uncurry ab_biprod) (f, g) (a, b)) =
 snd (fmap (uncurry ab_biprod) (f', g') (a, b)))
    exact (p a, q b).
  -
forall a : AbGroup * AbGroup,
fmap (uncurry ab_biprod) (Id a) $== Id (uncurry ab_biprod a) reflexivity.
  -
forall (a b c : AbGroup * AbGroup) (f : a $-> b) (g : b $-> c),
fmap (uncurry ab_biprod) (g $o f) $==
fmap (uncurry ab_biprod) g $o fmap (uncurry ab_biprod) f cbn; reflexivity.
Defined.

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 H1 : GroupIsomorphism A A' =>
       grp_iso_homo A' A (grp_iso_inverse H1) in
     X {| grp_iso_homo := f; isequiv_group_iso := H |})
    (let X :=
       fun H1 : GroupIsomorphism B B' =>
       grp_iso_homo B' B (grp_iso_inverse H1) 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 H1 : GroupIsomorphism A A' => grp_iso_homo A' A (grp_iso_inverse H1)
     in
   X {| grp_iso_homo := f; isequiv_group_iso := H |})
  (let X :=
     fun H1 : GroupIsomorphism B B' => grp_iso_homo B' B (grp_iso_inverse H1)
     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 + 0 = 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
0 + 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 + 0 = 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
0 + p' a'.1 = b' exact (left_identity _ @ a'.2).
Defined.

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

(** 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
  snapply 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
  snapply 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
  snapply 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) snapply 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 ?grp_homo_map
    +
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
  {|
    grp_homo_map :=
      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);
    issemigrouppreserving_grp_homo :=
      (fun x y : ab_biprod (ab_biprod A B) C => 1)
      :
      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))
  |} snapply isequiv_adjointify.
A, B, C: AbGroup
ab_biprod (ab_biprod C B) A -> ab_biprod (ab_biprod A B) C
A, B, C: AbGroup
{|
  grp_homo_map :=
    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);
  issemigrouppreserving_grp_homo :=
    (fun x y : ab_biprod (ab_biprod A B) C => 1)
    :
    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))
|} o ?g == idmap
A, B, C: AbGroup
?g
o {|
    grp_homo_map :=
      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);
    issemigrouppreserving_grp_homo :=
      (fun x y : ab_biprod (ab_biprod A B) C => 1)
      :
      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))
  |} ==
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
{|
  grp_homo_map :=
    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);
  issemigrouppreserving_grp_homo :=
    (fun x y : ab_biprod (ab_biprod A B) C => 1)
    :
    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))
|}
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 {|
    grp_homo_map :=
      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);
    issemigrouppreserving_grp_homo :=
      (fun x y : ab_biprod (ab_biprod A B) C => 1)
      :
      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))
  |} ==
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
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.