Require Import Basics Types Truncations.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat 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 mc_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'
  snrapply (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))) nrapply (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
    nrapply 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))) snrapply 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
      nrapply 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 = 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'
c_in_kernel: projection E c = mon_unit
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 = mon_unit 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 = mon_unit
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 = mon_unit
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 = mon_unit
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 = mon_unit
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 = mon_unit
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 = mon_unit
a: A
s: inclusion E a = c
(class_of
   (fun x y : A' * E =>
    Trunc (-1)
      {a : A &
      (- f a, inclusion E a) =
      (- 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 = mon_unit
a: A
s: inclusion E a = c
class_of
  (fun x y : A' * E =>
   Trunc (-1)
     {a : A &
     (- f a, inclusion E a) =
     (- 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 = mon_unit
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 = mon_unit
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 = mon_unit
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 = mon_unit
a: A
s: inclusion E a = c
Trunc (-1)
  {a0 : A &
  (- f a0, inclusion E a0) =
  (- 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 = mon_unit
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 = mon_unit
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 = mon_unit
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 = mon_unit
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 = mon_unit
a: A
s: inclusion E a = c
- - b + - f (- a) = b + - f (- a)
        by rewrite negate_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 = mon_unit
a: A
s: inclusion E a = c
inclusion E (- a) = - c + group_unit exact ((preserves_negate 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)
  snrapply (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
  snrapply (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 + mon_unit
    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) snrapply (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))
    refine (grp_homo_op (projection F) _ _ @ ap011 (+) _ _ @ (grp_homo_op _ _ _ )^).
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)) = mon_unit
      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 = mon_unit + 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
  nrapply 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)
  nrapply 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. *)

Global 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%path)
  ((fun (x y : A -> F) (p : x == y) (x0 : A) =>
    (p 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) nrapply 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%path)
  ((fun (x y : A -> F) (p : x == y) (x0 : A) =>
    (p 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 x : ab_biprod A' E,
(fun
   q : 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) q =
 (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%path)
    ((fun (x0 y : A -> F) (p : x0 == y) (x1 : A) =>
      (p x1)^) (p.1 $o inclusion E)
       (inclusion F $o grp_homo_id) (fst p.2))) q)
  (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))
        |}) x)
    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.

Global 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) {a : A & (- f a, inclusion F a) = - x + y})
  (a', group_unit) +
class_of
  (fun x y : A' * F =>
   Tr (-1) {a : A & (- f a, inclusion F a) = - x + y})
  (group_unit, g0.1 e) =
class_of
  (fun x y : A' * F =>
   Tr (-1) {a : A & (- f a, inclusion F a) = - x + y})
  (a', group_unit) +
class_of
  (fun x y : A' * F =>
   Tr (-1) {a : A & (- f a, inclusion F a) = - 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) {a : A & (- f a, inclusion E a) = - x + y})
  (a', group_unit) +
class_of
  (fun x y : A' * E =>
   Tr (-1) {a : A & (- f a, inclusion E a) = - x + y})
  (group_unit, e) =
class_of
  (fun x y : A' * E =>
   Tr (-1) {a : A & (- f a, inclusion E a) = - 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) {a : A & (- f a, inclusion G a) = - x + y})
  (a', group_unit) +
class_of
  (fun x y : A' * G =>
   Tr (-1) {a : A & (- f a, inclusion G a) = - x + y})
  (group_unit, g1.1 (g0.1 e)) =
class_of
  (fun x y : A' * G =>
   Tr (-1) {a : A & (- f a, inclusion G a) = - x + y})
  (a' + group_unit, group_unit) +
class_of
  (fun x y : A' * G =>
   Tr (-1) {a : A & (- f a, inclusion G a) = - 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 x : ab_biprod A' E,
(fun
   q : 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 q =
 (Id (abses_pushout f E)).1 q)
  (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))
        |}) x)
  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) {a : A & (- f a, inclusion E a) = - x + y})
  (a', group_unit) +
class_of
  (fun x y : A' * E =>
   Tr (-1) {a : A & (- f a, inclusion E a) = - x + y})
  (group_unit, e) =
class_of
  (fun x y : A' * E =>
   Tr (-1) {a : A & (- f a, inclusion E a) = - x + y})
  (a', e)
  apply qglue.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
a': A'
e: E
Tr (-1)
  {a : A &
  (- f a, inclusion E a) =
  - ((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
(- f 0, 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
- mon_unit = - (a' + group_unit) + a'
    refine (negate_mon_unit @ _).
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E: AbSES B A
a': A'
e: E
mon_unit = - (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 + mon_unit = 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
mon_unit = - (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 + mon_unit = 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%path))
  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%path)
  2: refine ((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'
GroupHomomorphism (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'
GroupHomomorphism (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%path) $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%path) $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%path) $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%path) $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%path) $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 mon_unit = 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%path) $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 + mon_unit = 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%path) srapply Quotient_ind_hprop.
H: Univalence
A, A', B: AbGroup
f: A $-> A'
forall x : ab_biprod A' pt,
(fun
   q : 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) q =
 (projection pt $o
  ab_pushout_rec ab_biprod_inl
    (functor_ab_biprod f grp_homo_id)
    (fun x0 : A => 1%path)) q)
  (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))
        |}) x)
    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
?Goal 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: apply 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. *)
  nrapply (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%path) =
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%path)).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%path)).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
GroupHomomorphism (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
GroupHomomorphism (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: apply 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)
    apply (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' (mon_unit + a), mon_unit + 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' (mon_unit + 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 + (mon_unit + 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' (mon_unit + 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 + (mon_unit + 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
GroupHomomorphism (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
GroupHomomorphism (abses_pushout (g $o f) E)
  (abses_pushout g (abses_pushout f E)) snrapply 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 x : ab_biprod A2 E,
(fun
   q : 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) q =
 (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)) q)
  (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))
        |}) x)
    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 (mon_unit + 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 (mon_unit + 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
   (mon_unit +
    (mon_unit + group_unit + f (mon_unit + a0))),
mon_unit + (group_unit + (mon_unit + 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]. *)

Global 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.

Global 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 apply 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.

Global 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.

Global 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.