Require Import Basics Types Truncations.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat.Core HSet.
Require Export Algebra.Groups.Image 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 = mon_unit
  -
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 = mon_unit 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: {a : A &
ab_biprod_corec (ab_homo_negation $o f) g a =
(x, y)}
b x + c y = mon_unit
    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 = mon_unit 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 = mon_unit
    refine (ap (uncurry (fun x y => b x + c y)) 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)
uncurry (fun (x : B) (y : C) => b x + c y)
  (- f a, g a) = mon_unit
    unfold uncurry; 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) = mon_unit
    refine (ap011 sg_op (preserves_negate _) (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) = mon_unit
    exact (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.
A, B, C: AbGroup
f: A $-> B
g: A $-> C
a: A
(ab_pushout_inl $o f) a = (ab_pushout_inr $o g) a
  apply qglue; cbn.
A, B, C: AbGroup
f: A $-> B
g: A $-> C
a: A
Trunc (-1)
  {a0 : A &
  (- f a0, g a0) =
  (- f a + group_unit, - group_unit + g a)}
  apply tr.
A, B, C: AbGroup
f: A $-> B
g: A $-> C
a: A
{a0 : A &
(- f a0, g a0) =
(- f a + group_unit, - group_unit + g a)}
  exists a.
A, B, C: AbGroup
f: A $-> B
g: A $-> C
a: A
(- f a, 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 negate_mon_unit.
A, B, C: AbGroup
f: A $-> B
g: A $-> C
a: A
g a = mon_unit + 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 + mon_unit = 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
mon_unit + 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
      refine (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 + mon_unit = 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 refine (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; 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))
grp_homo_compose
  (ab_pushout_rec_uncurried f g Y (b; c; p))
  ab_pushout_inr = c
      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))
grp_homo_compose
  (ab_pushout_rec_uncurried f g Y (b; c; p))
  ab_pushout_inr == c
      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
      refine (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
mon_unit + 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
  rapply path_quotient.
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
isinj 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
  refine (_ o (path_ab_pushout f g (grp_prod_inl c0) (grp_prod_inl c1))^-1).
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
{a : A &
ab_biprod_corec (ab_homo_negation $o f) g a =
- 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 = mon_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)
a = mon_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 = mon_unit
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 = mon_unit 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 mon_unit
    refine (ap snd p @ _); cbn.
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 mon_unit
    exact (left_inverse mon_unit @ (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 = mon_unit
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 = mon_unit
mon_unit = - c0 + c1
    refine (_ @ ap fst p); cbn; 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 = mon_unit
- f a = mon_unit
    refine (_ @ negate_mon_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 = mon_unit
- f a = - mon_unit
    refine (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 = mon_unit
f a = mon_unit
    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. *)
Global 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.