Require Import Basics Types Truncations.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat.Core HSet.
Require Import Algebra.Groups.Group.
Require Export Algebra.Groups.QuotientGroup.
Require Import AbGroups.AbelianGroup AbGroups.Biproduct.

Local Open Scope mc_scope.
Local Open Scope mc_add_scope.

(** * Pushouts of abelian groups. *)

(** The pushout of two morphisms [f : A $-> B] and [g : A $-> C] is constructed as the quotient of the biproduct [B + C] by the image of [f - g]. Since this image comes up repeatedly, we name it. *)

Definition ab_pushout_subgroup {A B C : AbGroup} (f : A $-> B) (g : A $-> C)
  : Subgroup (ab_biprod B C)
  := grp_image (ab_biprod_corec (ab_homo_negation $o f) g).

Definition ab_pushout {A B C : AbGroup}
           (f : A $-> B) (g : A $-> C) : AbGroup
  := QuotientAbGroup (ab_biprod B C) (ab_pushout_subgroup f g).

(** Recursion principle. *)
Theorem ab_pushout_rec {A B C Y : AbGroup} {f : A $-> B} {g : A $-> C}
        (b : B $-> Y) (c : C $-> Y) (p : b o f == c o g)
  : ab_pushout f g $-> Y.
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: b o f == c o g
ab_pushout f g $-> Y
Proof.
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: b o f == c o g
ab_pushout f g $-> Y
  srapply grp_quotient_rec.
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: b o f == c o g
ab_biprod B C $-> Y
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: b o f == c o g
forall n : ab_biprod B C,
{|
  normalsubgroup_subgroup := ab_pushout_subgroup f g;
  normalsubgroup_isnormal :=
    isnormal_ab_subgroup (ab_biprod B C)
      (ab_pushout_subgroup f g)
|} n -> ?f n = 0
  -
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: b o f == c o g
ab_biprod B C $-> Y exact (ab_biprod_rec b c).
  -
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: b o f == c o g
forall n : ab_biprod B C,
{|
  normalsubgroup_subgroup := ab_pushout_subgroup f g;
  normalsubgroup_isnormal :=
    isnormal_ab_subgroup (ab_biprod B C)
      (ab_pushout_subgroup f g)
|} n -> ab_biprod_rec b c n = 0 intros [x y] q; strip_truncations; simpl.
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: b o f == c o g
x: B
y: C
q: {x0 : A &
ab_biprod_corec (ab_homo_negation $o f) g x0 =
(x, y)}
b x + c y = 0
    destruct q as [a q].
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: b o f == c o g
x: B
y: C
a: A
q: ab_biprod_corec (ab_homo_negation $o f) g a =
(x, y)
b x + c y = 0 cbn in q.
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: b o f == c o g
x: B
y: C
a: A
q: (- f a, g a) = (x, y)
b x + c y = 0
    lhs_V exact (ap (fun '(x, y) => b x + c y) q); cbn.
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: b o f == c o g
x: B
y: C
a: A
q: (- f a, g a) = (x, y)
b (- f a) + c (g a) = 0
    lhs rapply (ap011 (+) (preserves_inverse _) (p a)^).
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: b o f == c o g
x: B
y: C
a: A
q: (- f a, g a) = (x, y)
- b (f a) + b (f a) = 0
    apply left_inverse.
Defined.

Corollary ab_pushout_rec_uncurried {A B C : AbGroup}
          (f : A $-> B) (g : A $-> C) (Y : AbGroup)
  : {b : B $-> Y & {c : C $-> Y & b o f == c o g}}
      -> (ab_pushout f g $-> Y).
A, B, C: AbGroup
f: A $-> B
g: A $-> C
Y: AbGroup
{b : B $-> Y & {c : C $-> Y & b o f == c o g}} ->
ab_pushout f g $-> Y
Proof.
A, B, C: AbGroup
f: A $-> B
g: A $-> C
Y: AbGroup
{b : B $-> Y & {c : C $-> Y & b o f == c o g}} ->
ab_pushout f g $-> Y
  intros [b [c p]]; exact (ab_pushout_rec b c p).
Defined.

Definition ab_pushout_inl {A B C : AbGroup} {f : A $-> B} {g : A $-> C}
  : B $-> ab_pushout f g := grp_quotient_map $o grp_prod_inl.

Definition ab_pushout_inr {A B C : AbGroup} {f : A $-> B} {g : A $-> C}
  : C $-> ab_pushout f g := grp_quotient_map $o grp_prod_inr.

Proposition ab_pushout_commsq {A B C : AbGroup} {f : A $-> B} {g : A $-> C}
  : (@ab_pushout_inl A B C f g) $o f == ab_pushout_inr $o g.
A, B, C: AbGroup
f: A $-> B
g: A $-> C
ab_pushout_inl $o f == ab_pushout_inr $o g
Proof.
A, B, C: AbGroup
f: A $-> B
g: A $-> C
ab_pushout_inl $o f == ab_pushout_inr $o g
  intro a; simpl.
A, B, C: AbGroup
f: A $-> B
g: A $-> C
a: A
class_of
  (fun x y : B * C =>
   Tr (-1) {x0 : A & (- f x0, g x0) = - x + y})
  (f a, group_unit) =
class_of
  (fun x y : B * C =>
   Tr (-1) {x0 : A & (- f x0, g x0) = - x + y})
  (group_unit, g a)
  apply qglue, tr; exists a.
A, B, C: AbGroup
f: A $-> B
g: A $-> C
a: A
ab_biprod_corec (ab_homo_negation $o f) g a =
- (f a, group_unit) + (group_unit, g a)
  apply path_prod; simpl.
A, B, C: AbGroup
f: A $-> B
g: A $-> C
a: A
- f a = - f a + group_unit
A, B, C: AbGroup
f: A $-> B
g: A $-> C
a: A
g a = - group_unit + g a
  -
A, B, C: AbGroup
f: A $-> B
g: A $-> C
a: A
- f a = - f a + group_unit exact (right_identity _)^.
  -
A, B, C: AbGroup
f: A $-> B
g: A $-> C
a: A
g a = - group_unit + g a rewrite grp_inv_unit.
A, B, C: AbGroup
f: A $-> B
g: A $-> C
a: A
g a = 0 + g a
    exact (left_identity _)^.
Defined.

(** A map out of the pushout induces itself after restricting along the inclusions. *)
Proposition ab_pushout_rec_beta `{Funext} {A B C Y : AbGroup}
            {f : A $-> B} {g : A $-> C}
            (phi : ab_pushout f g $-> Y)
  : ab_pushout_rec (phi $o ab_pushout_inl) (phi $o ab_pushout_inr)
                   (fun a:A => ap phi (ab_pushout_commsq a)) = phi.
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
phi: ab_pushout f g $-> Y
ab_pushout_rec (phi $o ab_pushout_inl)
  (phi $o ab_pushout_inr)
  (fun a : A => ap phi (ab_pushout_commsq a)) = phi
Proof.
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
phi: ab_pushout f g $-> Y
ab_pushout_rec (phi $o ab_pushout_inl)
  (phi $o ab_pushout_inr)
  (fun a : A => ap phi (ab_pushout_commsq a)) = phi
  rapply (equiv_ap' (equiv_quotient_abgroup_ump (G:=ab_biprod B C) _ Y)^-1%equiv _ _)^-1.
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
phi: ab_pushout f g $-> Y
(equiv_quotient_abgroup_ump (ab_pushout_subgroup f g)
   Y)^-1%equiv
  (ab_pushout_rec (phi $o ab_pushout_inl)
     (phi $o ab_pushout_inr)
     (fun a : A => ap phi (ab_pushout_commsq a))) =
(equiv_quotient_abgroup_ump (ab_pushout_subgroup f g)
   Y)^-1%equiv phi
  srapply path_sigma_hprop.
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
phi: ab_pushout f g $-> Y
((equiv_quotient_abgroup_ump (ab_pushout_subgroup f g)
    Y)^-1%equiv
   (ab_pushout_rec (phi $o ab_pushout_inl)
      (phi $o ab_pushout_inr)
      (fun a : A => ap phi (ab_pushout_commsq a)))).1 =
((equiv_quotient_abgroup_ump (ab_pushout_subgroup f g)
    Y)^-1%equiv phi).1
  refine (grp_quotient_rec_beta _ Y _ _ @ _).
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
phi: ab_pushout f g $-> Y
ab_biprod_rec (phi $o ab_pushout_inl)
  (phi $o ab_pushout_inr) =
((equiv_quotient_abgroup_ump (ab_pushout_subgroup f g)
    Y)^-1%equiv phi).1
  apply equiv_path_grouphomomorphism; intro bc.
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
phi: ab_pushout f g $-> Y
bc: ab_biprod B C
ab_biprod_rec (phi $o ab_pushout_inl)
  (phi $o ab_pushout_inr) bc =
((equiv_quotient_abgroup_ump (ab_pushout_subgroup f g)
    Y)^-1%equiv phi).1 bc
  exact (ab_biprod_rec_eta (phi $o grp_quotient_map) bc).
Defined.

(** Restricting [ab_pushout_rec] along [ab_pushout_inl] recovers the left inducing map. *)
Lemma ab_pushout_rec_beta_left {A B C Y : AbGroup}
            (f : A $-> B) (g : A $-> C)
            (l : B $-> Y) (r : C $-> Y) (p : l o f == r o g)
  : ab_pushout_rec l r p $o ab_pushout_inl == l.
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
l: B $-> Y
r: C $-> Y
p: l o f == r o g
ab_pushout_rec l r p $o ab_pushout_inl == l
Proof.
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
l: B $-> Y
r: C $-> Y
p: l o f == r o g
ab_pushout_rec l r p $o ab_pushout_inl == l
  intro x; simpl.
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
l: B $-> Y
r: C $-> Y
p: l o f == r o g
x: B
l x + r group_unit = l x
  rewrite (grp_homo_unit r).
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
l: B $-> Y
r: C $-> Y
p: l o f == r o g
x: B
l x + 0 = l x
  apply right_identity.
Defined.

Lemma ab_pushout_rec_beta_right {A B C Y : AbGroup}
      (f : A $-> B) (g : A $-> C)
      (l : B $-> Y) (r : C $-> Y) (p : l o f == r o g)
  : ab_pushout_rec l r p $o ab_pushout_inr == r.
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
l: B $-> Y
r: C $-> Y
p: l o f == r o g
ab_pushout_rec l r p $o ab_pushout_inr == r
Proof.
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
l: B $-> Y
r: C $-> Y
p: l o f == r o g
ab_pushout_rec l r p $o ab_pushout_inr == r
  intro x; simpl.
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
l: B $-> Y
r: C $-> Y
p: l o f == r o g
x: C
l group_unit + r x = r x
  rewrite (grp_homo_unit l).
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
l: B $-> Y
r: C $-> Y
p: l o f == r o g
x: C
0 + r x = r x
  apply left_identity.
Defined.

Theorem isequiv_ab_pushout_rec `{Funext} {A B C Y : AbGroup}
        {f : A $-> B} {g : A $-> C}
  : IsEquiv (ab_pushout_rec_uncurried f g Y).
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
IsEquiv (ab_pushout_rec_uncurried f g Y)
Proof.
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
IsEquiv (ab_pushout_rec_uncurried f g Y)
  srapply isequiv_adjointify.
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
(ab_pushout f g $-> Y) ->
{b : B $-> Y & {c : C $-> Y & b o f == c o g}}
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
ab_pushout_rec_uncurried f g Y o ?g == idmap
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
?g o ab_pushout_rec_uncurried f g Y == idmap
  -
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
(ab_pushout f g $-> Y) ->
{b : B $-> Y & {c : C $-> Y & b o f == c o g}} intro phi.
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
phi: ab_pushout f g $-> Y
{b : B $-> Y & {c : C $-> Y & b o f == c o g}}
    refine (phi $o ab_pushout_inl; phi $o ab_pushout_inr; _).
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
phi: ab_pushout f g $-> Y
(fun x : A => (phi $o ab_pushout_inl) (f x)) ==
(fun x : A => (phi $o ab_pushout_inr) (g x))
    intro a.
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
phi: ab_pushout f g $-> Y
a: A
(phi $o ab_pushout_inl) (f a) =
(phi $o ab_pushout_inr) (g a)
    apply (ap phi).
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
phi: ab_pushout f g $-> Y
a: A
ab_pushout_inl (f a) = ab_pushout_inr (g a)
    exact (ab_pushout_commsq a).
  -
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
ab_pushout_rec_uncurried f g Y
o (fun phi : ab_pushout f g $-> Y =>
   (phi $o ab_pushout_inl; phi $o ab_pushout_inr;
   (fun a : A => ap phi (ab_pushout_commsq a))
   :
   (fun x : A => (phi $o ab_pushout_inl) (f x)) ==
   (fun x : A => (phi $o ab_pushout_inr) (g x)))) ==
idmap intro phi.
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
phi: ab_pushout f g $-> Y
ab_pushout_rec_uncurried f g Y
  (phi $o ab_pushout_inl; phi $o ab_pushout_inr;
  fun a : A => ap phi (ab_pushout_commsq a)) = phi
    exact (ab_pushout_rec_beta phi).
  -
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
(fun phi : ab_pushout f g $-> Y =>
 (phi $o ab_pushout_inl; phi $o ab_pushout_inr;
 (fun a : A => ap phi (ab_pushout_commsq a))
 :
 (fun x : A => (phi $o ab_pushout_inl) (f x)) ==
 (fun x : A => (phi $o ab_pushout_inr) (g x))))
o ab_pushout_rec_uncurried f g Y == idmap intros [b [c p]].
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: (fun x : A => b (f x)) == (fun x : A => c (g x))
(ab_pushout_rec_uncurried f g Y (b; c; p) $o
 ab_pushout_inl;
ab_pushout_rec_uncurried f g Y (b; c; p) $o
ab_pushout_inr;
fun a : A =>
ap (ab_pushout_rec_uncurried f g Y (b; c; p))
  (ab_pushout_commsq a)) = (b; c; p)
    srapply path_sigma.
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: (fun x : A => b (f x)) == (fun x : A => c (g x))
(ab_pushout_rec_uncurried f g Y (b; c; p) $o
 ab_pushout_inl;
ab_pushout_rec_uncurried f g Y (b; c; p) $o
ab_pushout_inr;
fun a : A =>
ap (ab_pushout_rec_uncurried f g Y (b; c; p))
  (ab_pushout_commsq a)).1 = (b; c; p).1
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: (fun x : A => b (f x)) == (fun x : A => c (g x))
transport
  (fun b : B $-> Y =>
   {c : C $-> Y &
   (fun x : A => b (f x)) == (fun x : A => c (g x))})
  ?p
  (ab_pushout_rec_uncurried f g Y (b; c; p) $o
   ab_pushout_inl;
  ab_pushout_rec_uncurried f g Y (b; c; p) $o
  ab_pushout_inr;
  fun a : A =>
  ap (ab_pushout_rec_uncurried f g Y (b; c; p))
    (ab_pushout_commsq a)).2 = (b; c; p).2
    +
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: (fun x : A => b (f x)) == (fun x : A => c (g x))
(ab_pushout_rec_uncurried f g Y (b; c; p) $o
 ab_pushout_inl;
ab_pushout_rec_uncurried f g Y (b; c; p) $o
ab_pushout_inr;
fun a : A =>
ap (ab_pushout_rec_uncurried f g Y (b; c; p))
  (ab_pushout_commsq a)).1 = (b; c; p).1 apply equiv_path_grouphomomorphism.
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: (fun x : A => b (f x)) == (fun x : A => c (g x))
(ab_pushout_rec_uncurried f g Y (b; c; p) $o
 ab_pushout_inl;
ab_pushout_rec_uncurried f g Y (b; c; p) $o
ab_pushout_inr;
fun a : A =>
ap (ab_pushout_rec_uncurried f g Y (b; c; p))
  (ab_pushout_commsq a)).1 == (b; c; p).1
      intro x; simpl.
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: (fun x : A => b (f x)) == (fun x : A => c (g x))
x: B
b x + c group_unit = b x
      lhs exact (ap (fun k => b x + k) (grp_homo_unit c)).
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: (fun x : A => b (f x)) == (fun x : A => c (g x))
x: B
b x + 0 = b x
      apply right_identity.
    +
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: (fun x : A => b (f x)) == (fun x : A => c (g x))
transport
  (fun b : B $-> Y =>
   {c : C $-> Y &
   (fun x : A => b (f x)) == (fun x : A => c (g x))})
  (let X := equiv_fun equiv_path_grouphomomorphism in
   X
     ((fun x : B =>
       ap (fun k : Y => b x + k) (grp_homo_unit c) @
       right_identity (b x)
       :
       (ab_pushout_rec_uncurried f g Y (b; c; p) $o
        ab_pushout_inl;
       ab_pushout_rec_uncurried f g Y (b; c; p) $o
       ab_pushout_inr;
       fun a : A =>
       ap (ab_pushout_rec_uncurried f g Y (b; c; p))
         (ab_pushout_commsq a)).1 x = (b; c; p).1 x)
      :
      (ab_pushout_rec_uncurried f g Y (b; c; p) $o
       ab_pushout_inl;
      ab_pushout_rec_uncurried f g Y (b; c; p) $o
      ab_pushout_inr;
      fun a : A =>
      ap (ab_pushout_rec_uncurried f g Y (b; c; p))
        (ab_pushout_commsq a)).1 == (b; c; p).1))
  (ab_pushout_rec_uncurried f g Y (b; c; p) $o
   ab_pushout_inl;
  ab_pushout_rec_uncurried f g Y (b; c; p) $o
  ab_pushout_inr;
  fun a : A =>
  ap (ab_pushout_rec_uncurried f g Y (b; c; p))
    (ab_pushout_commsq a)).2 = (b; c; p).2 lhs napply transport_sigma'.
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: (fun x : A => b (f x)) == (fun x : A => c (g x))
(((ab_pushout_rec_uncurried f g Y (b; c; p) $o
   ab_pushout_inl;
  ab_pushout_rec_uncurried f g Y (b; c; p) $o
  ab_pushout_inr;
  fun a : A =>
  ap (ab_pushout_rec_uncurried f g Y (b; c; p))
    (ab_pushout_commsq a)).2).1;
transport
  (fun x : B $-> Y =>
   (fun x0 : A => x (f x0)) ==
   (fun x0 : A =>
    ((ab_pushout_rec_uncurried f g Y (b; c; p) $o
      ab_pushout_inl;
     ab_pushout_rec_uncurried f g Y (b; c; p) $o
     ab_pushout_inr;
     fun a : A =>
     ap (ab_pushout_rec_uncurried f g Y (b; c; p))
       (ab_pushout_commsq a)).2).1 (g x0)))
  (let X := equiv_fun equiv_path_grouphomomorphism in
   X
     (fun x : B =>
      ap (fun k : Y => b x + k) (grp_homo_unit c) @
      right_identity (b x)))
  ((ab_pushout_rec_uncurried f g Y (b; c; p) $o
    ab_pushout_inl;
   ab_pushout_rec_uncurried f g Y (b; c; p) $o
   ab_pushout_inr;
   fun a : A =>
   ap (ab_pushout_rec_uncurried f g Y (b; c; p))
     (ab_pushout_commsq a)).2).2) = (b; c; p).2
      apply path_sigma_hprop.
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: (fun x : A => b (f x)) == (fun x : A => c (g x))
(((ab_pushout_rec_uncurried f g Y (b; c; p) $o
   ab_pushout_inl;
  ab_pushout_rec_uncurried f g Y (b; c; p) $o
  ab_pushout_inr;
  fun a : A =>
  ap (ab_pushout_rec_uncurried f g Y (b; c; p))
    (ab_pushout_commsq a)).2).1;
transport
  (fun x : B $-> Y =>
   (fun x0 : A => x (f x0)) ==
   (fun x0 : A =>
    ((ab_pushout_rec_uncurried f g Y (b; c; p) $o
      ab_pushout_inl;
     ab_pushout_rec_uncurried f g Y (b; c; p) $o
     ab_pushout_inr;
     fun a : A =>
     ap (ab_pushout_rec_uncurried f g Y (b; c; p))
       (ab_pushout_commsq a)).2).1 (g x0)))
  (let X := equiv_fun equiv_path_grouphomomorphism in
   X
     (fun x : B =>
      ap (fun k : Y => b x + k) (grp_homo_unit c) @
      right_identity (b x)))
  ((ab_pushout_rec_uncurried f g Y (b; c; p) $o
    ab_pushout_inl;
   ab_pushout_rec_uncurried f g Y (b; c; p) $o
   ab_pushout_inr;
   fun a : A =>
   ap (ab_pushout_rec_uncurried f g Y (b; c; p))
     (ab_pushout_commsq a)).2).2).1 = ((b; c; p).2).1
      apply equiv_path_grouphomomorphism.
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: (fun x : A => b (f x)) == (fun x : A => c (g x))
(((ab_pushout_rec_uncurried f g Y (b; c; p) $o
   ab_pushout_inl;
  ab_pushout_rec_uncurried f g Y (b; c; p) $o
  ab_pushout_inr;
  fun a : A =>
  ap (ab_pushout_rec_uncurried f g Y (b; c; p))
    (ab_pushout_commsq a)).2).1;
transport
  (fun x : B $-> Y =>
   (fun x0 : A => x (f x0)) ==
   (fun x0 : A =>
    ((ab_pushout_rec_uncurried f g Y (b; c; p) $o
      ab_pushout_inl;
     ab_pushout_rec_uncurried f g Y (b; c; p) $o
     ab_pushout_inr;
     fun a : A =>
     ap (ab_pushout_rec_uncurried f g Y (b; c; p))
       (ab_pushout_commsq a)).2).1 (g x0)))
  (let X := equiv_fun equiv_path_grouphomomorphism in
   X
     (fun x : B =>
      ap (fun k : Y => b x + k) (grp_homo_unit c) @
      right_identity (b x)))
  ((ab_pushout_rec_uncurried f g Y (b; c; p) $o
    ab_pushout_inl;
   ab_pushout_rec_uncurried f g Y (b; c; p) $o
   ab_pushout_inr;
   fun a : A =>
   ap (ab_pushout_rec_uncurried f g Y (b; c; p))
     (ab_pushout_commsq a)).2).2).1 == ((b; c; p).2).1
      intro y; simpl.
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: (fun x : A => b (f x)) == (fun x : A => c (g x))
y: C
b group_unit + c y = c y
      lhs exact (ap (fun k => k + c y) (grp_homo_unit b)).
H: Funext
A, B, C, Y: AbGroup
f: A $-> B
g: A $-> C
b: B $-> Y
c: C $-> Y
p: (fun x : A => b (f x)) == (fun x : A => c (g x))
y: C
0 + c y = c y
      apply left_identity.
Defined.

Definition path_ab_pushout `{Univalence} {A B C : AbGroup} (f : A $-> B) (g : A $-> C)
           (bc0 bc1 : ab_biprod B C)
  : @in_cosetL (ab_biprod B C) (ab_pushout_subgroup f g) bc0 bc1
               <~> (grp_quotient_map bc0 = grp_quotient_map bc1 :> ab_pushout f g).
H: Univalence
A, B, C: AbGroup
f: A $-> B
g: A $-> C
bc0, bc1: ab_biprod B C
in_cosetL (ab_pushout_subgroup f g) bc0 bc1 <~>
grp_quotient_map bc0 = grp_quotient_map bc1
Proof.
H: Univalence
A, B, C: AbGroup
f: A $-> B
g: A $-> C
bc0, bc1: ab_biprod B C
in_cosetL (ab_pushout_subgroup f g) bc0 bc1 <~>
grp_quotient_map bc0 = grp_quotient_map bc1
  napply path_quotient; exact _.
Defined.

(** The pushout of an embedding is an embedding. *)
Definition ab_pushout_embedding_inl `{Univalence} {A B C : AbGroup}
           (f : A $-> B) (g : A $-> C) `{IsEmbedding g}
  : IsEmbedding (ab_pushout_inl (f:=f) (g:=g)).
H: Univalence
A, B, C: AbGroup
f: A $-> B
g: A $-> C
IsEmbedding0: IsEmbedding g
IsEmbedding ab_pushout_inl
Proof.
H: Univalence
A, B, C: AbGroup
f: A $-> B
g: A $-> C
IsEmbedding0: IsEmbedding g
IsEmbedding ab_pushout_inl
  apply isembedding_isinj_hset.
H: Univalence
A, B, C: AbGroup
f: A $-> B
g: A $-> C
IsEmbedding0: IsEmbedding g
IsInjective ab_pushout_inl
  intros c0 c1.
H: Univalence
A, B, C: AbGroup
f: A $-> B
g: A $-> C
IsEmbedding0: IsEmbedding g
c0, c1: B
ab_pushout_inl c0 = ab_pushout_inl c1 -> c0 = c1
  nrefine (_ o (path_ab_pushout f g (grp_prod_inl c0) (grp_prod_inl c1))^-1%equiv).
H: Univalence
A, B, C: AbGroup
f: A $-> B
g: A $-> C
IsEmbedding0: IsEmbedding g
c0, c1: B
in_cosetL (ab_pushout_subgroup f g) 
  (grp_prod_inl c0) (grp_prod_inl c1) -> 
c0 = c1
  rapply Trunc_ind.
H: Univalence
A, B, C: AbGroup
f: A $-> B
g: A $-> C
IsEmbedding0: IsEmbedding g
c0, c1: B
{x : A &
ab_biprod_corec (ab_homo_negation $o f) g x =
- grp_prod_inl c0 + grp_prod_inl c1} -> 
c0 = c1
  cbn; intros [a p].
H: Univalence
A, B, C: AbGroup
f: A $-> B
g: A $-> C
IsEmbedding0: IsEmbedding g
c0, c1: B
a: A
p: (- f a, g a) =
(- c0 + c1, - group_unit + group_unit)
c0 = c1
  assert (z : a = 0).
H: Univalence
A, B, C: AbGroup
f: A $-> B
g: A $-> C
IsEmbedding0: IsEmbedding g
c0, c1: B
a: A
p: (- f a, g a) =
(- c0 + c1, - group_unit + group_unit)
a = 0
H: Univalence
A, B, C: AbGroup
f: A $-> B
g: A $-> C
IsEmbedding0: IsEmbedding g
c0, c1: B
a: A
p: (- f a, g a) =
(- c0 + c1, - group_unit + group_unit)
z: a = 0
c0 = c1
  -
H: Univalence
A, B, C: AbGroup
f: A $-> B
g: A $-> C
IsEmbedding0: IsEmbedding g
c0, c1: B
a: A
p: (- f a, g a) =
(- c0 + c1, - group_unit + group_unit)
a = 0 rapply (isinj_embedding g).
H: Univalence
A, B, C: AbGroup
f: A $-> B
g: A $-> C
IsEmbedding0: IsEmbedding g
c0, c1: B
a: A
p: (- f a, g a) =
(- c0 + c1, - group_unit + group_unit)
g a = g 0
    lhs exact (ap snd p); unfold snd.
H: Univalence
A, B, C: AbGroup
f: A $-> B
g: A $-> C
IsEmbedding0: IsEmbedding g
c0, c1: B
a: A
p: (- f a, g a) =
(- c0 + c1, - group_unit + group_unit)
- group_unit + group_unit = g 0
    exact (left_inverse 0 @ (grp_homo_unit g)^).
  -
H: Univalence
A, B, C: AbGroup
f: A $-> B
g: A $-> C
IsEmbedding0: IsEmbedding g
c0, c1: B
a: A
p: (- f a, g a) =
(- c0 + c1, - group_unit + group_unit)
z: a = 0
c0 = c1 apply grp_moveR_M1.
H: Univalence
A, B, C: AbGroup
f: A $-> B
g: A $-> C
IsEmbedding0: IsEmbedding g
c0, c1: B
a: A
p: (- f a, g a) =
(- c0 + c1, - group_unit + group_unit)
z: a = 0
0 = - c0 + c1
    rhs_V exact (ap fst p); unfold fst; symmetry.
H: Univalence
A, B, C: AbGroup
f: A $-> B
g: A $-> C
IsEmbedding0: IsEmbedding g
c0, c1: B
a: A
p: (- f a, g a) =
(- c0 + c1, - group_unit + group_unit)
z: a = 0
- f a = 0
    rhs_V napply grp_inv_unit.
H: Univalence
A, B, C: AbGroup
f: A $-> B
g: A $-> C
IsEmbedding0: IsEmbedding g
c0, c1: B
a: A
p: (- f a, g a) =
(- c0 + c1, - group_unit + group_unit)
z: a = 0
- f a = - 0
    apply ap.
H: Univalence
A, B, C: AbGroup
f: A $-> B
g: A $-> C
IsEmbedding0: IsEmbedding g
c0, c1: B
a: A
p: (- f a, g a) =
(- c0 + c1, - group_unit + group_unit)
z: a = 0
f a = 0
    exact (ap f z @ grp_homo_unit f).
Defined.

(** Functoriality of pushouts *)
Definition functor_ab_pushout {A A' B B' C C' : AbGroup}
           (f : A $-> B) (f' : A' $-> B')
           (g : A $-> C) (g' : A' $-> C')
           (alpha : A $-> A') (beta : B $-> B') (gamma : C $-> C')
           (h : beta $o f == f' $o alpha) (k : g' $o alpha == gamma $o g)
  : ab_pushout f g $-> ab_pushout f' g'.
A, A', B, B', C, C': AbGroup
f: A $-> B
f': A' $-> B'
g: A $-> C
g': A' $-> C'
alpha: A $-> A'
beta: B $-> B'
gamma: C $-> C'
h: beta $o f == f' $o alpha
k: g' $o alpha == gamma $o g
ab_pushout f g $-> ab_pushout f' g'
Proof.
A, A', B, B', C, C': AbGroup
f: A $-> B
f': A' $-> B'
g: A $-> C
g': A' $-> C'
alpha: A $-> A'
beta: B $-> B'
gamma: C $-> C'
h: beta $o f == f' $o alpha
k: g' $o alpha == gamma $o g
ab_pushout f g $-> ab_pushout f' g'
  srapply ab_pushout_rec.
A, A', B, B', C, C': AbGroup
f: A $-> B
f': A' $-> B'
g: A $-> C
g': A' $-> C'
alpha: A $-> A'
beta: B $-> B'
gamma: C $-> C'
h: beta $o f == f' $o alpha
k: g' $o alpha == gamma $o g
B $-> ab_pushout f' g'
A, A', B, B', C, C': AbGroup
f: A $-> B
f': A' $-> B'
g: A $-> C
g': A' $-> C'
alpha: A $-> A'
beta: B $-> B'
gamma: C $-> C'
h: beta $o f == f' $o alpha
k: g' $o alpha == gamma $o g
C $-> ab_pushout f' g'
A, A', B, B', C, C': AbGroup
f: A $-> B
f': A' $-> B'
g: A $-> C
g': A' $-> C'
alpha: A $-> A'
beta: B $-> B'
gamma: C $-> C'
h: beta $o f == f' $o alpha
k: g' $o alpha == gamma $o g
?b o f == ?c o g
  -
A, A', B, B', C, C': AbGroup
f: A $-> B
f': A' $-> B'
g: A $-> C
g': A' $-> C'
alpha: A $-> A'
beta: B $-> B'
gamma: C $-> C'
h: beta $o f == f' $o alpha
k: g' $o alpha == gamma $o g
B $-> ab_pushout f' g' exact (ab_pushout_inl $o beta).
  -
A, A', B, B', C, C': AbGroup
f: A $-> B
f': A' $-> B'
g: A $-> C
g': A' $-> C'
alpha: A $-> A'
beta: B $-> B'
gamma: C $-> C'
h: beta $o f == f' $o alpha
k: g' $o alpha == gamma $o g
C $-> ab_pushout f' g' exact (ab_pushout_inr $o gamma).
  -
A, A', B, B', C, C': AbGroup
f: A $-> B
f': A' $-> B'
g: A $-> C
g': A' $-> C'
alpha: A $-> A'
beta: B $-> B'
gamma: C $-> C'
h: beta $o f == f' $o alpha
k: g' $o alpha == gamma $o g
ab_pushout_inl $o beta o f ==
ab_pushout_inr $o gamma o g intro a.
A, A', B, B', C, C': AbGroup
f: A $-> B
f': A' $-> B'
g: A $-> C
g': A' $-> C'
alpha: A $-> A'
beta: B $-> B'
gamma: C $-> C'
h: beta $o f == f' $o alpha
k: g' $o alpha == gamma $o g
a: A
(ab_pushout_inl $o beta) (f a) =
(ab_pushout_inr $o gamma) (g a)
    refine (ap ab_pushout_inl (h a) @ _ @ ap ab_pushout_inr (k a)).
A, A', B, B', C, C': AbGroup
f: A $-> B
f': A' $-> B'
g: A $-> C
g': A' $-> C'
alpha: A $-> A'
beta: B $-> B'
gamma: C $-> C'
h: beta $o f == f' $o alpha
k: g' $o alpha == gamma $o g
a: A
ab_pushout_inl ((f' $o alpha) a) =
ab_pushout_inr ((g' $o alpha) a)
    exact (ab_pushout_commsq (alpha a)).
Defined.

(** ** Properties of pushouts of maps *)

(** The pushout of an epimorphism is an epimorphism. *)
Instance ab_pushout_surjection_inr {A B C : AbGroup}
  (f : A $-> B) (g : A $-> C) `{S : IsSurjection f}
  : IsSurjection (ab_pushout_inr (f:=f) (g:=g)).
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
ReflectiveSubuniverse.IsConnMap (Tr (-1))
  ab_pushout_inr
Proof.
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
ReflectiveSubuniverse.IsConnMap (Tr (-1))
  ab_pushout_inr
  intro x.
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
ReflectiveSubuniverse.IsConnected (Tr (-1))
  (hfiber ab_pushout_inr x)
  rapply contr_inhabited_hprop.
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
Tr (-1) (hfiber ab_pushout_inr x)
  (* To find a preimage of [x], we may first choose a representative [x']. *)
  assert (x' : merely (hfiber grp_quotient_map x)).
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
merely (hfiber grp_quotient_map x)
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
x': merely (hfiber grp_quotient_map x)
Tr (-1) (hfiber ab_pushout_inr x)
  1: apply center, issurj_class_of.
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
x': merely (hfiber grp_quotient_map x)
Tr (-1) (hfiber ab_pushout_inr x)
  strip_truncations; destruct x' as [[b c] p].
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
b: B
c: C
p: grp_quotient_map (b, c) = x
Tr (-1) (hfiber ab_pushout_inr x)
  (* Now [x] = [b + c] in the quotient. We find a preimage of [a]. *)
  assert (a : merely (hfiber f b)).
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
b: B
c: C
p: grp_quotient_map (b, c) = x
merely (hfiber f b)
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
b: B
c: C
p: grp_quotient_map (b, c) = x
a: merely (hfiber f b)
Tr (-1) (hfiber ab_pushout_inr x)
  1: apply center, S.
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
b: B
c: C
p: grp_quotient_map (b, c) = x
a: merely (hfiber f b)
Tr (-1) (hfiber ab_pushout_inr x)
  strip_truncations; destruct a as [a q].
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
b: B
c: C
p: grp_quotient_map (b, c) = x
a: A
q: f a = b
Tr (-1) (hfiber ab_pushout_inr x)
  refine (tr (g a + c; _)).
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
b: B
c: C
p: grp_quotient_map (b, c) = x
a: A
q: f a = b
ab_pushout_inr (g a + c) = x
  refine (grp_homo_op _ _ _ @ _).
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
b: B
c: C
p: grp_quotient_map (b, c) = x
a: A
q: f a = b
ab_pushout_inr (g a) + ab_pushout_inr c = x
  refine (ap (fun z => sg_op z _) _^ @ _).
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
b: B
c: C
p: grp_quotient_map (b, c) = x
a: A
q: f a = b
?Goal = ab_pushout_inr (g a)
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
b: B
c: C
p: grp_quotient_map (b, c) = x
a: A
q: f a = b
?Goal + ab_pushout_inr c = x
  {
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
b: B
c: C
p: grp_quotient_map (b, c) = x
a: A
q: f a = b
?Goal = ab_pushout_inr (g a) refine (_^ @ ab_pushout_commsq _).
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
b: B
c: C
p: grp_quotient_map (b, c) = x
a: A
q: f a = b
(ab_pushout_inl $o f) a = ?Goal
    exact (ap _ q). }
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
b: B
c: C
p: grp_quotient_map (b, c) = x
a: A
q: f a = b
ab_pushout_inl b + ab_pushout_inr c = x
  refine (ap grp_quotient_map _ @ p).
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
b: B
c: C
p: grp_quotient_map (b, c) = x
a: A
q: f a = b
grp_prod_inl b + grp_prod_inr c = (b, c)
  apply path_prod'; cbn.
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
b: B
c: C
p: grp_quotient_map (b, c) = x
a: A
q: f a = b
b + group_unit = b
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
b: B
c: C
p: grp_quotient_map (b, c) = x
a: A
q: f a = b
group_unit + c = c
  -
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
b: B
c: C
p: grp_quotient_map (b, c) = x
a: A
q: f a = b
b + group_unit = b apply right_identity.
  -
A, B, C: AbGroup
f: A $-> B
g: A $-> C
S: ReflectiveSubuniverse.IsConnMap (Tr (-1)) f
x: ab_pushout f g
b: B
c: C
p: grp_quotient_map (b, c) = x
a: A
q: f a = b
group_unit + c = c apply left_identity.
Defined.