From HoTT Require Import Basics Types Truncations.Core.From HoTT Require Import Basics Types Truncations.Core.
From HoTT.WildCat Require Import Core Universe Opposite NatTrans.
Require Import Pointed.Core Homotopy.ExactSequence HIT.epi.
Require Import Modalities.ReflectiveSubuniverse.
Require Import AbelianGroup AbPushout AbHom AbGroups.Biproduct.
Require Import AbSES.Core AbSES.DirectSum.

Local Open Scope pointed_scope.
Local Open Scope type_scope.
Local Open Scope path_scope.
Local Open Scope mc_add_scope.

(** * Pushouts of short exact sequences *)

Definition abses_pushout `{Univalence} {A A' B : AbGroup} (f : A $-> A')
  : AbSES B A -> AbSES B A'.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
AbSES B A -> AbSES B A'
Proof.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
AbSES B A -> AbSES B A'
  intro E.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
AbSES B A'
  snapply (Build_AbSES (ab_pushout f (inclusion E))
                        ab_pushout_inl
                        (ab_pushout_rec grp_homo_const (projection E) _)).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
grp_homo_const o f == projection E o inclusion E
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
IsEmbedding ab_pushout_inl
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
IsConnMap (Tr (-1)) (ab_pushout_rec grp_homo_const (projection E) ?p)
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
IsExact (Tr (-1)) ab_pushout_inl
  (ab_pushout_rec grp_homo_const (projection E) ?p)
  -
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
grp_homo_const o f == projection E o inclusion E symmetry; rapply iscomplex_abses.
  -
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
IsEmbedding ab_pushout_inl rapply ab_pushout_embedding_inl.
  -
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
IsConnMap (Tr (-1))
  (ab_pushout_rec grp_homo_const (projection E)
     ((fun (x y : A -> B) (p : x == y) (x0 : A) => (p x0)^)
        (projection E o inclusion E) (grp_homo_const o f) 
        (iscomplex_abses E))) napply (cancelR_issurjection ab_pushout_inr _).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
IsConnMap (Tr (-1))
  (fun x : E =>
   ab_pushout_rec grp_homo_const (projection E)
     (fun x0 : A => (iscomplex_abses E x0)^) (ab_pushout_inr x))
    rapply (conn_map_homotopic _ (projection E)); symmetry.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
(fun x : E =>
 ab_pushout_rec grp_homo_const (projection E)
   (fun x0 : A => (iscomplex_abses E x0)^) (ab_pushout_inr x)) ==
projection E
    napply ab_pushout_rec_beta_right.
  -
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
IsExact (Tr (-1)) ab_pushout_inl
  (ab_pushout_rec grp_homo_const (projection E)
     ((fun (x y : A -> B) (p : x == y) (x0 : A) => (p x0)^)
        (projection E o inclusion E) (grp_homo_const o f) 
        (iscomplex_abses E))) snapply Build_IsExact.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
IsComplex ab_pushout_inl
  (ab_pushout_rec grp_homo_const (projection E)
     ((fun (x y : A -> B) (p : x == y) (x0 : A) => (p x0)^)
        (projection E o inclusion E) (grp_homo_const o f) 
        (iscomplex_abses E)))
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
IsConnMap (Tr (-1)) (cxfib ?cx_isexact)
    +
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
IsComplex ab_pushout_inl
  (ab_pushout_rec grp_homo_const (projection E)
     ((fun (x y : A -> B) (p : x == y) (x0 : A) => (p x0)^)
        (projection E o inclusion E) (grp_homo_const o f) 
        (iscomplex_abses E))) srapply phomotopy_homotopy_hset.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
ab_pushout_rec grp_homo_const (projection E)
  ((fun (x y : A -> B) (p : x == y) (x0 : A) => (p x0)^)
     (projection E o inclusion E) (grp_homo_const o f) 
     (iscomplex_abses E))
o* ab_pushout_inl == pconst
      napply ab_pushout_rec_beta_left.
    +
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
IsConnMap (Tr (-1))
  (cxfib
     (phomotopy_homotopy_hset
        (ab_pushout_rec_beta_left f (inclusion E) grp_homo_const
           (projection E) (fun x0 : A => (iscomplex_abses E x0)^)))) intros [bc' p].
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (ab_pushout_rec_beta_left f (inclusion E) grp_homo_const
              (projection E) (fun x0 : A => (iscomplex_abses E x0)^))))
     (bc'; p))
      rapply contr_inhabited_hprop.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (ab_pushout_rec_beta_left f (inclusion E) grp_homo_const
              (projection E) (fun x0 : A => (iscomplex_abses E x0)^))))
     (bc'; p))
      (** Pick a preimage under the quotient map. *)
      assert (bc : merely (hfiber grp_quotient_map bc')).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
merely (hfiber grp_quotient_map bc')
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
bc: merely (hfiber grp_quotient_map bc')
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (ab_pushout_rec_beta_left f (inclusion E) grp_homo_const
              (projection E) (fun x0 : A => (iscomplex_abses E x0)^))))
     (bc'; p))
      1: apply center, issurj_class_of.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
bc: merely (hfiber grp_quotient_map bc')
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (ab_pushout_rec_beta_left f (inclusion E) grp_homo_const
              (projection E) (fun x0 : A => (iscomplex_abses E x0)^))))
     (bc'; p))
      strip_truncations.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
bc: hfiber grp_quotient_map bc'
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (ab_pushout_rec_beta_left f (inclusion E) grp_homo_const
              (projection E) (fun x0 : A => (iscomplex_abses E x0)^))))
     (bc'; p))
      destruct bc as [[b c] q].
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (ab_pushout_rec_beta_left f (inclusion E) grp_homo_const
              (projection E) (fun x0 : A => (iscomplex_abses E x0)^))))
     (bc'; p))
      (** The E-component of the preimage is in the kernel of [projection E]. *)
      assert (c_in_kernel : (projection E) c = mon_unit).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
projection E c = 0
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
c_in_kernel: projection E c = 0
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (ab_pushout_rec_beta_left f (inclusion E) grp_homo_const
              (projection E) (fun x0 : A => (iscomplex_abses E x0)^))))
     (bc'; p))
      1: {
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
projection E c = 0 refine (_ @ p); symmetry.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
projection E c
           rewrite <- q; simpl.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
group_unit + projection E c = projection E c
           apply left_identity. }
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
c_in_kernel: projection E c = 0
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (ab_pushout_rec_beta_left f (inclusion E) grp_homo_const
              (projection E) (fun x0 : A => (iscomplex_abses E x0)^))))
     (bc'; p))
      (** By exactness, we get an element in [A]. *)
      pose proof (a := isexact_preimage _ _ _ c c_in_kernel).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
c_in_kernel: projection E c = 0
a: Tr (-1) (hfiber (inclusion E) c)
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (ab_pushout_rec_beta_left f (inclusion E) grp_homo_const
              (projection E) (fun x0 : A => (iscomplex_abses E x0)^))))
     (bc'; p))
      strip_truncations.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
c_in_kernel: projection E c = 0
a: hfiber (inclusion E) c
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (ab_pushout_rec_beta_left f (inclusion E) grp_homo_const
              (projection E) (fun x0 : A => (iscomplex_abses E x0)^))))
     (bc'; p))
      destruct a as [a s].
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
c_in_kernel: projection E c = 0
a: A
s: inclusion E a = c
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (ab_pushout_rec_beta_left f (inclusion E) grp_homo_const
              (projection E) (fun x0 : A => (iscomplex_abses E x0)^))))
     (bc'; p))
      (** Now the goal is to show that [bc'] lies in the image of [ab_pushout_inl]. *)
      apply tr.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
c_in_kernel: projection E c = 0
a: A
s: inclusion E a = c
hfiber
  (cxfib
     (phomotopy_homotopy_hset
        (ab_pushout_rec_beta_left f (inclusion E) grp_homo_const
           (projection E) (fun x0 : A => (iscomplex_abses E x0)^))))
  (bc'; p)
      exists (b + - f (- a)); cbn.  (* It simplifies the algebra to write [- f(- a)] instead of [f a]. *)
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
c_in_kernel: projection E c = 0
a: A
s: inclusion E a = c
(class_of
   (fun x y : A' * E =>
    Trunc (-1)
      {x0 : A &
      (- f x0, inclusion E x0) = (- fst x + fst y, - snd x + snd y)})
   (b - f (- a), group_unit);
ab_pushout_rec_beta_left f (inclusion E)
  (grp_homo_compose (grp_trivial_rec B) (grp_trivial_corec A'))
  (projection E) (fun x0 : A => (iscomplex_abses E x0)^) 
  (b - f (- a))) =
(bc'; p)
      apply path_sigma_hprop; cbn.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
c_in_kernel: projection E c = 0
a: A
s: inclusion E a = c
class_of
  (fun x y : A' * E =>
   Trunc (-1)
     {x0 : A & (- f x0, inclusion E x0) = (- fst x + fst y, - snd x + snd y)})
  (b - f (- a), group_unit) =
bc'
      change (ab_pushout_inl (b + - f (- a)) = bc').  (* Just to guide the reader. *)
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
c_in_kernel: projection E c = 0
a: A
s: inclusion E a = c
ab_pushout_inl (b - f (- a)) = bc'
      refine (_ @ q).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
c_in_kernel: projection E c = 0
a: A
s: inclusion E a = c
ab_pushout_inl (b - f (- a)) = grp_quotient_map (b, c)
      symmetry.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
c_in_kernel: projection E c = 0
a: A
s: inclusion E a = c
grp_quotient_map (b, c) = ab_pushout_inl (b - f (- a))
      apply path_ab_pushout; cbn.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
c_in_kernel: projection E c = 0
a: A
s: inclusion E a = c
Trunc (-1)
  {x : A & (- f x, inclusion E x) = (- b + (b - f (- a)), - c + group_unit)}
      refine (tr (-a; _)).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
c_in_kernel: projection E c = 0
a: A
s: inclusion E a = c
(- f (- a), inclusion E (- a)) = (- b + (b - f (- a)), - c + group_unit)
      apply path_prod; cbn.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
c_in_kernel: projection E c = 0
a: A
s: inclusion E a = c
- f (- a) = - b + (b - f (- a))
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
c_in_kernel: projection E c = 0
a: A
s: inclusion E a = c
inclusion E (- a) = - c + group_unit
      *
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
c_in_kernel: projection E c = 0
a: A
s: inclusion E a = c
- f (- a) = - b + (b - f (- a)) apply grp_moveL_Mg.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
c_in_kernel: projection E c = 0
a: A
s: inclusion E a = c
- - b - f (- a) = b - f (- a)
        by rewrite involutive.
      *
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
bc': ab_pushout f (inclusion E)
p: ab_pushout_rec grp_homo_const (projection E)
  (fun x0 : A => (iscomplex_abses E x0)^) bc' =
pt
b: A'
c: E
q: grp_quotient_map (b, c) = bc'
c_in_kernel: projection E c = 0
a: A
s: inclusion E a = c
inclusion E (- a) = - c + group_unit exact ((preserves_inverse a) @ ap _ s @ (right_identity _)^).
Defined.

(** ** The universal property of [abses_pushout_morphism] *)

Definition abses_pushout_morphism `{Univalence} {A A' B : AbGroup}
  (E : AbSES B A) (f : A $-> A')
  : AbSESMorphism E (abses_pushout f E).
H: Univalence
A, A', B: AbGroup
E: AbSES B A
f: A $-> A'
AbSESMorphism E (abses_pushout f E)
Proof.
H: Univalence
A, A', B: AbGroup
E: AbSES B A
f: A $-> A'
AbSESMorphism E (abses_pushout f E)
  snapply (Build_AbSESMorphism f _ grp_homo_id).
H: Univalence
A, A', B: AbGroup
E: AbSES B A
f: A $-> A'
E $-> abses_pushout f E
H: Univalence
A, A', B: AbGroup
E: AbSES B A
f: A $-> A'
inclusion (abses_pushout f E) $o f == ?component2 $o inclusion E
H: Univalence
A, A', B: AbGroup
E: AbSES B A
f: A $-> A'
projection (abses_pushout f E) $o ?component2 == grp_homo_id $o projection E
  -
H: Univalence
A, A', B: AbGroup
E: AbSES B A
f: A $-> A'
E $-> abses_pushout f E exact ab_pushout_inr.
  -
H: Univalence
A, A', B: AbGroup
E: AbSES B A
f: A $-> A'
inclusion (abses_pushout f E) $o f == ab_pushout_inr $o inclusion E exact ab_pushout_commsq.
  -
H: Univalence
A, A', B: AbGroup
E: AbSES B A
f: A $-> A'
projection (abses_pushout f E) $o ab_pushout_inr ==
grp_homo_id $o projection E rapply ab_pushout_rec_beta_right.
Defined.

(** Any map [f : E -> F] of short exact sequences factors (uniquely) through [abses_pushout E f1]. *)

Definition abses_pushout_morphism_rec `{Univalence} {A B X Y : AbGroup}
  {E : AbSES B A} {F : AbSES Y X} (f : AbSESMorphism E F)
  : AbSESMorphism (abses_pushout (component1 f) E) F.
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
AbSESMorphism (abses_pushout (component1 f) E) F
Proof.
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
AbSESMorphism (abses_pushout (component1 f) E) F
  snapply (Build_AbSESMorphism grp_homo_id _ (component3 f)).
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
abses_pushout (component1 f) E $-> F
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
inclusion F $o grp_homo_id ==
?component2 $o inclusion (abses_pushout (component1 f) E)
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
projection F $o ?component2 ==
component3 f $o projection (abses_pushout (component1 f) E)
  -
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
abses_pushout (component1 f) E $-> F rapply ab_pushout_rec.
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
(fun x : A => ?Goal (component1 f x)) ==
(fun x : A => ?Goal0 (inclusion E x))
    apply left_square.
  -
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
inclusion F $o grp_homo_id ==
ab_pushout_rec (inclusion F) (component2 f) (left_square f) $o
inclusion (abses_pushout (component1 f) E) intro x; simpl.
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
x: X
inclusion F x = inclusion F x + component2 f group_unit
    rewrite grp_homo_unit.
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
x: X
inclusion F x = inclusion F x + 0
    exact (right_identity _)^.
  -
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
projection F $o ab_pushout_rec (inclusion F) (component2 f) (left_square f) ==
component3 f $o projection (abses_pushout (component1 f) E) snapply (issurj_isepi_funext grp_quotient_map).
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
IsConnMap (Tr (-1)) grp_quotient_map
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
projection F $o ab_pushout_rec (inclusion F) (component2 f) (left_square f)
o grp_quotient_map ==
component3 f $o projection (abses_pushout (component1 f) E)
o grp_quotient_map
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
IsHSet Y
    1: apply issurj_class_of.
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
projection F $o ab_pushout_rec (inclusion F) (component2 f) (left_square f)
o grp_quotient_map ==
component3 f $o projection (abses_pushout (component1 f) E)
o grp_quotient_map
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
IsHSet Y
    2: exact _.
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
projection F $o ab_pushout_rec (inclusion F) (component2 f) (left_square f)
o grp_quotient_map ==
component3 f $o projection (abses_pushout (component1 f) E)
o grp_quotient_map
    intro x; simpl.
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
x: ab_biprod X E
projection F (inclusion F (fst x) + component2 f (snd x)) =
component3 f (group_unit + projection E (snd x))
    napply grp_homo_op_agree.
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
x: ab_biprod X E
projection F (inclusion F (fst x)) = component3 f group_unit
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
x: ab_biprod X E
projection F (component2 f (snd x)) = component3 f (projection E (snd x))
    +
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
x: ab_biprod X E
projection F (inclusion F (fst x)) = component3 f group_unit refine (_ @ (grp_homo_unit _)^).
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
x: ab_biprod X E
projection F (inclusion F (fst x)) = 0
      apply iscomplex_abses.
    +
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
x: ab_biprod X E
projection F (component2 f (snd x)) = component3 f (projection E (snd x)) apply right_square.
Defined.

(** The original map factors via the induced map. *)
Definition abses_pushout_morphism_rec_beta `{Univalence} (A B X Y : AbGroup)
  (E : AbSES B A) (F : AbSES Y X) (f : AbSESMorphism E F)
  : f = absesmorphism_compose (abses_pushout_morphism_rec f)
                              (abses_pushout_morphism E (component1 f)).
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
f =
absesmorphism_compose (abses_pushout_morphism_rec f)
  (abses_pushout_morphism E (component1 f))
Proof.
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
f =
absesmorphism_compose (abses_pushout_morphism_rec f)
  (abses_pushout_morphism E (component1 f))
  apply (equiv_ap issig_AbSESMorphism^-1 _ _).
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
issig_AbSESMorphism^-1 f =
issig_AbSESMorphism^-1
  (absesmorphism_compose (abses_pushout_morphism_rec f)
     (abses_pushout_morphism E (component1 f)))
  srapply path_sigma_hprop.
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
(issig_AbSESMorphism^-1 f).1 =
(issig_AbSESMorphism^-1
   (absesmorphism_compose (abses_pushout_morphism_rec f)
      (abses_pushout_morphism E (component1 f)))).1
  1: apply path_prod.
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
fst (issig_AbSESMorphism^-1 f).1 =
fst
  (issig_AbSESMorphism^-1
     (absesmorphism_compose (abses_pushout_morphism_rec f)
        (abses_pushout_morphism E (component1 f)))).1
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
snd (issig_AbSESMorphism^-1 f).1 =
snd
  (issig_AbSESMorphism^-1
     (absesmorphism_compose (abses_pushout_morphism_rec f)
        (abses_pushout_morphism E (component1 f)))).1
  1: apply path_prod.
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
fst (fst (issig_AbSESMorphism^-1 f).1) =
fst
  (fst
     (issig_AbSESMorphism^-1
        (absesmorphism_compose (abses_pushout_morphism_rec f)
           (abses_pushout_morphism E (component1 f)))).1)
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
snd (fst (issig_AbSESMorphism^-1 f).1) =
snd
  (fst
     (issig_AbSESMorphism^-1
        (absesmorphism_compose (abses_pushout_morphism_rec f)
           (abses_pushout_morphism E (component1 f)))).1)
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
snd (issig_AbSESMorphism^-1 f).1 =
snd
  (issig_AbSESMorphism^-1
     (absesmorphism_compose (abses_pushout_morphism_rec f)
        (abses_pushout_morphism E (component1 f)))).1
  all: apply equiv_path_grouphomomorphism; intro x; simpl.
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
x: A
component1 f x = component1 f x
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
x: E
component2 f x = inclusion F group_unit + component2 f x
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
x: B
component3 f x = component3 f x
  1,3: reflexivity.
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
x: E
component2 f x = inclusion F group_unit + component2 f x
  rewrite grp_homo_unit.
H: Univalence
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
x: E
component2 f x = 0 + component2 f x
  exact (left_identity _)^.
Defined.

(** Given [E : AbSES B A'] and [F : AbSES B A] and a morphism [f : E -> F], the pushout of [E] along [f_1] is [F] if [f_3] is homotopic to [id_B]. *)
Lemma abses_pushout_component3_id' `{Univalence}
  {A A' B : AbGroup} {E : AbSES B A'} {F : AbSES B A}
  (f : AbSESMorphism E F) (h : component3 f == grp_homo_id)
  : abses_pushout (component1 f) E $== F.
H: Univalence
A, A', B: AbGroup
E: AbSES B A'
F: AbSES B A
f: AbSESMorphism E F
h: component3 f == grp_homo_id
abses_pushout (component1 f) E $== F
Proof.
H: Univalence
A, A', B: AbGroup
E: AbSES B A'
F: AbSES B A
f: AbSESMorphism E F
h: component3 f == grp_homo_id
abses_pushout (component1 f) E $== F
  pose (g := abses_pushout_morphism_rec f).
H: Univalence
A, A', B: AbGroup
E: AbSES B A'
F: AbSES B A
f: AbSESMorphism E F
h: component3 f == grp_homo_id
g:= abses_pushout_morphism_rec f: AbSESMorphism (abses_pushout (component1 f) E) F
abses_pushout (component1 f) E $== F
  napply abses_path_data_to_iso.
H: Univalence
A, A', B: AbGroup
E: AbSES B A'
F: AbSES B A
f: AbSESMorphism E F
h: component3 f == grp_homo_id
g:= abses_pushout_morphism_rec f: AbSESMorphism (abses_pushout (component1 f) E) F
abses_path_data (abses_pushout (component1 f) E) F
  exists (component2 g); split.
H: Univalence
A, A', B: AbGroup
E: AbSES B A'
F: AbSES B A
f: AbSESMorphism E F
h: component3 f == grp_homo_id
g:= abses_pushout_morphism_rec f: AbSESMorphism (abses_pushout (component1 f) E) F
component2 g $o inclusion (abses_pushout (component1 f) E) == inclusion F
H: Univalence
A, A', B: AbGroup
E: AbSES B A'
F: AbSES B A
f: AbSESMorphism E F
h: component3 f == grp_homo_id
g:= abses_pushout_morphism_rec f: AbSESMorphism (abses_pushout (component1 f) E) F
projection (abses_pushout (component1 f) E) == projection F $o component2 g
  +
H: Univalence
A, A', B: AbGroup
E: AbSES B A'
F: AbSES B A
f: AbSESMorphism E F
h: component3 f == grp_homo_id
g:= abses_pushout_morphism_rec f: AbSESMorphism (abses_pushout (component1 f) E) F
component2 g $o inclusion (abses_pushout (component1 f) E) == inclusion F intro x.
H: Univalence
A, A', B: AbGroup
E: AbSES B A'
F: AbSES B A
f: AbSESMorphism E F
h: component3 f == grp_homo_id
g:= abses_pushout_morphism_rec f: AbSESMorphism (abses_pushout (component1 f) E) F
x: A
(component2 g $o inclusion (abses_pushout (component1 f) E)) x =
inclusion F x
    exact (left_square g _)^.
  +
H: Univalence
A, A', B: AbGroup
E: AbSES B A'
F: AbSES B A
f: AbSESMorphism E F
h: component3 f == grp_homo_id
g:= abses_pushout_morphism_rec f: AbSESMorphism (abses_pushout (component1 f) E) F
projection (abses_pushout (component1 f) E) == projection F $o component2 g intro x.
H: Univalence
A, A', B: AbGroup
E: AbSES B A'
F: AbSES B A
f: AbSESMorphism E F
h: component3 f == grp_homo_id
g:= abses_pushout_morphism_rec f: AbSESMorphism (abses_pushout (component1 f) E) F
x: abses_pushout (component1 f) E
projection (abses_pushout (component1 f) E) x =
(projection F $o component2 g) x
    exact ((right_square g _) @ h _)^.
Defined.

(** A version with equality instead of path data. *)
Definition abses_pushout_component3_id `{Univalence}
  {A A' B : AbGroup} {E : AbSES B A'} {F : AbSES B A}
  (f : AbSESMorphism E F) (h : component3 f == grp_homo_id)
  : abses_pushout (component1 f) E = F
  := equiv_path_abses_iso (abses_pushout_component3_id' f h).

(** Given short exact sequences [E] and [F] and homomorphisms [f : A' $-> A] and [g : D' $-> D], there is a morphism [E + F -> fE + gF] induced by the universal properties of the pushouts of [E] and [F]. *)
Definition abses_directsum_pushout_morphism `{Univalence}
  {A A' B C D D' : AbGroup} {E : AbSES B A'} {F : AbSES C D'}
  (f : A' $-> A) (g : D' $-> D)
  : AbSESMorphism (abses_direct_sum E F) (abses_direct_sum (abses_pushout f E) (abses_pushout g F))
  := functor_abses_directsum (abses_pushout_morphism E f) (abses_pushout_morphism F g).

(** For [E, F : AbSES B A'] and [f, g : A' $-> A], we have (f+g)(E+F) = fE + gF, where + denotes the direct sum. *)
Definition abses_directsum_distributive_pushouts `{Univalence}
  {A A' B C C' D : AbGroup} {E : AbSES B A'} {F : AbSES D C'} (f : A' $-> A) (g : C' $-> C)
  : abses_pushout (functor_ab_biprod f g) (abses_direct_sum E F)
    = abses_direct_sum (abses_pushout f E) (abses_pushout g F)
  := abses_pushout_component3_id (abses_directsum_pushout_morphism f g) (fun _ => idpath).

(** Given an [AbSESMorphism] whose third component is the identity, we know that it induces a path from the pushout of the domain along the first map to the codomain. Conversely, given a path from a pushout, we can deduce that the following square commutes: *)
Definition abses_path_pushout_inclusion_commsq `{Univalence} {A A' B : AbGroup}
  (alpha : A $-> A') (E : AbSES B A) (F : AbSES B A')
  (p : abses_pushout alpha E = F)
  : exists phi : middle E $-> F, inclusion F o alpha == phi o inclusion E.
H: Univalence
A, A', B: AbGroup
alpha: A $-> A'
E: AbSES B A
F: AbSES B A'
p: abses_pushout alpha E = F
{phi : E $-> F & inclusion F o alpha == phi o inclusion E}
Proof.
H: Univalence
A, A', B: AbGroup
alpha: A $-> A'
E: AbSES B A
F: AbSES B A'
p: abses_pushout alpha E = F
{phi : E $-> F & inclusion F o alpha == phi o inclusion E}
  induction p.
H: Univalence
A, A', B: AbGroup
alpha: A $-> A'
E: AbSES B A
{phi : E $-> abses_pushout alpha E &
(fun x : A => inclusion (abses_pushout alpha E) (alpha x)) ==
(fun x : A => phi (inclusion E x))}
  exists ab_pushout_inr; intro x.
H: Univalence
A, A', B: AbGroup
alpha: A $-> A'
E: AbSES B A
x: A
inclusion (abses_pushout alpha E) (alpha x) = ab_pushout_inr (inclusion E x)
  napply ab_pushout_commsq.
Defined.

(** ** Functoriality of [abses_pushout f : AbSES B A -> AbSES B A'] *)

(** In this file we will prove various "levels" of functoriality of pushing out. Here we show that the induced map between [AbSES B A] respect the groupoid structure of [is1gpd_abses] from AbSES.Core. *)

Instance is0functor_abses_pushout `{Univalence} {A A' B : AbGroup} (f : A $-> A')
  : Is0Functor (abses_pushout (B:=B) f).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
Is0Functor (abses_pushout f)
Proof.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
Is0Functor (abses_pushout f)
  srapply Build_Is0Functor;
    intros E F p.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
p: E $-> F
abses_pushout f E $-> abses_pushout f F
  srapply abses_path_data_to_iso.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
p: E $-> F
abses_path_data (abses_pushout f E) (abses_pushout f F)
  srefine (functor_ab_pushout f f (inclusion _) (inclusion _) grp_homo_id grp_homo_id p.1 _ _; (_, _)).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
p: E $-> F
grp_homo_id $o f == f $o grp_homo_id
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
p: E $-> F
inclusion F $o grp_homo_id == p.1 $o inclusion E
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
p: E $-> F
functor_ab_pushout f f (inclusion E) (inclusion F) grp_homo_id grp_homo_id
  p.1 ?h ?k $o
inclusion (abses_pushout f E) == inclusion (abses_pushout f F)
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
p: E $-> F
projection (abses_pushout f E) ==
projection (abses_pushout f F) $o
functor_ab_pushout f f (inclusion E) (inclusion F) grp_homo_id grp_homo_id
  p.1 ?h ?k
  -
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
p: E $-> F
grp_homo_id $o f == f $o grp_homo_id reflexivity.
  -
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
p: E $-> F
inclusion F $o grp_homo_id == p.1 $o inclusion E symmetry; exact (fst p.2).
  -
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
p: E $-> F
functor_ab_pushout f f (inclusion E) (inclusion F) grp_homo_id grp_homo_id
  p.1 (fun x0 : A => 1)
  ((fun (x y : A -> F) (p0 : x == y) (x0 : A) => (p0 x0)^)
     (p.1 $o inclusion E) (inclusion F $o grp_homo_id) 
     (fst p.2)) $o
inclusion (abses_pushout f E) == inclusion (abses_pushout f F) napply ab_pushout_rec_beta_left.
  -
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
p: E $-> F
projection (abses_pushout f E) ==
projection (abses_pushout f F) $o
functor_ab_pushout f f (inclusion E) (inclusion F) grp_homo_id grp_homo_id
  p.1 (fun x0 : A => 1)
  ((fun (x y : A -> F) (p0 : x == y) (x0 : A) => (p0 x0)^)
     (p.1 $o inclusion E) (inclusion F $o grp_homo_id) 
     (fst p.2)) srapply Quotient_ind_hprop.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
p: E $-> F
forall a : ab_biprod A' E,
(fun
   x : ab_biprod A' E /
       in_cosetL
         {|
           normalsubgroup_subgroup := ab_pushout_subgroup f (inclusion E);
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup (ab_biprod A' E)
               (ab_pushout_subgroup f (inclusion E))
         |} =>
 projection (abses_pushout f E) x =
 (projection (abses_pushout f F) $o
  functor_ab_pushout f f (inclusion E) (inclusion F) grp_homo_id grp_homo_id
    p.1 (fun x0 : A => 1)
    ((fun (x0 y : A -> F) (p0 : x0 == y) (x1 : A) => (p0 x1)^)
       (p.1 $o inclusion E) (inclusion F $o grp_homo_id) 
       (fst p.2)))
   x)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := ab_pushout_subgroup f (inclusion E);
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup (ab_biprod A' E)
              (ab_pushout_subgroup f (inclusion E))
        |})
     a)
    intro x; simpl.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
p: E $-> F
x: ab_biprod A' E
group_unit + projection E (snd x) =
group_unit + projection F (group_unit + p.1 (snd x))
    apply grp_cancelL.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
p: E $-> F
x: ab_biprod A' E
projection E (snd x) = projection F (group_unit + p.1 (snd x))
    refine (snd p.2 (snd x) @ ap (projection F) _).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
p: E $-> F
x: ab_biprod A' E
p.1 (snd x) = group_unit + p.1 (snd x)
    exact (left_identity _)^.
Defined.

Instance is1functor_abses_pushout `{Univalence}
  {A A' B : AbGroup} (f : A $-> A')
  : Is1Functor (abses_pushout (B:=B) f).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
Is1Functor (abses_pushout f)
Proof.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
Is1Functor (abses_pushout f)
  srapply Build_Is1Functor.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
forall (a b : AbSES B A) (f0 g : a $-> b),
f0 $== g -> fmap (abses_pushout f) f0 $== fmap (abses_pushout f) g
H: Univalence
A, A', B: AbGroup
f: A $-> A'
forall a : AbSES B A,
fmap (abses_pushout f) (Id a) $== Id (abses_pushout f a)
H: Univalence
A, A', B: AbGroup
f: A $-> A'
forall (a b c : AbSES B A) (f0 : a $-> b) (g : b $-> c),
fmap (abses_pushout f) (g $o f0) $==
fmap (abses_pushout f) g $o fmap (abses_pushout f) f0
  -
H: Univalence
A, A', B: AbGroup
f: A $-> A'
forall (a b : AbSES B A) (f0 g : a $-> b),
f0 $== g -> fmap (abses_pushout f) f0 $== fmap (abses_pushout f) g intros E F g0 g1 h.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
g0, g1: E $-> F
h: g0 $== g1
fmap (abses_pushout f) g0 $== fmap (abses_pushout f) g1
    rapply Quotient_ind_hprop; intros [a' e]; simpl.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
g0, g1: E $-> F
h: g0 $== g1
a': A'
e: E
class_of
  (fun x y : A' * F => Tr (-1) {x0 : A & (- f x0, inclusion F x0) = - x + y})
  (a', group_unit) +
class_of
  (fun x y : A' * F => Tr (-1) {x0 : A & (- f x0, inclusion F x0) = - x + y})
  (group_unit, g0.1 e) =
class_of
  (fun x y : A' * F => Tr (-1) {x0 : A & (- f x0, inclusion F x0) = - x + y})
  (a', group_unit) +
class_of
  (fun x y : A' * F => Tr (-1) {x0 : A & (- f x0, inclusion F x0) = - x + y})
  (group_unit, g1.1 e)
    by rewrite (h e).
  -
H: Univalence
A, A', B: AbGroup
f: A $-> A'
forall a : AbSES B A,
fmap (abses_pushout f) (Id a) $== Id (abses_pushout f a) intro E.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
fmap (abses_pushout f) (Id E) $== Id (abses_pushout f E)
    rapply Quotient_ind_hprop; intros [a' e]; simpl.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
a': A'
e: E
class_of
  (fun x y : A' * E => Tr (-1) {x0 : A & (- f x0, inclusion E x0) = - x + y})
  (a', group_unit) +
class_of
  (fun x y : A' * E => Tr (-1) {x0 : A & (- f x0, inclusion E x0) = - x + y})
  (group_unit, e) =
class_of
  (fun x y : A' * E => Tr (-1) {x0 : A & (- f x0, inclusion E x0) = - x + y})
  (a', e)
    refine (ap (class_of _) (path_prod' _ _)).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
a': A'
e: E
a' + group_unit = a'
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
a': A'
e: E
group_unit + e = e
    +
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
a': A'
e: E
a' + group_unit = a' exact (grp_unit_r _).
    +
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
a': A'
e: E
group_unit + e = e exact (grp_unit_l _).
  -
H: Univalence
A, A', B: AbGroup
f: A $-> A'
forall (a b c : AbSES B A) (f0 : a $-> b) (g : b $-> c),
fmap (abses_pushout f) (g $o f0) $==
fmap (abses_pushout f) g $o fmap (abses_pushout f) f0 intros E F G g0 g1.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F, G: AbSES B A
g0: E $-> F
g1: F $-> G
fmap (abses_pushout f) (g1 $o g0) $==
fmap (abses_pushout f) g1 $o fmap (abses_pushout f) g0
    rapply Quotient_ind_hprop; intros [a' e]; simpl.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F, G: AbSES B A
g0: E $-> F
g1: F $-> G
a': A'
e: E
class_of
  (fun x y : A' * G => Tr (-1) {x0 : A & (- f x0, inclusion G x0) = - x + y})
  (a', group_unit) +
class_of
  (fun x y : A' * G => Tr (-1) {x0 : A & (- f x0, inclusion G x0) = - x + y})
  (group_unit, g1.1 (g0.1 e)) =
class_of
  (fun x y : A' * G => Tr (-1) {x0 : A & (- f x0, inclusion G x0) = - x + y})
  (a' + group_unit, group_unit) +
class_of
  (fun x y : A' * G => Tr (-1) {x0 : A & (- f x0, inclusion G x0) = - x + y})
  (group_unit, g1.1 (group_unit + g0.1 e))
    refine (ap (class_of _) (path_prod' _ _)).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F, G: AbSES B A
g0: E $-> F
g1: F $-> G
a': A'
e: E
a' + group_unit = a' + group_unit + group_unit
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F, G: AbSES B A
g0: E $-> F
g1: F $-> G
a': A'
e: E
group_unit + g1.1 (g0.1 e) = group_unit + g1.1 (group_unit + g0.1 e)
    +
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F, G: AbSES B A
g0: E $-> F
g1: F $-> G
a': A'
e: E
a' + group_unit = a' + group_unit + group_unit exact (grp_unit_r _)^.
    +
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F, G: AbSES B A
g0: E $-> F
g1: F $-> G
a': A'
e: E
group_unit + g1.1 (g0.1 e) = group_unit + g1.1 (group_unit + g0.1 e) exact (ap (fun x => _ + g1.1 x) (grp_unit_l _)^).
Defined.

Definition abses_pushout_path_data_1 `{Univalence} {A A' B : AbGroup} (f : A $-> A') {E : AbSES B A} 
  : fmap (abses_pushout f) (Id E) = Id (abses_pushout f E).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
fmap (abses_pushout f) (Id E) = Id (abses_pushout f E)
Proof.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
fmap (abses_pushout f) (Id E) = Id (abses_pushout f E)
  srapply path_sigma_hprop.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
(fmap (abses_pushout f) (Id E)).1 = (Id (abses_pushout f E)).1
  apply equiv_path_groupisomorphism.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
(fmap (abses_pushout f) (Id E)).1 == (Id (abses_pushout f E)).1
  srapply Quotient_ind_hprop.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
forall a : ab_biprod A' E,
(fun
   x : ab_biprod A' E /
       in_cosetL
         {|
           normalsubgroup_subgroup := ab_pushout_subgroup f (inclusion E);
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup (ab_biprod A' E)
               (ab_pushout_subgroup f (inclusion E))
         |} =>
 (fmap (abses_pushout f) (Id E)).1 x = (Id (abses_pushout f E)).1 x)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := ab_pushout_subgroup f (inclusion E);
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup (ab_biprod A' E)
              (ab_pushout_subgroup f (inclusion E))
        |})
     a)
  intros [a' e]; simpl. (* This is true even on the representatives. *)
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
a': A'
e: E
class_of
  (fun x y : A' * E => Tr (-1) {x0 : A & (- f x0, inclusion E x0) = - x + y})
  (a', group_unit) +
class_of
  (fun x y : A' * E => Tr (-1) {x0 : A & (- f x0, inclusion E x0) = - x + y})
  (group_unit, e) =
class_of
  (fun x y : A' * E => Tr (-1) {x0 : A & (- f x0, inclusion E x0) = - x + y})
  (a', e)
  apply qglue.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
a': A'
e: E
in_cosetL (ab_pushout_subgroup f (inclusion E))
  ((a', group_unit) + (group_unit, e)) (a', e)
  refine (tr (0; _)).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
a': A'
e: E
ab_biprod_corec (ab_homo_negation $o f) (inclusion E) 0 =
- ((a', group_unit) + (group_unit, e)) + (a', e)
  apply path_prod'; cbn.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
a': A'
e: E
- f 0 = - (a' + group_unit) + a'
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
a': A'
e: E
inclusion E 0 = - (group_unit + e) + e
  -
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
a': A'
e: E
- f 0 = - (a' + group_unit) + a' refine (ap _ (grp_homo_unit _) @ _).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
a': A'
e: E
- 0 = - (a' + group_unit) + a'
    refine (grp_inv_unit @ _).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
a': A'
e: E
0 = - (a' + group_unit) + a'
    apply grp_moveL_Vg.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
a': A'
e: E
a' + group_unit + 0 = a'
    exact (right_identity _ @ right_identity _).
  -
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
a': A'
e: E
inclusion E 0 = - (group_unit + e) + e refine (grp_homo_unit _ @ _).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
a': A'
e: E
0 = - (group_unit + e) + e
    apply grp_moveL_Vg.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
a': A'
e: E
group_unit + e + 0 = e
    exact (right_identity _ @ left_identity _).
Defined.

Definition ap_abses_pushout `{Univalence} {A A' B : AbGroup} (f : A $-> A')
  {E F : AbSES B A} (p : E = F)
  : ap (abses_pushout f) p
    = equiv_path_abses_iso (fmap (abses_pushout f) (equiv_path_abses_iso^-1 p)).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
p: E = F
ap (abses_pushout f) p =
equiv_path_abses_iso (fmap (abses_pushout f) (equiv_path_abses_iso^-1 p))
Proof.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
p: E = F
ap (abses_pushout f) p =
equiv_path_abses_iso (fmap (abses_pushout f) (equiv_path_abses_iso^-1 p))
  induction p.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
ap (abses_pushout f) 1 =
equiv_path_abses_iso (fmap (abses_pushout f) (equiv_path_abses_iso^-1 1))
  refine (_ @ ap _ _).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
ap (abses_pushout f) 1 = equiv_path_abses_iso ?Goal0
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
?Goal0 = fmap (abses_pushout f) (equiv_path_abses_iso^-1 1)
  2: exact ((abses_pushout_path_data_1 f)^ @ ap _ equiv_path_absesV_1^).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
ap (abses_pushout f) 1 = equiv_path_abses_iso (Id (abses_pushout f E))
  exact equiv_path_abses_1^.
Defined.

Definition ap_abses_pushout_data `{Univalence} {A A' B : AbGroup} (f : A $-> A')
  {E F : AbSES B A} (p : E $== F)
  : ap (abses_pushout f) (equiv_path_abses_iso p)
    = equiv_path_abses_iso (fmap (abses_pushout f) p).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
p: E $== F
ap (abses_pushout f) (equiv_path_abses_iso p) =
equiv_path_abses_iso (fmap (abses_pushout f) p)
Proof.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
p: E $== F
ap (abses_pushout f) (equiv_path_abses_iso p) =
equiv_path_abses_iso (fmap (abses_pushout f) p)
  refine (ap_abses_pushout _ _ @ _).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
p: E $== F
equiv_path_abses_iso
  (fmap (abses_pushout f) (equiv_path_abses_iso^-1 (equiv_path_abses_iso p))) =
equiv_path_abses_iso (fmap (abses_pushout f) p)
  apply (ap (equiv_path_abses_iso o _)).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
p: E $== F
equiv_path_abses_iso^-1 (equiv_path_abses_iso p) = p
  apply eissect.
Defined.

Definition abses_pushout_point' `{Univalence} {A A' B : AbGroup} (f : A $-> A')
  : abses_pushout f (point (AbSES B A)) $== pt.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
abses_pushout f pt $== pt
Proof.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
abses_pushout f pt $== pt
  srapply abses_path_data_to_iso;
    srefine (_; (_,_)).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
abses_pushout f pt $-> pt
H: Univalence
A, A', B: AbGroup
f: A $-> A'
?proj1 $o inclusion (abses_pushout f pt) == inclusion pt
H: Univalence
A, A', B: AbGroup
f: A $-> A'
projection (abses_pushout f pt) == projection pt $o ?proj1
  -
H: Univalence
A, A', B: AbGroup
f: A $-> A'
abses_pushout f pt $-> pt snrefine (ab_pushout_rec ab_biprod_inl _ _).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
pt $-> ab_biprod A' B
H: Univalence
A, A', B: AbGroup
f: A $-> A'
ab_biprod_inl o f == ?c o inclusion pt
    +
H: Univalence
A, A', B: AbGroup
f: A $-> A'
pt $-> ab_biprod A' B exact (functor_ab_biprod f grp_homo_id).
    +
H: Univalence
A, A', B: AbGroup
f: A $-> A'
ab_biprod_inl o f == functor_ab_biprod f grp_homo_id o inclusion pt reflexivity.
  -
H: Univalence
A, A', B: AbGroup
f: A $-> A'
ab_pushout_rec ab_biprod_inl (functor_ab_biprod f grp_homo_id)
  (fun x0 : A => 1) $o
inclusion (abses_pushout f pt) == inclusion pt intro a'.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
a': A'
(ab_pushout_rec ab_biprod_inl (functor_ab_biprod f grp_homo_id)
   (fun x0 : A => 1) $o
 inclusion (abses_pushout f pt)) a' =
inclusion pt a' 
    apply path_prod.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
a': A'
fst
  ((ab_pushout_rec ab_biprod_inl (functor_ab_biprod f grp_homo_id)
      (fun x0 : A => 1) $o
    inclusion (abses_pushout f pt)) a') =
fst (inclusion pt a')
H: Univalence
A, A', B: AbGroup
f: A $-> A'
a': A'
snd
  ((ab_pushout_rec ab_biprod_inl (functor_ab_biprod f grp_homo_id)
      (fun x0 : A => 1) $o
    inclusion (abses_pushout f pt)) a') =
snd (inclusion pt a')
    +
H: Univalence
A, A', B: AbGroup
f: A $-> A'
a': A'
fst
  ((ab_pushout_rec ab_biprod_inl (functor_ab_biprod f grp_homo_id)
      (fun x0 : A => 1) $o
    inclusion (abses_pushout f pt)) a') =
fst (inclusion pt a') simpl.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
a': A'
a' + f 0 = a'
      exact (ap _ (grp_homo_unit f) @ right_identity _).
    +
H: Univalence
A, A', B: AbGroup
f: A $-> A'
a': A'
snd
  ((ab_pushout_rec ab_biprod_inl (functor_ab_biprod f grp_homo_id)
      (fun x0 : A => 1) $o
    inclusion (abses_pushout f pt)) a') =
snd (inclusion pt a') simpl.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
a': A'
group_unit + 0 = group_unit
      exact (right_identity _).
  -
H: Univalence
A, A', B: AbGroup
f: A $-> A'
projection (abses_pushout f pt) ==
projection pt $o
ab_pushout_rec ab_biprod_inl (functor_ab_biprod f grp_homo_id)
  (fun x0 : A => 1) srapply Quotient_ind_hprop.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
forall a : ab_biprod A' pt,
(fun
   x : ab_biprod A' pt /
       in_cosetL
         {|
           normalsubgroup_subgroup := ab_pushout_subgroup f (inclusion pt);
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup (ab_biprod A' pt)
               (ab_pushout_subgroup f (inclusion pt))
         |} =>
 projection (abses_pushout f pt) x =
 (projection pt $o
  ab_pushout_rec ab_biprod_inl (functor_ab_biprod f grp_homo_id)
    (fun x0 : A => 1))
   x)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := ab_pushout_subgroup f (inclusion pt);
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup (ab_biprod A' pt)
              (ab_pushout_subgroup f (inclusion pt))
        |})
     a)
    reflexivity.
Defined.

Definition abses_pushout_point `{Univalence} {A A' B : AbGroup} (f : A $-> A')
  : abses_pushout f (point (AbSES B A)) = pt
  := equiv_path_abses_iso (abses_pushout_point' f).

Definition abses_pushout' `{Univalence} {A A' B : AbGroup} (f : A $-> A')
  : AbSES B A -->* AbSES B A'
  := Build_BasepointPreservingFunctor (abses_pushout f) (abses_pushout_point' f).

Definition abses_pushout_pmap `{Univalence} {A A' B : AbGroup} (f : A $-> A')
  : AbSES B A ->* AbSES B A'
  := to_pointed (abses_pushout' f).

(** The following general lemma lets us show that [abses_pushout f E] is trivial in cases of interest. It says that if you have a map [phi : E -> A'], then if you push out along the restriction [phi $o inclusion E], the result is trivial. Specifically, we get a morphism witnessing this fact.  *)
Definition abses_pushout_trivial_morphism {B A A' : AbGroup}
  (E : AbSES B A) (f : A $-> A') (phi : middle E $-> A')
  (k : f == phi $o inclusion E)
  : AbSESMorphism E (pt : AbSES B A').
B, A, A': AbGroup
E: AbSES B A
f: A $-> A'
phi: E $-> A'
k: f == phi $o inclusion E
AbSESMorphism E (pt : AbSES B A')
Proof.
B, A, A': AbGroup
E: AbSES B A
f: A $-> A'
phi: E $-> A'
k: f == phi $o inclusion E
AbSESMorphism E (pt : AbSES B A')
  srapply (Build_AbSESMorphism f _ grp_homo_id).
B, A, A': AbGroup
E: AbSES B A
f: A $-> A'
phi: E $-> A'
k: f == phi $o inclusion E
E $-> pt
B, A, A': AbGroup
E: AbSES B A
f: A $-> A'
phi: E $-> A'
k: f == phi $o inclusion E
inclusion pt $o f == ?component2 $o inclusion E
B, A, A': AbGroup
E: AbSES B A
f: A $-> A'
phi: E $-> A'
k: f == phi $o inclusion E
projection pt $o ?component2 == grp_homo_id $o projection E
  1: exact (ab_biprod_corec phi (projection E)).
B, A, A': AbGroup
E: AbSES B A
f: A $-> A'
phi: E $-> A'
k: f == phi $o inclusion E
inclusion pt $o f == ab_biprod_corec phi (projection E) $o inclusion E
B, A, A': AbGroup
E: AbSES B A
f: A $-> A'
phi: E $-> A'
k: f == phi $o inclusion E
projection pt $o ab_biprod_corec phi (projection E) ==
grp_homo_id $o projection E
  {
B, A, A': AbGroup
E: AbSES B A
f: A $-> A'
phi: E $-> A'
k: f == phi $o inclusion E
inclusion pt $o f == ab_biprod_corec phi (projection E) $o inclusion E intro a; cbn.
B, A, A': AbGroup
E: AbSES B A
f: A $-> A'
phi: E $-> A'
k: f == phi $o inclusion E
a: A
(f a, group_unit) = (phi (inclusion E a), projection E (inclusion E a))
    refine (path_prod' (k a) _^).
B, A, A': AbGroup
E: AbSES B A
f: A $-> A'
phi: E $-> A'
k: f == phi $o inclusion E
a: A
projection E (inclusion E a) = group_unit
    apply isexact_inclusion_projection. }
B, A, A': AbGroup
E: AbSES B A
f: A $-> A'
phi: E $-> A'
k: f == phi $o inclusion E
projection pt $o ab_biprod_corec phi (projection E) ==
grp_homo_id $o projection E
  reflexivity.
Defined.

(** The pushout of a short exact sequence along its inclusion map is trivial. *)
Definition abses_pushout_inclusion_morphism {B A : AbGroup} (E : AbSES B A)
  : AbSESMorphism E (pt : AbSES B E)
  := abses_pushout_trivial_morphism E (inclusion E) grp_homo_id (fun _ => idpath).

Definition abses_pushout_inclusion `{Univalence} {B A : AbGroup} (E : AbSES B A)
  : abses_pushout (inclusion E) E = pt
  := abses_pushout_component3_id
       (abses_pushout_inclusion_morphism E) (fun _ => idpath).

(** Pushing out along [grp_homo_const] is trivial. *)
Definition abses_pushout_const_morphism {B A A' : AbGroup} (E : AbSES B A)
  : AbSESMorphism E (pt : AbSES B A')
  := abses_pushout_trivial_morphism E
       grp_homo_const grp_homo_const (fun _ => idpath).

Definition abses_pushout_const `{Univalence} {B A A' : AbGroup} (E : AbSES B A)
  : abses_pushout grp_homo_const E = pt :> AbSES B A'
  := abses_pushout_component3_id
       (abses_pushout_const_morphism E) (fun _ => idpath).

(** Pushing out a fixed extension, with the map variable. This is the connecting map in the contravariant six-term exact sequence (see SixTerm.v). *)
Definition abses_pushout_abses `{Univalence} {B A G : AbGroup} (E : AbSES B A)
  : ab_hom A G ->* AbSES B G.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
ab_hom A G ->* AbSES B G
Proof.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
ab_hom A G ->* AbSES B G
  srapply Build_pMap.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
ab_hom A G -> AbSES B G
H: Univalence
B, A, G: AbGroup
E: AbSES B A
?f pt = pt
  1: exact (fun g => abses_pushout g E).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
(fun g : ab_hom A G => abses_pushout g E) pt = pt
  apply abses_pushout_const.
Defined.

(** ** Functoriality of pushing out *)

(** For every [E : AbSES B A], the pushout of [E] along [id_A] is [E]. *)
Definition abses_pushout_id `{Univalence} {A B : AbGroup}
  : abses_pushout (B:=B) (@grp_homo_id A) == idmap
  := fun E => abses_pushout_component3_id (abses_morphism_id E) (fun _ => idpath).

Definition abses_pushout_pmap_id `{Univalence} {A B : AbGroup}
  : abses_pushout_pmap (B:=B) (@grp_homo_id A) ==* @pmap_idmap (AbSES B A).
H: Univalence
A, B: AbGroup
abses_pushout_pmap grp_homo_id ==* pmap_idmap
Proof.
H: Univalence
A, B: AbGroup
abses_pushout_pmap grp_homo_id ==* pmap_idmap
  srapply Build_pHomotopy.
H: Univalence
A, B: AbGroup
abses_pushout_pmap grp_homo_id == pmap_idmap
H: Univalence
A, B: AbGroup
?p pt = dpoint_eq (abses_pushout_pmap grp_homo_id) @ (dpoint_eq pmap_idmap)^
  1: exact abses_pushout_id.
H: Univalence
A, B: AbGroup
abses_pushout_id pt =
dpoint_eq (abses_pushout_pmap grp_homo_id) @ (dpoint_eq pmap_idmap)^
  refine (_ @ (concat_p1 _)^).
H: Univalence
A, B: AbGroup
abses_pushout_id pt = dpoint_eq (abses_pushout_pmap grp_homo_id)
  (* For some reason Coq spends time finding [x] below, so we specify it. *)
  napply (ap equiv_path_abses_iso
             (x:=abses_pushout_component3_id' (abses_morphism_id pt) _)).
H: Univalence
A, B: AbGroup
abses_pushout_component3_id' (abses_morphism_id pt) (fun x : B => 1) =
bp_pointed (abses_pushout' grp_homo_id)
  apply path_sigma_hprop.
H: Univalence
A, B: AbGroup
(abses_pushout_component3_id' (abses_morphism_id pt) (fun x : B => 1)).1 =
(bp_pointed (abses_pushout' grp_homo_id)).1
  apply equiv_path_groupisomorphism.
H: Univalence
A, B: AbGroup
(abses_pushout_component3_id' (abses_morphism_id pt) (fun x : B => 1)).1 ==
(bp_pointed (abses_pushout' grp_homo_id)).1
  by rapply Quotient_ind_hprop.
Defined.

(** Pushing out along homotopic maps induces homotopic pushout functors. This statement has a short proof by path induction on the homotopy [h], but we prefer to construct a path using [abses_path_data_iso] with better computational properties. *)
Lemma abses_pushout_homotopic' `{Univalence} {A A' B : AbGroup}
  (f f' : A $-> A') (h : f == f')
  : abses_pushout (B:=B) f $=> abses_pushout f'.
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
abses_pushout f $=> abses_pushout f'
Proof.
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
abses_pushout f $=> abses_pushout f'
  intro E; cbn.
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
E: AbSES B A
abses_path_data_iso (abses_pushout f E) (abses_pushout f' E)
  apply abses_path_data_to_iso.
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
E: AbSES B A
abses_path_data (abses_pushout f E) (abses_pushout f' E)
  snrefine (_; (_, _)).
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
E: AbSES B A
abses_pushout f E $-> abses_pushout f' E
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
E: AbSES B A
?proj1 $o inclusion (abses_pushout f E) == inclusion (abses_pushout f' E)
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
E: AbSES B A
projection (abses_pushout f E) == projection (abses_pushout f' E) $o ?proj1
  -
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
E: AbSES B A
abses_pushout f E $-> abses_pushout f' E srapply (ab_pushout_rec (inclusion _)).
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
E: AbSES B A
E $-> abses_pushout f' E
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
E: AbSES B A
inclusion (abses_pushout f' E) o f == ?c o inclusion E
    1: exact ab_pushout_inr.
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
E: AbSES B A
inclusion (abses_pushout f' E) o f == ab_pushout_inr o inclusion E
    intro x.
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
E: AbSES B A
x: A
inclusion (abses_pushout f' E) (f x) = ab_pushout_inr (inclusion E x)
    refine (ap _ (h x) @ _).
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
E: AbSES B A
x: A
inclusion (abses_pushout f' E) (f' x) = ab_pushout_inr (inclusion E x)
    exact (ab_pushout_commsq x).
  -
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
E: AbSES B A
ab_pushout_rec (inclusion (abses_pushout f' E)) ab_pushout_inr
  ((fun x : A =>
    ap (inclusion (abses_pushout f' E)) (h x) @ ab_pushout_commsq x)
   :
   inclusion (abses_pushout f' E) o f == ab_pushout_inr o inclusion E) $o
inclusion (abses_pushout f E) == inclusion (abses_pushout f' E) apply ab_pushout_rec_beta_left.
  -
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
E: AbSES B A
projection (abses_pushout f E) ==
projection (abses_pushout f' E) $o
ab_pushout_rec (inclusion (abses_pushout f' E)) ab_pushout_inr
  ((fun x : A =>
    ap (inclusion (abses_pushout f' E)) (h x) @ ab_pushout_commsq x)
   :
   inclusion (abses_pushout f' E) o f == ab_pushout_inr o inclusion E) rapply Quotient_ind_hprop; intros [a' e]; simpl.
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
E: AbSES B A
a': A'
e: E
group_unit + projection E e = group_unit + projection E (group_unit + e)
    exact (ap (fun x => _ + projection E x) (grp_unit_l _)^).
Defined.

Definition abses_pushout_homotopic `{Univalence} {A A' B : AbGroup}
  (f f' : A $-> A') (h : f == f')
  : abses_pushout (B:=B) f == abses_pushout f'
  := equiv_path_data_homotopy _ _ (abses_pushout_homotopic' _ _ h).

Definition abses_pushout_phomotopic' `{Univalence} {A A' B : AbGroup}
  (f f' : A $-> A') (h : f == f')
  : abses_pushout' (B:=B) f $=>* abses_pushout' f'.
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
abses_pushout' f $=>* abses_pushout' f'
Proof.
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
abses_pushout' f $=>* abses_pushout' f'
  exists (abses_pushout_homotopic' _ _ h).
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
abses_pushout_homotopic' f f' h pt $==
bp_pointed (abses_pushout' f) $@ (bp_pointed (abses_pushout' f'))^$
  apply gpd_moveL_Vh.
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
bp_pointed (abses_pushout' f') $o abses_pushout_homotopic' f f' h pt $==
bp_pointed (abses_pushout' f)
  rapply Quotient_ind_hprop; intros [a' [a b]]; simpl.
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
a': A'
a: A
b: B
(a' + group_unit, group_unit) + (f' (0 + a), 0 + b) =
(a', group_unit) + (f a, b)
  apply path_prod'.
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
a': A'
a: A
b: B
a' + group_unit + f' (0 + a) = a' + f a
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
a': A'
a: A
b: B
group_unit + (0 + b) = group_unit + b
  -
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
a': A'
a: A
b: B
a' + group_unit + f' (0 + a) = a' + f a by rewrite grp_unit_l, grp_unit_r, (h a).
  -
H: Univalence
A, A', B: AbGroup
f, f': A $-> A'
h: f == f'
a': A'
a: A
b: B
group_unit + (0 + b) = group_unit + b apply grp_unit_l.
Defined.

Definition abses_pushout_phomotopic `{Univalence} {A A' B : AbGroup}
  (f f' : A $-> A') (h : f == f')
  : abses_pushout_pmap (B:=B) f ==* abses_pushout_pmap f'
  := equiv_ptransformation_phomotopy (abses_pushout_phomotopic' f f' h).

Definition abses_pushout_compose' `{Univalence} {A0 A1 A2 B : AbGroup}
  (f : A0 $-> A1) (g : A1 $-> A2)
  : abses_pushout (g $o f) $=> abses_pushout (B:=B) g o abses_pushout f.
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
abses_pushout (g $o f) $=> abses_pushout g o abses_pushout f
Proof.
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
abses_pushout (g $o f) $=> abses_pushout g o abses_pushout f
  intro E.
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
E: AbSES B A0
abses_pushout (g $o f) E $-> abses_pushout g (abses_pushout f E)
  srapply abses_path_data_to_iso;
    srefine (_; (_,_)).
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
E: AbSES B A0
abses_pushout (g $o f) E $-> abses_pushout g (abses_pushout f E)
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
E: AbSES B A0
?proj1 $o inclusion (abses_pushout (g $o f) E) ==
inclusion (abses_pushout g (abses_pushout f E))
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
E: AbSES B A0
projection (abses_pushout (g $o f) E) ==
projection (abses_pushout g (abses_pushout f E)) $o ?proj1
  -
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
E: AbSES B A0
abses_pushout (g $o f) E $-> abses_pushout g (abses_pushout f E) snapply ab_pushout_rec.
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
E: AbSES B A0
A2 $-> abses_pushout g (abses_pushout f E)
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
E: AbSES B A0
E $-> abses_pushout g (abses_pushout f E)
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
E: AbSES B A0
?b o (g $o f) == ?c o inclusion E
    +
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
E: AbSES B A0
A2 $-> abses_pushout g (abses_pushout f E) apply inclusion.
    +
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
E: AbSES B A0
E $-> abses_pushout g (abses_pushout f E) exact (component2 (abses_pushout_morphism _ g)
                        $o component2 (abses_pushout_morphism _ f)).
    +
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
E: AbSES B A0
inclusion (abses_pushout g (abses_pushout f E)) o (g $o f) ==
component2 (abses_pushout_morphism (abses_pushout f E) g) $o
component2 (abses_pushout_morphism E f) o inclusion E intro a0.
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
E: AbSES B A0
a0: A0
inclusion (abses_pushout g (abses_pushout f E)) ((g $o f) a0) =
(component2 (abses_pushout_morphism (abses_pushout f E) g) $o
 component2 (abses_pushout_morphism E f)) (inclusion E a0)
      refine (left_square (abses_pushout_morphism _ g) _ @ _).
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
E: AbSES B A0
a0: A0
(component2 (abses_pushout_morphism (abses_pushout f E) g) $o
 inclusion (abses_pushout f E)) (f a0) =
(component2 (abses_pushout_morphism (abses_pushout f E) g) $o
 component2 (abses_pushout_morphism E f)) (inclusion E a0)
      exact (ap (component2 (abses_pushout_morphism (abses_pushout f E) g))
                (left_square (abses_pushout_morphism _ f) a0)).
  -
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
E: AbSES B A0
ab_pushout_rec (inclusion (abses_pushout g (abses_pushout f E)))
  (component2 (abses_pushout_morphism (abses_pushout f E) g) $o
   component2 (abses_pushout_morphism E f))
  ((fun a0 : A0 =>
    left_square (abses_pushout_morphism (abses_pushout f E) g) (f a0) @
    ap (component2 (abses_pushout_morphism (abses_pushout f E) g))
      (left_square (abses_pushout_morphism E f) a0))
   :
   inclusion (abses_pushout g (abses_pushout f E)) o (g $o f) ==
   component2 (abses_pushout_morphism (abses_pushout f E) g) $o
   component2 (abses_pushout_morphism E f) o inclusion E) $o
inclusion (abses_pushout (g $o f) E) ==
inclusion (abses_pushout g (abses_pushout f E)) apply ab_pushout_rec_beta_left.
  -
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
E: AbSES B A0
projection (abses_pushout (g $o f) E) ==
projection (abses_pushout g (abses_pushout f E)) $o
ab_pushout_rec (inclusion (abses_pushout g (abses_pushout f E)))
  (component2 (abses_pushout_morphism (abses_pushout f E) g) $o
   component2 (abses_pushout_morphism E f))
  ((fun a0 : A0 =>
    left_square (abses_pushout_morphism (abses_pushout f E) g) (f a0) @
    ap (component2 (abses_pushout_morphism (abses_pushout f E) g))
      (left_square (abses_pushout_morphism E f) a0))
   :
   inclusion (abses_pushout g (abses_pushout f E)) o (g $o f) ==
   component2 (abses_pushout_morphism (abses_pushout f E) g) $o
   component2 (abses_pushout_morphism E f) o inclusion E) srapply Quotient_ind_hprop.
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
E: AbSES B A0
forall a : ab_biprod A2 E,
(fun
   x : ab_biprod A2 E /
       in_cosetL
         {|
           normalsubgroup_subgroup :=
             ab_pushout_subgroup (g $o f) (inclusion E);
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup (ab_biprod A2 E)
               (ab_pushout_subgroup (g $o f) (inclusion E))
         |} =>
 projection (abses_pushout (g $o f) E) x =
 (projection (abses_pushout g (abses_pushout f E)) $o
  ab_pushout_rec (inclusion (abses_pushout g (abses_pushout f E)))
    (component2 (abses_pushout_morphism (abses_pushout f E) g) $o
     component2 (abses_pushout_morphism E f))
    ((fun a0 : A0 =>
      left_square (abses_pushout_morphism (abses_pushout f E) g) (f a0) @
      ap (component2 (abses_pushout_morphism (abses_pushout f E) g))
        (left_square (abses_pushout_morphism E f) a0))
     :
     inclusion (abses_pushout g (abses_pushout f E)) o (g $o f) ==
     component2 (abses_pushout_morphism (abses_pushout f E) g) $o
     component2 (abses_pushout_morphism E f) o inclusion E))
   x)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup :=
            ab_pushout_subgroup (g $o f) (inclusion E);
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup (ab_biprod A2 E)
              (ab_pushout_subgroup (g $o f) (inclusion E))
        |})
     a)
    intro x; simpl.
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
E: AbSES B A0
x: ab_biprod A2 E
group_unit + projection E (snd x) =
group_unit + (group_unit + projection E (0 + snd x))
    apply grp_cancelL; symmetry.
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
E: AbSES B A0
x: ab_biprod A2 E
group_unit + projection E (0 + snd x) = projection E (snd x)
    exact (left_identity _ @ ap (projection E) (left_identity _)).
Defined.

Definition abses_pushout_compose `{Univalence} {A0 A1 A2 B : AbGroup}
  (f : A0 $-> A1) (g : A1 $-> A2)
  : abses_pushout (g $o f) == abses_pushout (B:=B) g o abses_pushout f
  := equiv_path_data_homotopy _ _ (abses_pushout_compose' f g).

Definition abses_pushout_pcompose' `{Univalence} {A0 A1 A2 B : AbGroup}
  (f : A0 $-> A1) (g : A1 $-> A2)
  : abses_pushout' (B:=B) (g $o f) $=>* abses_pushout' g $o* abses_pushout' f.
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
abses_pushout' (g $o f) $=>* abses_pushout' g $o* abses_pushout' f
Proof.
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
abses_pushout' (g $o f) $=>* abses_pushout' g $o* abses_pushout' f
  exists (abses_pushout_compose' f g).
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
abses_pushout_compose' f g pt $==
bp_pointed (abses_pushout' (g $o f)) $@
(bp_pointed (abses_pushout' g $o* abses_pushout' f))^$
  apply gpd_moveL_Vh. (* it's easiest to construct a path in [pt] *)
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
bp_pointed (abses_pushout' g $o* abses_pushout' f) $o
abses_pushout_compose' f g pt $== bp_pointed (abses_pushout' (g $o f))
  rapply Quotient_ind_hprop; intros [a2 [a0 b]]; simpl.
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
a2: A2
a0: A0
b: B
(a2 + group_unit + group_unit, group_unit) +
(g (0 + (0 + group_unit + f (0 + a0))), 0 + (group_unit + (0 + b))) =
(a2, group_unit) + (g (f a0), b)
  by rewrite 7 grp_unit_l, 2 grp_unit_r.
Defined.

Definition abses_pushout_pcompose `{Univalence} {A0 A1 A2 B : AbGroup}
  (f : A0 $-> A1) (g : A1 $-> A2)
  : abses_pushout_pmap (B:=B) (g $o f)
      ==* abses_pushout_pmap g o* abses_pushout_pmap f.
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
abses_pushout_pmap (g $o f) ==* abses_pushout_pmap g o* abses_pushout_pmap f
Proof.
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
abses_pushout_pmap (g $o f) ==* abses_pushout_pmap g o* abses_pushout_pmap f
  refine (_ @* (to_pointed_compose _ _)^*).
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
abses_pushout_pmap (g $o f) ==*
to_pointed (abses_pushout' g $o* abses_pushout' f)
  apply equiv_ptransformation_phomotopy.
H: Univalence
A0, A1, A2, B: AbGroup
f: A0 $-> A1
g: A1 $-> A2
abses_pushout' (g $o f) $=>* abses_pushout' g $o* abses_pushout' f
  apply abses_pushout_pcompose'.
Defined.

(** [AbSES B : AbGroup -> pType] and [AbSES' B : AbGroup -> Type] are covariant functors, for any [B]. *)

Instance is0functor_abses'01 `{Univalence} {B : AbGroup^op}
  : Is0Functor (AbSES' B).
H: Univalence
B: AbGroup^op
Is0Functor (AbSES' B)
Proof.
H: Univalence
B: AbGroup^op
Is0Functor (AbSES' B)
  apply Build_Is0Functor.
H: Univalence
B: AbGroup^op
forall a b : AbGroup, (a $-> b) -> AbSES' B a $-> AbSES' B b
  exact (fun _ _ g => abses_pushout g).
Defined.

Instance is1functor_abses'01 `{Univalence} {B : AbGroup^op}
  : Is1Functor (AbSES' B).
H: Univalence
B: AbGroup^op
Is1Functor (AbSES' B)
Proof.
H: Univalence
B: AbGroup^op
Is1Functor (AbSES' B)
  apply Build_Is1Functor; intros; cbn.
H: Univalence
B: AbGroup^op
a, b: AbGroup
f, g: a $-> b
X: f $== g
abses_pushout f == abses_pushout g
H: Univalence
B: AbGroup^op
a: AbGroup
abses_pushout grp_homo_id == idmap
H: Univalence
B: AbGroup^op
a, b, c: AbGroup
f: a $-> b
g: b $-> c
abses_pushout (grp_homo_compose g f) ==
(fun x : AbSES' B a => abses_pushout g (abses_pushout f x))
  -
H: Univalence
B: AbGroup^op
a, b: AbGroup
f, g: a $-> b
X: f $== g
abses_pushout f == abses_pushout g by apply abses_pushout_homotopic.
  -
H: Univalence
B: AbGroup^op
a: AbGroup
abses_pushout grp_homo_id == idmap exact abses_pushout_id.
  -
H: Univalence
B: AbGroup^op
a, b, c: AbGroup
f: a $-> b
g: b $-> c
abses_pushout (grp_homo_compose g f) ==
(fun x : AbSES' B a => abses_pushout g (abses_pushout f x)) apply abses_pushout_compose.
Defined.

Instance is0functor_abses01 `{Univalence} {B : AbGroup^op}
  : Is0Functor (AbSES B).
H: Univalence
B: AbGroup^op
Is0Functor (AbSES B)
Proof.
H: Univalence
B: AbGroup^op
Is0Functor (AbSES B)
  apply Build_Is0Functor.
H: Univalence
B: AbGroup^op
forall a b : AbGroup, (a $-> b) -> AbSES B a $-> AbSES B b
  exact (fun _ _ g => abses_pushout_pmap g).
Defined.

Instance is1functor_abses01 `{Univalence} {B : AbGroup^op}
  : Is1Functor (AbSES B).
H: Univalence
B: AbGroup^op
Is1Functor (AbSES B)
Proof.
H: Univalence
B: AbGroup^op
Is1Functor (AbSES B)
  apply Build_Is1Functor; intros; cbn.
H: Univalence
B: AbGroup^op
a, b: AbGroup
f, g: a $-> b
X: f $== g
abses_pushout_pmap f ==* abses_pushout_pmap g
H: Univalence
B: AbGroup^op
a: AbGroup
abses_pushout_pmap grp_homo_id ==* pmap_idmap
H: Univalence
B: AbGroup^op
a, b, c: AbGroup
f: a $-> b
g: b $-> c
abses_pushout_pmap (grp_homo_compose g f) ==*
abses_pushout_pmap g o* abses_pushout_pmap f
  -
H: Univalence
B: AbGroup^op
a, b: AbGroup
f, g: a $-> b
X: f $== g
abses_pushout_pmap f ==* abses_pushout_pmap g by apply abses_pushout_phomotopic.
  -
H: Univalence
B: AbGroup^op
a: AbGroup
abses_pushout_pmap grp_homo_id ==* pmap_idmap apply abses_pushout_pmap_id.
  -
H: Univalence
B: AbGroup^op
a, b, c: AbGroup
f: a $-> b
g: b $-> c
abses_pushout_pmap (grp_homo_compose g f) ==*
abses_pushout_pmap g o* abses_pushout_pmap f apply abses_pushout_pcompose.
Defined.