Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import HSet Limits.Pullback.
Require Import WildCat Pointed.Core Homotopy.ExactSequence.
Require Import Modalities.ReflectiveSubuniverse.
Require Import AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct.
Require Import AbSES.Core AbSES.DirectSum.

Local Open Scope abses_scope.

(** * Pullbacks of short exact sequences *)

(** A short exact sequence [A -> E -> B] can be pulled back along a map [B' -> B]. We start by defining the underlying map, then the pointed version. *)
Definition abses_pullback {A B B' : AbGroup} (f : B' $-> B)
  : AbSES B A -> AbSES B' A.
A, B, B': AbGroup
f: B' $-> B
AbSES B A -> AbSES B' A
Proof.
A, B, B': AbGroup
f: B' $-> B
AbSES B A -> AbSES B' A
  intro E.
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
AbSES B' A
  snapply (Build_AbSES (ab_pullback (projection E) f)
                        (grp_pullback_corec _ _ (inclusion _) grp_homo_const _)
                        (grp_pullback_pr2 (projection _) f)).
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
projection E o inclusion E == f o grp_homo_const
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
IsEmbedding
  (grp_pullback_corec (projection E) f (inclusion E)
     grp_homo_const ?p)
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
IsConnMap
  (Modality.modality_to_reflective_subuniverse
     (Core.Tr (-1)))
  (grp_pullback_pr2 (projection E) f)
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
IsExact (Core.Tr (-1))
  (grp_pullback_corec (projection E) f (inclusion E)
     grp_homo_const ?p)
  (grp_pullback_pr2 (projection E) f)
  -
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
projection E o inclusion E == f o grp_homo_const intro x.
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
x: A
projection E (inclusion E x) = f (grp_homo_const x)
    nrefine (_ @ (grp_homo_unit f)^).
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
x: A
projection E (inclusion E x) = mon_unit
    apply isexact_inclusion_projection.
  -
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
IsEmbedding
  (grp_pullback_corec (projection E) f (inclusion E)
     grp_homo_const
     ((fun x : A =>
       (let X := fun a : AbSES' B A => cx_isexact in
        let X0 :=
          fun a : AbSES' B A => pointed_fun (X a) in
        X0 E x) @ (grp_homo_unit f)^)
      :
      projection E o inclusion E == f o grp_homo_const)) exact (cancelL_isembedding (g:= grp_pullback_pr1 _ _)).
  -
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
IsConnMap
  (Modality.modality_to_reflective_subuniverse
     (Core.Tr (-1)))
  (grp_pullback_pr2 (projection E) f) rapply conn_map_pullback'.
  -
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
IsExact (Core.Tr (-1))
  (grp_pullback_corec (projection E) f (inclusion E)
     grp_homo_const
     ((fun x : A =>
       (let X := fun a : AbSES' B A => cx_isexact in
        let X0 :=
          fun a : AbSES' B A => pointed_fun (X a) in
        X0 E x) @ (grp_homo_unit f)^)
      :
      projection E o inclusion E == f o grp_homo_const))
  (grp_pullback_pr2 (projection E) f) snapply Build_IsExact.
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
IsComplex
  (grp_pullback_corec (projection E) f (inclusion E)
     grp_homo_const
     ((fun x : A =>
       (let X := fun a : AbSES' B A => cx_isexact in
        let X0 :=
          fun a : AbSES' B A => pointed_fun (X a) in
        X0 E x) @ (grp_homo_unit f)^)
      :
      projection E o inclusion E == f o grp_homo_const))
  (grp_pullback_pr2 (projection E) f)
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
IsConnMap
  (Modality.modality_to_reflective_subuniverse
     (Core.Tr (-1))) (cxfib ?cx_isexact)
    +
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
IsComplex
  (grp_pullback_corec (projection E) f (inclusion E)
     grp_homo_const
     ((fun x : A =>
       (let X := fun a : AbSES' B A => cx_isexact in
        let X0 :=
          fun a : AbSES' B A => pointed_fun (X a) in
        X0 E x) @ (grp_homo_unit f)^)
      :
      projection E o inclusion E == f o grp_homo_const))
  (grp_pullback_pr2 (projection E) f) snapply phomotopy_homotopy_hset.
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
IsHSet B'
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
grp_pullback_pr2 (projection E) f
o* grp_pullback_corec (projection E) f (inclusion E)
     grp_homo_const
     ((fun x : A =>
       (let X := fun a : AbSES' B A => cx_isexact in
        let X0 :=
          fun a : AbSES' B A => pointed_fun (X a) in
        X0 E x) @ (grp_homo_unit f)^)
      :
      projection E o inclusion E == f o grp_homo_const) ==
pconst
      *
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
IsHSet B' exact _.
      *
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
grp_pullback_pr2 (projection E) f
o* grp_pullback_corec (projection E) f (inclusion E)
     grp_homo_const
     ((fun x : A =>
       (let X := fun a : AbSES' B A => cx_isexact in
        let X0 :=
          fun a : AbSES' B A => pointed_fun (X a) in
        X0 E x) @ (grp_homo_unit f)^)
      :
      projection E o inclusion E == f o grp_homo_const) ==
pconst reflexivity.
    +
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
IsConnMap
  (Modality.modality_to_reflective_subuniverse
     (Core.Tr (-1)))
  (cxfib (phomotopy_homotopy_hset (fun x0 : A => 1))) nrefine (cancelL_equiv_conn_map
                 _ _ (hfiber_pullback_along_pointed f (projection _) (grp_homo_unit _))).
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
IsConnMap
  (Modality.modality_to_reflective_subuniverse
     (Core.Tr (-1)))
  (fun x : A =>
   hfiber_pullback_along_pointed f (projection E)
     (grp_homo_unit f)
     (cxfib
        (phomotopy_homotopy_hset (fun x0 : A => 1)) x))
      nrefine (conn_map_homotopic _ _ _ _ (conn_map_isexact (IsExact:=isexact_inclusion_projection _))).
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
cxfib cx_isexact ==
(fun x : A =>
 hfiber_pullback_along_pointed f (projection E)
   (grp_homo_unit f)
   (cxfib (phomotopy_homotopy_hset (fun x0 : A => 1))
      x))
      intro a.
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
a: A
cxfib cx_isexact a =
hfiber_pullback_along_pointed f (projection E)
  (grp_homo_unit f)
  (cxfib (phomotopy_homotopy_hset (fun x0 : A => 1)) a)
      by apply path_sigma_hprop.
Defined.

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

(** The natural map from the pulled back sequence. *)
Definition abses_pullback_morphism {A B B' : AbGroup@{u}}
  (E : AbSES B A) (f : B' $-> B)
  : AbSESMorphism (abses_pullback f E) E.
A, B, B': AbGroup
E: AbSES B A
f: B' $-> B
AbSESMorphism (abses_pullback f E) E
Proof.
A, B, B': AbGroup
E: AbSES B A
f: B' $-> B
AbSESMorphism (abses_pullback f E) E
  snapply (Build_AbSESMorphism grp_homo_id _ f).
A, B, B': AbGroup
E: AbSES B A
f: B' $-> B
abses_pullback f E $-> E
A, B, B': AbGroup
E: AbSES B A
f: B' $-> B
inclusion E $o grp_homo_id ==
?component2 $o inclusion (abses_pullback f E)
A, B, B': AbGroup
E: AbSES B A
f: B' $-> B
projection E $o ?component2 ==
f $o projection (abses_pullback f E)
  -
A, B, B': AbGroup
E: AbSES B A
f: B' $-> B
abses_pullback f E $-> E apply grp_pullback_pr1.
  -
A, B, B': AbGroup
E: AbSES B A
f: B' $-> B
inclusion E $o grp_homo_id ==
grp_pullback_pr1 (projection E) f $o
inclusion (abses_pullback f E) reflexivity.
  -
A, B, B': AbGroup
E: AbSES B A
f: B' $-> B
projection E $o grp_pullback_pr1 (projection E) f ==
f $o projection (abses_pullback f E) apply pullback_commsq.
Defined.

(** Any map [f : E -> F] of short exact sequences factors (uniquely) through [abses_pullback F f3]. *)
Definition abses_pullback_morphism_corec {A B X Y : AbGroup@{u}}
  {E : AbSES B A} {F : AbSES Y X} (f : AbSESMorphism E F)
  : AbSESMorphism E (abses_pullback (component3 f) F).
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
AbSESMorphism E (abses_pullback (component3 f) F)
Proof.
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
AbSESMorphism E (abses_pullback (component3 f) F)
  snapply (Build_AbSESMorphism (component1 f) _ grp_homo_id).
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
E $-> abses_pullback (component3 f) F
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
inclusion (abses_pullback (component3 f) F) $o
component1 f == ?component2 $o inclusion E
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
projection (abses_pullback (component3 f) F) $o
?component2 == grp_homo_id $o projection E
  -
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
E $-> abses_pullback (component3 f) F apply (grp_pullback_corec (projection F) (component3 f)
                              (component2 f) (projection E)).
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
(fun x : E => projection F (component2 f x)) ==
(fun x : E => component3 f (projection E x))
    apply right_square.
  -
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
inclusion (abses_pullback (component3 f) F) $o
component1 f ==
grp_pullback_corec (projection F) (component3 f)
  (component2 f) (projection E) (right_square f) $o
inclusion E intro x; cbn.
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
x: A
(inclusion F (component1 f x); group_unit;
cx_isexact (component1 f x) @
(grp_homo_unit (component3 f))^) =
(component2 f (inclusion E x);
projection E (inclusion E x);
right_square f (inclusion E x))
    apply equiv_path_pullback_hset; cbn; split.
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
x: A
inclusion F (component1 f x) =
component2 f (inclusion E x)
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
x: A
group_unit = projection E (inclusion E x)
    +
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
x: A
inclusion F (component1 f x) =
component2 f (inclusion E x) apply left_square.
    +
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
x: A
group_unit = projection E (inclusion E x) symmetry; apply iscomplex_abses.
  -
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
projection (abses_pullback (component3 f) F) $o
grp_pullback_corec (projection F) (component3 f)
  (component2 f) (projection E) (right_square f) ==
grp_homo_id $o projection E reflexivity.
Defined.

(** The original map factors via the induced map. *)
Definition abses_pullback_morphism_corec_beta `{Funext}
  {A B X Y : AbGroup@{u}} {E : AbSES B A} {F : AbSES Y X}
  (f : AbSESMorphism E F)
  : f = absesmorphism_compose (abses_pullback_morphism F (component3 f))
                              (abses_pullback_morphism_corec f).
H: Funext
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
f =
absesmorphism_compose
  (abses_pullback_morphism F (component3 f))
  (abses_pullback_morphism_corec f)
Proof.
H: Funext
A, B, X, Y: AbGroup
E: AbSES B A
F: AbSES Y X
f: AbSESMorphism E F
f =
absesmorphism_compose
  (abses_pullback_morphism F (component3 f))
  (abses_pullback_morphism_corec f)
  apply (equiv_ap issig_AbSESMorphism^-1 _ _).
H: Funext
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_pullback_morphism F (component3 f))
     (abses_pullback_morphism_corec f))
  srapply path_sigma_hprop.
H: Funext
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_pullback_morphism F (component3 f))
      (abses_pullback_morphism_corec f))).1
  apply path_prod.
H: Funext
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_pullback_morphism F (component3 f))
        (abses_pullback_morphism_corec f))).1
H: Funext
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_pullback_morphism F (component3 f))
        (abses_pullback_morphism_corec f))).1
  1: apply path_prod.
H: Funext
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_pullback_morphism F (component3 f))
           (abses_pullback_morphism_corec f))).1)
H: Funext
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_pullback_morphism F (component3 f))
           (abses_pullback_morphism_corec f))).1)
H: Funext
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_pullback_morphism F (component3 f))
        (abses_pullback_morphism_corec f))).1
  all: by apply equiv_path_grouphomomorphism.
Defined.

Definition abses_pullback_component1_id'
  {A B B' : AbGroup@{u}} {E : AbSES B A} {F : AbSES B' A}
  (f : AbSESMorphism E F) (h : component1 f == grp_homo_id)
  : E $== abses_pullback (component3 f) F.
A, B, B': AbGroup
E: AbSES B A
F: AbSES B' A
f: AbSESMorphism E F
h: component1 f == grp_homo_id
E $== abses_pullback (component3 f) F
Proof.
A, B, B': AbGroup
E: AbSES B A
F: AbSES B' A
f: AbSESMorphism E F
h: component1 f == grp_homo_id
E $== abses_pullback (component3 f) F
  pose (g := abses_pullback_morphism_corec f).
A, B, B': AbGroup
E: AbSES B A
F: AbSES B' A
f: AbSESMorphism E F
h: component1 f == grp_homo_id
g:= abses_pullback_morphism_corec f: AbSESMorphism E (abses_pullback (component3 f) F)
E $== abses_pullback (component3 f) F
  napply abses_path_data_to_iso.
A, B, B': AbGroup
E: AbSES B A
F: AbSES B' A
f: AbSESMorphism E F
h: component1 f == grp_homo_id
g:= abses_pullback_morphism_corec f: AbSESMorphism E (abses_pullback (component3 f) F)
abses_path_data E (abses_pullback (component3 f) F)
  exists (component2 g); split.
A, B, B': AbGroup
E: AbSES B A
F: AbSES B' A
f: AbSESMorphism E F
h: component1 f == grp_homo_id
g:= abses_pullback_morphism_corec f: AbSESMorphism E (abses_pullback (component3 f) F)
component2 g $o inclusion E ==
inclusion (abses_pullback (component3 f) F)
A, B, B': AbGroup
E: AbSES B A
F: AbSES B' A
f: AbSESMorphism E F
h: component1 f == grp_homo_id
g:= abses_pullback_morphism_corec f: AbSESMorphism E (abses_pullback (component3 f) F)
projection E ==
projection (abses_pullback (component3 f) F) $o
component2 g
  -
A, B, B': AbGroup
E: AbSES B A
F: AbSES B' A
f: AbSESMorphism E F
h: component1 f == grp_homo_id
g:= abses_pullback_morphism_corec f: AbSESMorphism E (abses_pullback (component3 f) F)
component2 g $o inclusion E ==
inclusion (abses_pullback (component3 f) F) exact (fun a => (left_square g a)^ @ ap _ (h a)).
  -
A, B, B': AbGroup
E: AbSES B A
F: AbSES B' A
f: AbSESMorphism E F
h: component1 f == grp_homo_id
g:= abses_pullback_morphism_corec f: AbSESMorphism E (abses_pullback (component3 f) F)
projection E ==
projection (abses_pullback (component3 f) F) $o
component2 g reflexivity.
Defined.

(** In particular, if [component1] of a morphism is the identity, then it exhibits the domain as the pullback of the codomain. *)
Definition abses_pullback_component1_id `{Univalence} {A B B' : AbGroup}
  {E : AbSES B A} {F : AbSES B' A}
  (f : AbSESMorphism E F) (h : component1 f == grp_homo_id)
  : E = abses_pullback (component3 f) F
  := equiv_path_abses_iso (abses_pullback_component1_id' f h).

(** For any two [E, F : AbSES B A] and [f, g : B' $-> B], there is a morphism [Ef + Fg -> E + F] induced by the universal properties of the pullbacks of E and F, respectively. *)
Definition abses_directsum_pullback_morphism `{Funext}
  {A B B' C D D' : AbGroup@{u}} {E : AbSES B A} {F : AbSES D C}
  (f : B' $-> B) (g : D' $-> D)
  : AbSESMorphism
      (abses_direct_sum (abses_pullback f E) (abses_pullback g F))
      (abses_direct_sum E F)
  := functor_abses_directsum
       (abses_pullback_morphism E f) (abses_pullback_morphism F g).

(** For any two [E, F : AbSES B A] and [f, g : B' $-> B], we have (E + F)(f + g) = Ef + Eg, where + denotes the direct sum. *)
Definition abses_directsum_distributive_pullbacks `{Univalence}
  {A B B' C D D' : AbGroup@{u}}
  {E : AbSES B A} {F : AbSES D C} (f : B' $-> B) (g : D' $-> D)
  : abses_pullback (functor_ab_biprod f g) (abses_direct_sum E F)
    = abses_direct_sum (abses_pullback f E) (abses_pullback g F)
  := (abses_pullback_component1_id (abses_directsum_pullback_morphism f g)
        (fun _ => idpath))^.

Definition abses_path_pullback_projection_commsq
  {A B B' : AbGroup@{u}} (bt : B' $-> B)
  (E : AbSES B A) (F : AbSES B' A) (p : abses_pullback bt E = F)
  : exists phi : middle F $-> E, projection E o phi == bt o projection F.
A, B, B': AbGroup
bt: B' $-> B
E: AbSES B A
F: AbSES B' A
p: abses_pullback bt E = F
{phi : F $-> E &
projection E o phi == bt o projection F}
Proof.
A, B, B': AbGroup
bt: B' $-> B
E: AbSES B A
F: AbSES B' A
p: abses_pullback bt E = F
{phi : F $-> E &
projection E o phi == bt o projection F}
  induction p.
A, B, B': AbGroup
bt: B' $-> B
E: AbSES B A
{phi : abses_pullback bt E $-> E &
(fun x : abses_pullback bt E => projection E (phi x)) ==
(fun x : abses_pullback bt E =>
 bt (projection (abses_pullback bt E) x))}
  exists (grp_pullback_pr1 _ _); intro x.
A, B, B': AbGroup
bt: B' $-> B
E: AbSES B A
x: abses_pullback bt E
projection E (grp_pullback_pr1 (projection E) bt x) =
bt (projection (abses_pullback bt E) x)
  napply pullback_commsq.
Defined.


(** ** Functoriality of [abses_pullback f] for [f : B' $-> B] *)

(** As any function, [abses_pullback f] acts on paths. By explicitly describing the analogous action on path data we get an action which computes, this turn out to be useful. *)

Instance is0functor_abses_pullback {A B B' : AbGroup} (f : B' $-> B)
  : Is0Functor (abses_pullback (A:=A) f).
A, B, B': AbGroup
f: B' $-> B
Is0Functor (abses_pullback f)
Proof.
A, B, B': AbGroup
f: B' $-> B
Is0Functor (abses_pullback f)
  srapply Build_Is0Functor;
    intros E F p.
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
abses_pullback f E $-> abses_pullback f F
  snrefine (_; (_,_)).
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
GroupIsomorphism (abses_pullback f E)
  (abses_pullback f F)
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
?proj1 $o inclusion (abses_pullback f E) ==
inclusion (abses_pullback f F)
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
projection (abses_pullback f E) ==
projection (abses_pullback f F) $o ?proj1
  -
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
GroupIsomorphism (abses_pullback f E)
  (abses_pullback f F) srapply equiv_functor_grp_pullback.
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
GroupIsomorphism B B
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
GroupIsomorphism E F
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
GroupIsomorphism B' B'
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
projection F o ?beta == ?alpha o projection E
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
?alpha o f == f o ?gamma
    1,3: exact grp_iso_id.
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
GroupIsomorphism E F
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
projection F o ?beta == grp_iso_id o projection E
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
grp_iso_id o f == f o grp_iso_id
    1: exact p.1.
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
projection F o p.1 == grp_iso_id o projection E
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
grp_iso_id o f == f o grp_iso_id
    2: reflexivity.
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
projection F o p.1 == grp_iso_id o projection E
    intro x.
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
x: E
projection F (p.1 x) = grp_iso_id (projection E x)
    exact (snd p.2 x)^.
  -
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
equiv_functor_grp_pullback (projection E)
  (projection F) f f grp_iso_id p.1 grp_iso_id
  ((fun x : E => (snd p.2 x)^)
   :
   projection F o p.1 == grp_iso_id o projection E)
  (fun x0 : B' => 1) $o inclusion (abses_pullback f E) ==
inclusion (abses_pullback f F) intro x.
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
x: A
(equiv_functor_grp_pullback (projection E)
   (projection F) f f grp_iso_id p.1 grp_iso_id
   (fun x : E => (snd p.2 x)^) (fun x0 : B' => 1) $o
 inclusion (abses_pullback f E)) x =
inclusion (abses_pullback f F) x
    srapply equiv_path_pullback_hset; split; cbn.
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
x: A
p.1 (inclusion E x) = inclusion F x
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
x: A
group_unit = group_unit
    2: reflexivity.
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
x: A
p.1 (inclusion E x) = inclusion F x
    exact (fst p.2 x).
  -
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p: E $-> F
projection (abses_pullback f E) ==
projection (abses_pullback f F) $o
equiv_functor_grp_pullback (projection E)
  (projection F) f f grp_iso_id p.1 grp_iso_id
  ((fun x : E => (snd p.2 x)^)
   :
   projection F o p.1 == grp_iso_id o projection E)
  (fun x0 : B' => 1) reflexivity.
Defined.

Instance is1functor_abses_pullback {A B B' : AbGroup} (f : B' $-> B)
  : Is1Functor (abses_pullback (A:=A) f).
A, B, B': AbGroup
f: B' $-> B
Is1Functor (abses_pullback f)
Proof.
A, B, B': AbGroup
f: B' $-> B
Is1Functor (abses_pullback f)
  snapply Build_Is1Functor.
A, B, B': AbGroup
f: B' $-> B
forall (a b : AbSES B A) (f0 g : a $-> b),
f0 $== g ->
fmap (abses_pullback f) f0 $==
fmap (abses_pullback f) g
A, B, B': AbGroup
f: B' $-> B
forall a : AbSES B A,
fmap (abses_pullback f) (Id a) $==
Id (abses_pullback f a)
A, B, B': AbGroup
f: B' $-> B
forall (a b c : AbSES B A) (f0 : a $-> b)
(g : b $-> c),
fmap (abses_pullback f) (g $o f0) $==
fmap (abses_pullback f) g $o
fmap (abses_pullback f) f0
  -
A, B, B': AbGroup
f: B' $-> B
forall (a b : AbSES B A) (f0 g : a $-> b),
f0 $== g ->
fmap (abses_pullback f) f0 $==
fmap (abses_pullback f) g intros E F p q h x.
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p, q: E $-> F
h: p $== q
x: abses_pullback f E
(fmap (abses_pullback f) p).1 x =
(fmap (abses_pullback f) q).1 x
    srapply equiv_path_pullback_hset; split; cbn.
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p, q: E $-> F
h: p $== q
x: abses_pullback f E
p.1 (pullback_pr1 x) = q.1 (pullback_pr1 x)
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p, q: E $-> F
h: p $== q
x: abses_pullback f E
pullback_pr2 x = pullback_pr2 x
    2: reflexivity.
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
p, q: E $-> F
h: p $== q
x: abses_pullback f E
p.1 (pullback_pr1 x) = q.1 (pullback_pr1 x)
    exact (h _).
  -
A, B, B': AbGroup
f: B' $-> B
forall a : AbSES B A,
fmap (abses_pullback f) (Id a) $==
Id (abses_pullback f a) intros E x.
A, B, B': AbGroup
f: B' $-> B
E: AbSES B A
x: abses_pullback f E
(fmap (abses_pullback f) (Id E)).1 x =
(Id (abses_pullback f E)).1 x
    by srapply equiv_path_pullback_hset.
  -
A, B, B': AbGroup
f: B' $-> B
forall (a b c : AbSES B A) (f0 : a $-> b)
(g : b $-> c),
fmap (abses_pullback f) (g $o f0) $==
fmap (abses_pullback f) g $o
fmap (abses_pullback f) f0 intros E F G p q x.
A, B, B': AbGroup
f: B' $-> B
E, F, G: AbSES B A
p: E $-> F
q: F $-> G
x: abses_pullback f E
(fmap (abses_pullback f) (q $o p)).1 x =
(fmap (abses_pullback f) q $o
 fmap (abses_pullback f) p).1 x
    by srapply equiv_path_pullback_hset.
Defined.

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

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

Definition abses_pullback_point' {A B B' : AbGroup} (f : B' $-> B)
  : (abses_pullback f pt) $== (point (AbSES B' A)).
A, B, B': AbGroup
f: B' $-> B
abses_pullback f pt $== pt
Proof.
A, B, B': AbGroup
f: B' $-> B
abses_pullback f pt $== pt
  snrefine (_; (_, _)).
A, B, B': AbGroup
f: B' $-> B
GroupIsomorphism (abses_pullback f pt) pt
A, B, B': AbGroup
f: B' $-> B
?proj1 $o inclusion (abses_pullback f pt) ==
inclusion pt
A, B, B': AbGroup
f: B' $-> B
projection (abses_pullback f pt) ==
projection pt $o ?proj1
  -
A, B, B': AbGroup
f: B' $-> B
GroupIsomorphism (abses_pullback f pt) pt snapply Build_GroupIsomorphism.
A, B, B': AbGroup
f: B' $-> B
GroupHomomorphism (abses_pullback f pt) pt
A, B, B': AbGroup
f: B' $-> B
IsEquiv ?grp_iso_homo
    +
A, B, B': AbGroup
f: B' $-> B
GroupHomomorphism (abses_pullback f pt) pt srapply ab_biprod_corec.
A, B, B': AbGroup
f: B' $-> B
abses_pullback f pt $-> A
A, B, B': AbGroup
f: B' $-> B
abses_pullback f pt $-> B'
      *
A, B, B': AbGroup
f: B' $-> B
abses_pullback f pt $-> A refine (ab_biprod_pr1 $o _).
A, B, B': AbGroup
f: B' $-> B
abses_pullback f pt $-> ab_biprod A ?Goal
        apply grp_pullback_pr1.
      *
A, B, B': AbGroup
f: B' $-> B
abses_pullback f pt $-> B' apply projection.
    +
A, B, B': AbGroup
f: B' $-> B
IsEquiv
  (ab_biprod_corec
     (ab_biprod_pr1 $o
      grp_pullback_pr1 (projection pt) f)
     (projection (abses_pullback f pt))) srapply isequiv_adjointify.
A, B, B': AbGroup
f: B' $-> B
pt -> abses_pullback f pt
A, B, B': AbGroup
f: B' $-> B
ab_biprod_corec
  (ab_biprod_pr1 $o grp_pullback_pr1 (projection pt) f)
  (projection (abses_pullback f pt)) o ?g == idmap
A, B, B': AbGroup
f: B' $-> B
?g
o ab_biprod_corec
    (ab_biprod_pr1 $o
     grp_pullback_pr1 (projection pt) f)
    (projection (abses_pullback f pt)) == idmap
      *
A, B, B': AbGroup
f: B' $-> B
pt -> abses_pullback f pt snapply grp_pullback_corec.
A, B, B': AbGroup
f: B' $-> B
pt $-> pt
A, B, B': AbGroup
f: B' $-> B
pt $-> B'
A, B, B': AbGroup
f: B' $-> B
projection pt o ?b == f o ?c
        --
A, B, B': AbGroup
f: B' $-> B
pt $-> pt exact (functor_ab_biprod grp_homo_id f).
        --
A, B, B': AbGroup
f: B' $-> B
pt $-> B' exact ab_biprod_pr2.
        --
A, B, B': AbGroup
f: B' $-> B
projection pt o functor_ab_biprod grp_homo_id f ==
f o ab_biprod_pr2 reflexivity.
      *
A, B, B': AbGroup
f: B' $-> B
ab_biprod_corec
  (ab_biprod_pr1 $o grp_pullback_pr1 (projection pt) f)
  (projection (abses_pullback f pt))
o grp_pullback_corec (projection pt) f
    (functor_ab_biprod grp_homo_id f) ab_biprod_pr2
    (fun x0 : A * B' => 1) == idmap reflexivity.
      *
A, B, B': AbGroup
f: B' $-> B
grp_pullback_corec (projection pt) f
  (functor_ab_biprod grp_homo_id f) ab_biprod_pr2
  (fun x0 : A * B' => 1)
o ab_biprod_corec
    (ab_biprod_pr1 $o
     grp_pullback_pr1 (projection pt) f)
    (projection (abses_pullback f pt)) == idmap intros [[a b] [b' c]].
A, B, B': AbGroup
f: B' $-> B
a: A
b: B
b': B'
c: projection pt (a, b) = f b'
grp_pullback_corec (projection pt) f
  (functor_ab_biprod grp_homo_id f) ab_biprod_pr2
  (fun x0 : A * B' => 1)
  (ab_biprod_corec
     (ab_biprod_pr1 $o
      grp_pullback_pr1 (projection pt) f)
     (projection (abses_pullback f pt))
     ((a, b); b'; c)) = ((a, b); b'; c)
        srapply equiv_path_pullback_hset; split; cbn.
A, B, B': AbGroup
f: B' $-> B
a: A
b: B
b': B'
c: projection pt (a, b) = f b'
(a, f b') = (a, b)
A, B, B': AbGroup
f: B' $-> B
a: A
b: B
b': B'
c: projection pt (a, b) = f b'
b' = b'
        2: reflexivity.
A, B, B': AbGroup
f: B' $-> B
a: A
b: B
b': B'
c: projection pt (a, b) = f b'
(a, f b') = (a, b)
        exact (path_prod' idpath c^).
  -
A, B, B': AbGroup
f: B' $-> B
{|
  grp_iso_homo :=
    ab_biprod_corec
      (ab_biprod_pr1 $o
       grp_pullback_pr1 (projection pt) f)
      (projection (abses_pullback f pt));
  isequiv_group_iso :=
    isequiv_adjointify
      (ab_biprod_corec
         (ab_biprod_pr1 $o
          grp_pullback_pr1 (projection pt) f)
         (projection (abses_pullback f pt)))
      (grp_pullback_corec (projection pt) f
         (functor_ab_biprod grp_homo_id f)
         ab_biprod_pr2 (fun x0 : A * B' => 1))
      (fun x0 : A * B' => 1)
      ((fun x : abses_pullback f pt =>
        (fun proj1 : pt =>
         (fun (a : A) (b : B)
            (proj2 : {c : B' &
                     projection pt (a, b) = f c}) =>
          (fun (b' : B')
             (c : projection pt (a, b) = f b') =>
           equiv_path_pullback_hset (projection pt) f
             (grp_pullback_corec (projection pt) f
                (functor_ab_biprod grp_homo_id f)
                ab_biprod_pr2 (fun x0 : A * B' => 1)
                (ab_biprod_corec
                   (ab_biprod_pr1 $o
                    grp_pullback_pr1 ... f)
                   (projection (...)) ((a, b); b'; c)))
             ((a, b); b'; c)
             (path_prod' 1 c^
              :
              (grp_pullback_corec (projection pt) f
                 (functor_ab_biprod grp_homo_id f)
                 ab_biprod_pr2 (... => 1)
                 (ab_biprod_corec ... ... ...)).1 =
              ((a, b); b'; c).1,
             1
             :
             ((grp_pullback_corec (...) f (...)
                 ab_biprod_pr2 (...) (...)).2).1 =
             (((a, b); b'; c).2).1)) proj2.1 proj2.2)
           (fst proj1) (snd proj1)) x.1 x.2)
       :
       grp_pullback_corec (projection pt) f
         (functor_ab_biprod grp_homo_id f)
         ab_biprod_pr2 (fun x0 : A * B' => 1)
       o ab_biprod_corec
           (ab_biprod_pr1 $o
            grp_pullback_pr1 (projection pt) f)
           (projection (abses_pullback f pt)) == idmap)
|} $o inclusion (abses_pullback f pt) == inclusion pt reflexivity.
  -
A, B, B': AbGroup
f: B' $-> B
projection (abses_pullback f pt) ==
projection pt $o
{|
  grp_iso_homo :=
    ab_biprod_corec
      (ab_biprod_pr1 $o
       grp_pullback_pr1 (projection pt) f)
      (projection (abses_pullback f pt));
  isequiv_group_iso :=
    isequiv_adjointify
      (ab_biprod_corec
         (ab_biprod_pr1 $o
          grp_pullback_pr1 (projection pt) f)
         (projection (abses_pullback f pt)))
      (grp_pullback_corec (projection pt) f
         (functor_ab_biprod grp_homo_id f)
         ab_biprod_pr2 (fun x0 : A * B' => 1))
      (fun x0 : A * B' => 1)
      ((fun x : abses_pullback f pt =>
        (fun proj1 : pt =>
         (fun (a : A) (b : B)
            (proj2 : {c : B' &
                     projection pt (a, b) = f c}) =>
          (fun (b' : B')
             (c : projection pt (a, b) = f b') =>
           equiv_path_pullback_hset (projection pt) f
             (grp_pullback_corec (projection pt) f
                (functor_ab_biprod grp_homo_id f)
                ab_biprod_pr2 (fun x0 : A * B' => 1)
                (ab_biprod_corec
                   (ab_biprod_pr1 $o
                    grp_pullback_pr1 ... f)
                   (projection (...)) ((a, b); b'; c)))
             ((a, b); b'; c)
             (path_prod' 1 c^
              :
              (grp_pullback_corec (projection pt) f
                 (functor_ab_biprod grp_homo_id f)
                 ab_biprod_pr2 (... => 1)
                 (ab_biprod_corec ... ... ...)).1 =
              ((a, b); b'; c).1,
             1
             :
             ((grp_pullback_corec (...) f (...)
                 ab_biprod_pr2 (...) (...)).2).1 =
             (((a, b); b'; c).2).1)) proj2.1 proj2.2)
           (fst proj1) (snd proj1)) x.1 x.2)
       :
       grp_pullback_corec (projection pt) f
         (functor_ab_biprod grp_homo_id f)
         ab_biprod_pr2 (fun x0 : A * B' => 1)
       o ab_biprod_corec
           (ab_biprod_pr1 $o
            grp_pullback_pr1 (projection pt) f)
           (projection (abses_pullback f pt)) == idmap)
|} reflexivity.
Defined.

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

Definition abses_pullback' {A B B' : AbGroup} (f : B' $-> B)
  : AbSES B A -->* AbSES B' A
  := Build_BasepointPreservingFunctor (abses_pullback f) (abses_pullback_point' f).

(** Pullback of short exact sequences as a pointed map. *)
Definition abses_pullback_pmap `{Univalence} {A B B' : AbGroup} (f : B' $-> B)
  : AbSES B A ->* AbSES B' A
  := to_pointed (abses_pullback' f).

(** ** Functoriality of [abses_pullback] *)

(** [abses_pullback] is pseudo-functorial, and we can state this in terms of actual homotopies or "path data homotopies." We decorate the latter with the suffix ('). *)

(** For every [E : AbSES B A], the pullback of [E] along [id_B] is [E]. *)
Definition abses_pullback_id `{Univalence} {A B : AbGroup}
  : abses_pullback (A:=A) (@grp_homo_id B) == idmap.
H: Univalence
A, B: AbGroup
abses_pullback grp_homo_id == idmap
Proof.
H: Univalence
A, B: AbGroup
abses_pullback grp_homo_id == idmap
  intro E.
H: Univalence
A, B: AbGroup
E: AbSES B A
abses_pullback grp_homo_id E = E
  apply equiv_path_abses_iso; srefine (_; (_, _)).
H: Univalence
A, B: AbGroup
E: AbSES B A
GroupIsomorphism (abses_pullback grp_homo_id E) E
H: Univalence
A, B: AbGroup
E: AbSES B A
?proj1 $o inclusion (abses_pullback grp_homo_id E) ==
inclusion E
H: Univalence
A, B: AbGroup
E: AbSES B A
projection (abses_pullback grp_homo_id E) ==
projection E $o ?proj1
  1: rapply (Build_GroupIsomorphism _ _ (grp_pullback_pr1 _ _)).
H: Univalence
A, B: AbGroup
E: AbSES B A
{|
  grp_iso_homo :=
    grp_pullback_pr1 (projection E) grp_homo_id;
  isequiv_group_iso :=
    isequiv_pr1
      (fun b : E =>
       {c : B & projection E b = grp_homo_id c})
|} $o inclusion (abses_pullback grp_homo_id E) ==
inclusion E
H: Univalence
A, B: AbGroup
E: AbSES B A
projection (abses_pullback grp_homo_id E) ==
projection E $o
{|
  grp_iso_homo :=
    grp_pullback_pr1 (projection E) grp_homo_id;
  isequiv_group_iso :=
    isequiv_pr1
      (fun b : E =>
       {c : B & projection E b = grp_homo_id c})
|}
  1: reflexivity.
H: Univalence
A, B: AbGroup
E: AbSES B A
projection (abses_pullback grp_homo_id E) ==
projection E $o
{|
  grp_iso_homo :=
    grp_pullback_pr1 (projection E) grp_homo_id;
  isequiv_group_iso :=
    isequiv_pr1
      (fun b : E =>
       {c : B & projection E b = grp_homo_id c})
|}
  intros [a [p q]]; cbn.
H: Univalence
A, B: AbGroup
E: AbSES B A
a: E
p: B
q: projection E a = grp_homo_id p
p = projection E a
  exact q^.
Defined.

Definition abses_pullback_pmap_id `{Univalence} {A B : AbGroup}
  : abses_pullback_pmap (A:=A) (@grp_homo_id B) ==* pmap_idmap.
H: Univalence
A, B: AbGroup
abses_pullback_pmap grp_homo_id ==* pmap_idmap
Proof.
H: Univalence
A, B: AbGroup
abses_pullback_pmap grp_homo_id ==* pmap_idmap
  srapply Build_pHomotopy.
H: Univalence
A, B: AbGroup
abses_pullback_pmap grp_homo_id == pmap_idmap
H: Univalence
A, B: AbGroup
?p pt =
dpoint_eq (abses_pullback_pmap grp_homo_id) @
(dpoint_eq pmap_idmap)^
  1: exact abses_pullback_id.
H: Univalence
A, B: AbGroup
abses_pullback_id pt =
dpoint_eq (abses_pullback_pmap grp_homo_id) @
(dpoint_eq pmap_idmap)^
  refine (_ @ (concat_p1 _)^).
H: Univalence
A, B: AbGroup
abses_pullback_id pt =
dpoint_eq (abses_pullback_pmap grp_homo_id)
  napply (ap equiv_path_abses_iso).
H: Univalence
A, B: AbGroup
({|
   grp_iso_homo :=
     grp_pullback_pr1 (projection pt) grp_homo_id;
   isequiv_group_iso :=
     isequiv_pr1
       (fun b : pt =>
        {c : B & projection pt b = grp_homo_id c})
 |};
(fun x0 : A => 1,
fun x : abses_pullback grp_homo_id pt => ((x.2).2)^)) =
bp_pointed (abses_pullback' grp_homo_id)
  apply path_sigma_hprop.
H: Univalence
A, B: AbGroup
({|
   grp_iso_homo :=
     grp_pullback_pr1 (projection pt) grp_homo_id;
   isequiv_group_iso :=
     isequiv_pr1
       (fun b : pt =>
        {c : B & projection pt b = grp_homo_id c})
 |};
(fun x0 : A => 1,
fun x : abses_pullback grp_homo_id pt => ((x.2).2)^)).1 =
(bp_pointed (abses_pullback' grp_homo_id)).1
  apply equiv_path_groupisomorphism.
H: Univalence
A, B: AbGroup
({|
   grp_iso_homo :=
     grp_pullback_pr1 (projection pt) grp_homo_id;
   isequiv_group_iso :=
     isequiv_pr1
       (fun b : pt =>
        {c : B & projection pt b = grp_homo_id c})
 |};
(fun x0 : A => 1,
fun x : abses_pullback grp_homo_id pt => ((x.2).2)^)).1 ==
(bp_pointed (abses_pullback' grp_homo_id)).1
  intros [[a b] [b' p]]; cbn; cbn in p.
H: Univalence
A, B: AbGroup
a: A
b, b': B
p: b = b'
(a, b) = (a, b')
  by apply path_prod'.
Defined.

Definition abses_pullback_compose' {A B0 B1 B2 : AbGroup@{u}}
  (f : B0 $-> B1) (g : B1 $-> B2)
  : abses_pullback (A:=A) f o abses_pullback g $=> abses_pullback (g $o f).
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
abses_pullback f o abses_pullback g $=>
abses_pullback (g $o f)
Proof.
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
abses_pullback f o abses_pullback g $=>
abses_pullback (g $o f)
  intro E; srefine (_; (_,_)).
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
E: AbSES B2 A
GroupIsomorphism
  (abses_pullback f (abses_pullback g E))
  (abses_pullback (g $o f) E)
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
E: AbSES B2 A
?proj1 $o
inclusion (abses_pullback f (abses_pullback g E)) ==
inclusion (abses_pullback (g $o f) E)
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
E: AbSES B2 A
projection (abses_pullback f (abses_pullback g E)) ==
projection (abses_pullback (g $o f) E) $o ?proj1
  -
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
E: AbSES B2 A
GroupIsomorphism
  (abses_pullback f (abses_pullback g E))
  (abses_pullback (g $o f) E) apply equiv_grp_pullback_compose_r.
  -
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
E: AbSES B2 A
equiv_grp_pullback_compose_r (projection E) f g $o
inclusion (abses_pullback f (abses_pullback g E)) ==
inclusion (abses_pullback (g $o f) E) intro a.
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
E: AbSES B2 A
a: A
(equiv_grp_pullback_compose_r (projection E) f g $o
 inclusion (abses_pullback f (abses_pullback g E))) a =
inclusion (abses_pullback (g $o f) E) a
    by srapply equiv_path_pullback_hset.
  -
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
E: AbSES B2 A
projection (abses_pullback f (abses_pullback g E)) ==
projection (abses_pullback (g $o f) E) $o
equiv_grp_pullback_compose_r (projection E) f g reflexivity.
Defined.

(** The analog of [abses_pullback_compose'] with actual homotopies. *)
Definition abses_pullback_compose `{Univalence}
  {A B0 B1 B2 : AbGroup@{u}} (f : B0 $-> B1) (g : B1 $-> B2)
  : abses_pullback (A:=A) f o abses_pullback g == abses_pullback (g $o f)
  := fun x => equiv_path_abses_iso (abses_pullback_compose' f g x).

(** We now work towards *pointed* composition of pullback ([abses_pullback_pcompose]). The proof of pointedness will matter when we later prove that pulling back along a short exact sequence is exact (i.e. that the complex [iscomplex_pullback_abses] below is exact). For this reason we carefully construct the proof of pointedness in terms of the analog [abses_pullback_pcompose'] on path data, which computes. *)

Definition abses_pullback_pcompose' {B0 B1 B2 A : AbGroup}
  (f : B0 $-> B1) (g : B1 $-> B2)
  : abses_pullback' f $o* abses_pullback' g $=>* abses_pullback' (A:=A) (g $o f).
B0, B1, B2, A: AbGroup
f: B0 $-> B1
g: B1 $-> B2
abses_pullback' f $o* abses_pullback' g $=>*
abses_pullback' (g $o f)
Proof.
B0, B1, B2, A: AbGroup
f: B0 $-> B1
g: B1 $-> B2
abses_pullback' f $o* abses_pullback' g $=>*
abses_pullback' (g $o f)
  exists (abses_pullback_compose' f g).
B0, B1, B2, A: AbGroup
f: B0 $-> B1
g: B1 $-> B2
abses_pullback_compose' f g pt $==
bp_pointed (abses_pullback' f $o* abses_pullback' g) $@
(bp_pointed (abses_pullback' (g $o f)))^$
  intros [[[a b2] [b1 c]] [b0 c']]; cbn in c, c'.
B0, B1, B2, A: AbGroup
f: B0 $-> B1
g: B1 $-> B2
a: A
b2: B2
b1: B1
c: b2 = g b1
b0: B0
c': b1 = f b0
(abses_pullback_compose' f g pt).1
  (((a, b2); b1; c); b0; c') =
(bp_pointed (abses_pullback' f $o* abses_pullback' g) $@
 (bp_pointed (abses_pullback' (g $o f)))^$).1
  (((a, b2); b1; c); b0; c')
  srapply equiv_path_pullback_hset; split; cbn.
B0, B1, B2, A: AbGroup
f: B0 $-> B1
g: B1 $-> B2
a: A
b2: B2
b1: B1
c: b2 = g b1
b0: B0
c': b1 = f b0
(a, b2) = (a, g (f b0))
B0, B1, B2, A: AbGroup
f: B0 $-> B1
g: B1 $-> B2
a: A
b2: B2
b1: B1
c: b2 = g b1
b0: B0
c': b1 = f b0
b0 = b0
  2: reflexivity.
B0, B1, B2, A: AbGroup
f: B0 $-> B1
g: B1 $-> B2
a: A
b2: B2
b1: B1
c: b2 = g b1
b0: B0
c': b1 = f b0
(a, b2) = (a, g (f b0))
  exact (path_prod' idpath (c @ ap g c')).
Defined.

Definition abses_pullback_pcompose `{Univalence} {A B0 B1 B2 : AbGroup}
  (f : B0 $-> B1) (g : B1 $-> B2)
  : abses_pullback_pmap (A:=A) f o* abses_pullback_pmap g ==* abses_pullback_pmap (g $o f).
H: Univalence
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
abses_pullback_pmap f o* abses_pullback_pmap g ==*
abses_pullback_pmap (g $o f)
Proof.
H: Univalence
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
abses_pullback_pmap f o* abses_pullback_pmap g ==*
abses_pullback_pmap (g $o f)
  refine (to_pointed_compose _ _ @* _).
H: Univalence
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
to_pointed (abses_pullback' f $o* abses_pullback' g) ==*
abses_pullback_pmap (g $o f)
  apply equiv_ptransformation_phomotopy.
H: Univalence
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
abses_pullback' f $o* abses_pullback' g $=>*
abses_pullback' (g $o f)
  apply abses_pullback_pcompose'.
Defined.

(** *** Pulling back along constant maps *)

Lemma abses_pullback_const' {A B B' : AbGroup}
  : const pt $=> (@abses_pullback A B B' grp_homo_const).
A, B, B': AbGroup
const pt $=> abses_pullback grp_homo_const
Proof.
A, B, B': AbGroup
const pt $=> abses_pullback grp_homo_const
  intro E.
A, B, B': AbGroup
E: AbSES B A
const pt E $-> abses_pullback grp_homo_const E
  simpl.
A, B, B': AbGroup
E: AbSES B A
abses_path_data_iso (const pt E)
  (abses_pullback grp_homo_const E)
  napply abses_path_data_to_iso.
A, B, B': AbGroup
E: AbSES B A
abses_path_data (const pt E)
  (abses_pullback grp_homo_const E)
  srefine (_;(_,_)); cbn.
A, B, B': AbGroup
E: AbSES B A
GroupHomomorphism (grp_prod A B')
  (grp_pullback (projection E)
     (grp_homo_compose (grp_trivial_rec B)
        (grp_trivial_corec B')))
A, B, B': AbGroup
E: AbSES B A
(fun x : A => ?Goal (x, group_unit)) ==
(fun x : A =>
 (inclusion E x; group_unit;
 cx_isexact x @
 (grp_homo_unit
    (grp_homo_compose (grp_trivial_rec B)
       (grp_trivial_corec B')))^))
A, B, B': AbGroup
E: AbSES B A
snd == (fun x : A * B' => pullback_pr2 (?Goal x))
  -
A, B, B': AbGroup
E: AbSES B A
GroupHomomorphism (grp_prod A B')
  (grp_pullback (projection E)
     (grp_homo_compose (grp_trivial_rec B)
        (grp_trivial_corec B'))) srapply grp_pullback_corec.
A, B, B': AbGroup
E: AbSES B A
grp_prod A B' $-> E
A, B, B': AbGroup
E: AbSES B A
grp_prod A B' $-> B'
A, B, B': AbGroup
E: AbSES B A
projection E o ?b ==
grp_homo_compose (grp_trivial_rec B)
  (grp_trivial_corec B') o ?c
    +
A, B, B': AbGroup
E: AbSES B A
grp_prod A B' $-> E exact (inclusion _ $o ab_biprod_pr1).
    +
A, B, B': AbGroup
E: AbSES B A
grp_prod A B' $-> B' exact ab_biprod_pr2.
    +
A, B, B': AbGroup
E: AbSES B A
projection E o (inclusion E $o ab_biprod_pr1) ==
grp_homo_compose (grp_trivial_rec B)
  (grp_trivial_corec B') o ab_biprod_pr2 intro x; cbn.
A, B, B': AbGroup
E: AbSES B A
x: grp_prod A B'
projection E (inclusion E (fst x)) = group_unit
      apply iscomplex_abses.
  -
A, B, B': AbGroup
E: AbSES B A
(fun x : A =>
 grp_pullback_corec (projection E)
   (grp_homo_compose (grp_trivial_rec B)
      (grp_trivial_corec B'))
   (inclusion E $o ab_biprod_pr1) ab_biprod_pr2
   ((fun x0 : grp_prod A B' =>
     (let X :=
        fun E : AbSES' B A =>
        pointed_fun (iscomplex_abses E) in
      X E (fst x0))
     :
     projection E ((inclusion E $o ab_biprod_pr1) x0) =
     grp_homo_compose (grp_trivial_rec B)
       (grp_trivial_corec B') (ab_biprod_pr2 x0))
    :
    projection E o (inclusion E $o ab_biprod_pr1) ==
    grp_homo_compose (grp_trivial_rec B)
      (grp_trivial_corec B') o ab_biprod_pr2)
   (x, group_unit)) ==
(fun x : A =>
 (inclusion E x; group_unit;
 cx_isexact x @
 (grp_homo_unit
    (grp_homo_compose (grp_trivial_rec B)
       (grp_trivial_corec B')))^)) intro a; cbn.
A, B, B': AbGroup
E: AbSES B A
a: A
(inclusion E a; group_unit; iscomplex_abses E a) =
(inclusion E a; group_unit;
cx_isexact a @
(grp_homo_unit
   (grp_homo_compose (grp_trivial_rec B)
      (grp_trivial_corec B')))^)
    by srapply equiv_path_pullback_hset; split.
  -
A, B, B': AbGroup
E: AbSES B A
snd ==
(fun x : A * B' =>
 pullback_pr2
   (grp_pullback_corec (projection E)
      (grp_homo_compose (grp_trivial_rec B)
         (grp_trivial_corec B'))
      (inclusion E $o ab_biprod_pr1) ab_biprod_pr2
      ((fun x0 : grp_prod A B' =>
        (let X :=
           fun E : AbSES' B A =>
           pointed_fun (iscomplex_abses E) in
         X E (fst x0))
        :
        projection E
          ((inclusion E $o ab_biprod_pr1) x0) =
        grp_homo_compose (grp_trivial_rec B)
          (grp_trivial_corec B') (ab_biprod_pr2 x0))
       :
       projection E o (inclusion E $o ab_biprod_pr1) ==
       grp_homo_compose (grp_trivial_rec B)
         (grp_trivial_corec B') o ab_biprod_pr2) x)) reflexivity.
Defined.

Definition abses_pullback_const `{Univalence} {A B B' : AbGroup}
  : const pt == @abses_pullback A B B' grp_homo_const
  := fun x => (equiv_path_abses_iso (abses_pullback_const' x)).

Lemma abses_pullback_pconst' {A B B' : AbGroup}
  : @pmap_abses_const B' A B A $=>* abses_pullback' grp_homo_const.
A, B, B': AbGroup
pmap_abses_const $=>* abses_pullback' grp_homo_const
Proof.
A, B, B': AbGroup
pmap_abses_const $=>* abses_pullback' grp_homo_const
  srefine (_; _).
A, B, B': AbGroup
pmap_abses_const $=> abses_pullback' grp_homo_const
A, B, B': AbGroup
(fun
   eta : pmap_abses_const $=>
         abses_pullback' grp_homo_const =>
 eta pt $==
 bp_pointed pmap_abses_const $@
 (bp_pointed (abses_pullback' grp_homo_const))^$)
  ?proj1
  1: rapply abses_pullback_const'.
A, B, B': AbGroup
(fun
   eta : pmap_abses_const $=>
         abses_pullback' grp_homo_const =>
 eta pt $==
 bp_pointed pmap_abses_const $@
 (bp_pointed (abses_pullback' grp_homo_const))^$)
  abses_pullback_const'
  lazy beta.
A, B, B': AbGroup
abses_pullback_const' pt $==
bp_pointed pmap_abses_const $@
(bp_pointed (abses_pullback' grp_homo_const))^$
  intro x; reflexivity.
Defined.

Definition abses_pullback_pconst `{Univalence} {A B B' : AbGroup}
  : pconst ==* @abses_pullback_pmap _ A B B' grp_homo_const.
H: Univalence
A, B, B': AbGroup
pconst ==* abses_pullback_pmap grp_homo_const
Proof.
H: Univalence
A, B, B': AbGroup
pconst ==* abses_pullback_pmap grp_homo_const
  refine (pmap_abses_const_to_pointed @* _).
H: Univalence
A, B, B': AbGroup
to_pointed pmap_abses_const ==*
abses_pullback_pmap grp_homo_const
  rapply equiv_ptransformation_phomotopy.
H: Univalence
A, B, B': AbGroup
pmap_abses_const $=>* abses_pullback' grp_homo_const
  exact abses_pullback_pconst'.
Defined.

(** *** Pulling [E] back along [projection E] is trivial *)

Definition abses_pullback_projection_morphism {B A : AbGroup} (E : AbSES B A)
  : AbSESMorphism (pt : AbSES E A) E.
B, A: AbGroup
E: AbSES B A
AbSESMorphism (pt : AbSES E A) E
Proof.
B, A: AbGroup
E: AbSES B A
AbSESMorphism (pt : AbSES E A) E
  srapply (Build_AbSESMorphism grp_homo_id _ (projection E)).
B, A: AbGroup
E: AbSES B A
pt $-> E
B, A: AbGroup
E: AbSES B A
inclusion E $o grp_homo_id ==
?component2 $o inclusion pt
B, A: AbGroup
E: AbSES B A
projection E $o ?component2 ==
projection E $o projection pt
  -
B, A: AbGroup
E: AbSES B A
pt $-> E cbn.
B, A: AbGroup
E: AbSES B A
GroupHomomorphism (grp_prod A E) E exact (ab_biprod_rec (inclusion E) grp_homo_id).
  -
B, A: AbGroup
E: AbSES B A
inclusion E $o grp_homo_id ==
(ab_biprod_rec (inclusion E) grp_homo_id : pt $-> E) $o
inclusion pt intro x; cbn.
B, A: AbGroup
E: AbSES B A
x: A
inclusion E x = sg_op (inclusion E x) group_unit
    exact (right_identity _)^.
  -
B, A: AbGroup
E: AbSES B A
projection E $o
(ab_biprod_rec (inclusion E) grp_homo_id : pt $-> E) ==
projection E $o projection pt intros [a e]; cbn.
B, A: AbGroup
E: AbSES B A
a: A
e: E
projection E (sg_op (inclusion E a) e) =
projection E e
    refine (grp_homo_op _ _ _ @ _).
B, A: AbGroup
E: AbSES B A
a: A
e: E
sg_op (projection E (inclusion E a)) (projection E e) =
projection E e
    refine (ap (fun x => sg_op x _) _ @ _).
B, A: AbGroup
E: AbSES B A
a: A
e: E
projection E (inclusion E a) = ?Goal
B, A: AbGroup
E: AbSES B A
a: A
e: E
sg_op ?Goal (projection E e) = projection E e
    1: apply isexact_inclusion_projection.
B, A: AbGroup
E: AbSES B A
a: A
e: E
sg_op (pconst a) (projection E e) = projection E e
    apply left_identity.
Defined.

Definition abses_pullback_projection `{Univalence} {B A : AbGroup} (E : AbSES B A)
  : pt = abses_pullback (projection E) E
  := abses_pullback_component1_id
       (abses_pullback_projection_morphism E) (fun _ => idpath).

(** *** Pulling back along homotopic maps *)

Lemma abses_pullback_homotopic' {A B B' : AbGroup}
  (f f' : B $-> B') (h : f == f')
  : abses_pullback (A:=A) f $=> abses_pullback f'.
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
abses_pullback f $=> abses_pullback f'
Proof.
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
abses_pullback f $=> abses_pullback f'
  intro E.
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
E: AbSES B' A
abses_pullback f E $-> abses_pullback f' E
  srefine (_; (_, _)).
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
E: AbSES B' A
GroupIsomorphism (abses_pullback f E)
  (abses_pullback f' E)
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
E: AbSES B' A
?proj1 $o inclusion (abses_pullback f E) ==
inclusion (abses_pullback f' E)
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
E: AbSES B' A
projection (abses_pullback f E) ==
projection (abses_pullback f' E) $o ?proj1
  -
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
E: AbSES B' A
GroupIsomorphism (abses_pullback f E)
  (abses_pullback f' E) srapply equiv_functor_grp_pullback.
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
E: AbSES B' A
GroupIsomorphism B' B'
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
E: AbSES B' A
GroupIsomorphism E E
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
E: AbSES B' A
GroupIsomorphism B B
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
E: AbSES B' A
projection E o ?beta == ?alpha o projection E
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
E: AbSES B' A
?alpha o f == f' o ?gamma
    1-3: exact grp_iso_id.
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
E: AbSES B' A
projection E o grp_iso_id == grp_iso_id o projection E
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
E: AbSES B' A
grp_iso_id o f == f' o grp_iso_id
    1: reflexivity.
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
E: AbSES B' A
grp_iso_id o f == f' o grp_iso_id
    exact h.
  -
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
E: AbSES B' A
equiv_functor_grp_pullback (projection E)
  (projection E) f f' grp_iso_id grp_iso_id grp_iso_id
  (fun x0 : E => 1) h $o
inclusion (abses_pullback f E) ==
inclusion (abses_pullback f' E) intro a; cbn.
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
E: AbSES B' A
a: A
(inclusion E a; group_unit;
(1 @ ap idmap (cx_isexact a @ (grp_homo_unit f)^)) @
h group_unit) =
(inclusion E a; group_unit;
cx_isexact a @ (grp_homo_unit f')^)
    by srapply equiv_path_pullback_hset; split.
  -
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
E: AbSES B' A
projection (abses_pullback f E) ==
projection (abses_pullback f' E) $o
equiv_functor_grp_pullback (projection E)
  (projection E) f f' grp_iso_id grp_iso_id grp_iso_id
  (fun x0 : E => 1) h reflexivity.
Defined.

Lemma abses_pullback_homotopic `{Univalence} {A B B' : AbGroup}
  (f f' : B $-> B') (h : f == f')
  : abses_pullback (A:=A) f == abses_pullback f'.
H: Univalence
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
abses_pullback f == abses_pullback f'
Proof.
H: Univalence
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
abses_pullback f == abses_pullback f'
  intro E.
H: Univalence
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
E: AbSES B' A
abses_pullback f E = abses_pullback f' E
  apply equiv_path_abses_iso.
H: Univalence
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
E: AbSES B' A
abses_path_data_iso (abses_pullback f E)
  (abses_pullback f' E)
  exact (abses_pullback_homotopic' _ _ h _).
Defined.

Lemma abses_pullback_phomotopic' {A B B' : AbGroup}
  (f f' : B $-> B') (h : f == f')
  : abses_pullback' (A:=A) f $=>* abses_pullback' f'.
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
abses_pullback' f $=>* abses_pullback' f'
Proof.
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
abses_pullback' f $=>* abses_pullback' f'
  exists (abses_pullback_homotopic' f f' h); cbn.
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
(fun x : Pullback snd f =>
 (pullback_pr1 x; pullback_pr2 x;
 (1 @ ap idmap (pullback_commsq snd f x)) @
 h (pullback_pr2 x))) ==
(fun x : Pullback snd f =>
 ((fst (pullback_pr1 x), f' (pullback_pr2 x));
 pullback_pr2 x; 1))
  intros [[a b'] [b c]]; cbn in c.
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
a: A
b': B'
b: B
c: b' = f b
(pullback_pr1 ((a, b'); b; c);
pullback_pr2 ((a, b'); b; c);
(1 @ ap idmap (pullback_commsq snd f ((a, b'); b; c))) @
h (pullback_pr2 ((a, b'); b; c))) =
((fst (pullback_pr1 ((a, b'); b; c)),
 f' (pullback_pr2 ((a, b'); b; c)));
pullback_pr2 ((a, b'); b; c); 1)
  srapply equiv_path_pullback_hset; split; cbn.
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
a: A
b': B'
b: B
c: b' = f b
(a, b') = (a, f' b)
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
a: A
b': B'
b: B
c: b' = f b
b = b
  2: reflexivity.
A, B, B': AbGroup
f, f': B $-> B'
h: f == f'
a: A
b': B'
b: B
c: b' = f b
(a, b') = (a, f' b)
  exact (path_prod' idpath (c @ h b)).
Defined.

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

(** *** Pulling back along a complex *)

Definition iscomplex_abses_pullback' {A B0 B1 B2 : AbGroup}
  (f : B0 $-> B1) (g : B1 $-> B2) (h : g $o f == grp_homo_const)
  : abses_pullback' f $o* abses_pullback' g $=>* @pmap_abses_const _ _ _ A.
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
h: g $o f == grp_homo_const
abses_pullback' f $o* abses_pullback' g $=>*
pmap_abses_const
Proof.
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
h: g $o f == grp_homo_const
abses_pullback' f $o* abses_pullback' g $=>*
pmap_abses_const
  refine (abses_pullback_pcompose' _ _ $@* _).
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
h: g $o f == grp_homo_const
abses_pullback' (g $o f) $=>* pmap_abses_const
  refine (abses_pullback_phomotopic' _ _ h $@* _).
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
h: g $o f == grp_homo_const
abses_pullback' grp_homo_const $=>* pmap_abses_const
  exact abses_pullback_pconst'^*$.
Defined.

Definition iscomplex_abses_pullback `{Univalence} {A B0 B1 B2 : AbGroup}
  (f : B0 $-> B1) (g : B1 $-> B2) (h : g $o f == grp_homo_const)
  : IsComplex (abses_pullback_pmap (A:=A) g) (abses_pullback_pmap f).
H: Univalence
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
h: g $o f == grp_homo_const
IsComplex (abses_pullback_pmap g)
  (abses_pullback_pmap f)
Proof.
H: Univalence
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
h: g $o f == grp_homo_const
IsComplex (abses_pullback_pmap g)
  (abses_pullback_pmap f)
  refine (_ @* _).
H: Univalence
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
h: g $o f == grp_homo_const
abses_pullback_pmap f o* abses_pullback_pmap g ==*
?Goal
H: Univalence
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
h: g $o f == grp_homo_const
?Goal ==* pconst
  2: symmetry; exact pmap_abses_const_to_pointed.
H: Univalence
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
h: g $o f == grp_homo_const
abses_pullback_pmap f o* abses_pullback_pmap g ==*
to_pointed pmap_abses_const
  refine (to_pointed_compose _ _ @* _).
H: Univalence
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
h: g $o f == grp_homo_const
to_pointed (abses_pullback' f $o* abses_pullback' g) ==*
to_pointed pmap_abses_const
  apply equiv_ptransformation_phomotopy.
H: Univalence
A, B0, B1, B2: AbGroup
f: B0 $-> B1
g: B1 $-> B2
h: g $o f == grp_homo_const
abses_pullback' f $o* abses_pullback' g $=>*
pmap_abses_const
  by rapply iscomplex_abses_pullback'.
Defined.

(** A consequence is that pulling back along a short exact sequence forms a complex. *)

Definition iscomplex_pullback_abses `{Univalence} {A B C : AbGroup} (E : AbSES C B)
  : IsComplex (abses_pullback_pmap (A:=A) (projection E)) (abses_pullback_pmap (inclusion E)).
H: Univalence
A, B, C: AbGroup
E: AbSES C B
IsComplex (abses_pullback_pmap (projection E))
  (abses_pullback_pmap (inclusion E))
Proof.
H: Univalence
A, B, C: AbGroup
E: AbSES C B
IsComplex (abses_pullback_pmap (projection E))
  (abses_pullback_pmap (inclusion E))
  rapply iscomplex_abses_pullback.
H: Univalence
A, B, C: AbGroup
E: AbSES C B
projection E $o inclusion E == grp_homo_const
  rapply iscomplex_abses.
Defined.

(** In fact, pulling back along a short exact sequence is (purely) exact. See [AbSES.PullbackFiberSequence]. *)

(** *** Fibers of pullback in terms of path data *)

Definition equiv_hfiber_abses `{Univalence} {X : Type} {A B : AbGroup}
  (f : X -> AbSES B A) (E : AbSES B A)
  : graph_hfiber f E <~> hfiber f E
  := equiv_functor_sigma_id (fun _ => equiv_path_abses_iso).

Definition hfiber_abses_path {A B B' : AbGroup} {f : B' $-> B} {X : AbSES B' A}
  (E F : graph_hfiber (abses_pullback f) X)
  := {p : E.1 $-> F.1 & (fmap (abses_pullback f) p)^$ $@ E.2 $-> F.2}.

Definition transport_path_data_hfiber_abses_pullback_l `{Univalence} {A B B' : AbGroup} {f : B' $-> B}
  {Y : AbSES B' A} {X0 : graph_hfiber (abses_pullback f) Y} {X1 : AbSES B A} (p : X0.1 = X1)
  : transport (fun x : AbSES B A => abses_pullback f x $== Y) p X0.2
    = fmap (abses_pullback f) (equiv_path_abses_iso^-1 p^) $@ X0.2.
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
X0: graph_hfiber (abses_pullback f) Y
X1: AbSES B A
p: X0.1 = X1
transport
  (fun x : AbSES B A => abses_pullback f x $== Y) p
  X0.2 =
fmap (abses_pullback f) (equiv_path_abses_iso^-1 p^) $@
X0.2
Proof.
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
X0: graph_hfiber (abses_pullback f) Y
X1: AbSES B A
p: X0.1 = X1
transport
  (fun x : AbSES B A => abses_pullback f x $== Y) p
  X0.2 =
fmap (abses_pullback f) (equiv_path_abses_iso^-1 p^) $@
X0.2
  induction p.
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
X0: graph_hfiber (abses_pullback f) Y
transport
  (fun x : AbSES B A => abses_pullback f x $== Y) 1
  X0.2 =
fmap (abses_pullback f) (equiv_path_abses_iso^-1 1^) $@
X0.2
  refine (transport_1 _ _ @ _).
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
X0: graph_hfiber (abses_pullback f) Y
X0.2 =
fmap (abses_pullback f) (equiv_path_abses_iso^-1 1^) $@
X0.2
  nrefine (_ @ (ap (fun x => x $@ _)) _).
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
X0: graph_hfiber (abses_pullback f) Y
X0.2 = ?Goal0 $@ X0.2
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
X0: graph_hfiber (abses_pullback f) Y
?Goal0 =
fmap (abses_pullback f) (equiv_path_abses_iso^-1 1^)
  2: {
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
X0: graph_hfiber (abses_pullback f) Y
?Goal0 =
fmap (abses_pullback f) (equiv_path_abses_iso^-1 1^) refine (_ @ ap _ equiv_path_absesV_1^).
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
X0: graph_hfiber (abses_pullback f) Y
?Goal0 = fmap (abses_pullback f) (Id X0.1)
       exact (fmap_id_strong _ _)^. }
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
X0: graph_hfiber (abses_pullback f) Y
X0.2 = Id (abses_pullback f X0.1) $@ X0.2
  exact (cat_idr_strong _)^.
Defined.

Definition equiv_hfiber_abses_pullback `{Univalence} {A B B' : AbGroup} {f : B' $-> B}
  (Y : AbSES B' A) (U V : graph_hfiber (abses_pullback f) Y)
  : hfiber_abses_path U V <~> U = V.
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
U, V: graph_hfiber (abses_pullback f) Y
hfiber_abses_path U V <~> U = V
Proof.
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
U, V: graph_hfiber (abses_pullback f) Y
hfiber_abses_path U V <~> U = V
  refine (equiv_path_sigma _ _ _ oE _).
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
U, V: graph_hfiber (abses_pullback f) Y
hfiber_abses_path U V <~>
{p : U.1 = V.1 &
transport
  (fun b : AbSES B A => abses_pullback f b $-> Y) p
  U.2 = V.2}
  srapply (equiv_functor_sigma' equiv_path_abses_iso);
    intro p; lazy beta.
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
U, V: graph_hfiber (abses_pullback f) Y
p: abses_path_data_iso U.1 V.1
((fmap (abses_pullback f) p)^$ $@ U.2 $-> V.2) <~>
transport
  (fun b : AbSES B A => abses_pullback f b $-> Y)
  (equiv_path_abses_iso p) U.2 = V.2
  refine (equiv_concat_l _ _ oE _).
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
U, V: graph_hfiber (abses_pullback f) Y
p: abses_path_data_iso U.1 V.1
transport
  (fun b : AbSES B A => abses_pullback f b $-> Y)
  (equiv_path_abses_iso p) U.2 = ?Goal
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
U, V: graph_hfiber (abses_pullback f) Y
p: abses_path_data_iso U.1 V.1
((fmap (abses_pullback f) p)^$ $@ U.2 $-> V.2) <~>
?Goal = V.2
  {
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
U, V: graph_hfiber (abses_pullback f) Y
p: abses_path_data_iso U.1 V.1
transport
  (fun b : AbSES B A => abses_pullback f b $-> Y)
  (equiv_path_abses_iso p) U.2 = ?Goal refine (transport_path_data_hfiber_abses_pullback_l _ @ _).
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
U, V: graph_hfiber (abses_pullback f) Y
p: abses_path_data_iso U.1 V.1
fmap (abses_pullback f)
  (equiv_path_abses_iso^-1 (equiv_path_abses_iso p)^) $@
U.2 = ?Goal
    refine (ap (fun x => (fmap (abses_pullback f) x) $@ _) _ @ _).
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
U, V: graph_hfiber (abses_pullback f) Y
p: abses_path_data_iso U.1 V.1
equiv_path_abses_iso^-1 (equiv_path_abses_iso p)^ =
?Goal1
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
U, V: graph_hfiber (abses_pullback f) Y
p: abses_path_data_iso U.1 V.1
fmap (abses_pullback f) ?Goal1 $@ U.2 = ?Goal
    {
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
U, V: graph_hfiber (abses_pullback f) Y
p: abses_path_data_iso U.1 V.1
equiv_path_abses_iso^-1 (equiv_path_abses_iso p)^ =
?Goal1 refine (ap _ (abses_path_data_V p) @ _).
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
U, V: graph_hfiber (abses_pullback f) Y
p: abses_path_data_iso U.1 V.1
equiv_path_abses_iso^-1
  (equiv_path_abses_iso (abses_path_data_inverse p)) =
?Goal1
      apply eissect. }
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
U, V: graph_hfiber (abses_pullback f) Y
p: abses_path_data_iso U.1 V.1
fmap (abses_pullback f) (abses_path_data_inverse p) $@
U.2 = ?Goal
    refine (ap (fun x => x $@ _) _).
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
U, V: graph_hfiber (abses_pullback f) Y
p: abses_path_data_iso U.1 V.1
fmap (abses_pullback f) (abses_path_data_inverse p) =
?Goal0
    tapply gpd_strong_1functor_V. }
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
U, V: graph_hfiber (abses_pullback f) Y
p: abses_path_data_iso U.1 V.1
((fmap (abses_pullback f) p)^$ $@ U.2 $-> V.2) <~>
(fmap (abses_pullback f) p)^$ $@ U.2 = V.2
  refine (equiv_path_sigma_hprop _ _ oE _).
H: Univalence
A, B, B': AbGroup
f: B' $-> B
Y: AbSES B' A
U, V: graph_hfiber (abses_pullback f) Y
p: abses_path_data_iso U.1 V.1
((fmap (abses_pullback f) p)^$ $@ U.2 $-> V.2) <~>
((fmap (abses_pullback f) p)^$ $@ U.2).1 = (V.2).1
  apply equiv_path_groupisomorphism.
Defined.

(** *** [AbSES] and [AbSES'] become contravariant functors in the first variable by pulling back *)

Instance is0functor_abses'10 {A : AbGroup}
  : Is0Functor (fun B : AbGroup^op => AbSES' B A).
A: AbGroup
Is0Functor (fun B : AbGroup^op => AbSES' B A)
Proof.
A: AbGroup
Is0Functor (fun B : AbGroup^op => AbSES' B A)
  apply Build_Is0Functor.
A: AbGroup
forall a b : AbGroup^op,
(a $-> b) -> AbSES' a A $-> AbSES' b A
  exact (fun _ _ f => abses_pullback f).
Defined.

Instance is1functor_abses'10 `{Univalence} {A : AbGroup}
  : Is1Functor (fun B : AbGroup^op => AbSES' B A).
H: Univalence
A: AbGroup
Is1Functor (fun B : AbGroup^op => AbSES' B A)
Proof.
H: Univalence
A: AbGroup
Is1Functor (fun B : AbGroup^op => AbSES' B A)
  apply Build_Is1Functor; intros; cbn.
H: Univalence
A: AbGroup
a, b: AbGroup^op
f, g: a $-> b
X: f $== g
abses_pullback f == abses_pullback g
H: Univalence
A: AbGroup
a: AbGroup^op
abses_pullback grp_homo_id == idmap
H: Univalence
A: AbGroup
a, b, c: AbGroup^op
f: a $-> b
g: b $-> c
abses_pullback (grp_homo_compose f g) ==
(fun x : AbSES' a A =>
 abses_pullback g (abses_pullback f x))
  -
H: Univalence
A: AbGroup
a, b: AbGroup^op
f, g: a $-> b
X: f $== g
abses_pullback f == abses_pullback g by apply abses_pullback_homotopic.
  -
H: Univalence
A: AbGroup
a: AbGroup^op
abses_pullback grp_homo_id == idmap exact abses_pullback_id.
  -
H: Univalence
A: AbGroup
a, b, c: AbGroup^op
f: a $-> b
g: b $-> c
abses_pullback (grp_homo_compose f g) ==
(fun x : AbSES' a A =>
 abses_pullback g (abses_pullback f x)) symmetry; apply abses_pullback_compose.
Defined.


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

Instance is1functor_abses10 `{Univalence} {A : AbGroup}
  : Is1Functor (fun B : AbGroup^op => AbSES B A).
H: Univalence
A: AbGroup
Is1Functor (fun B : AbGroup^op => AbSES B A)
Proof.
H: Univalence
A: AbGroup
Is1Functor (fun B : AbGroup^op => AbSES B A)
  apply Build_Is1Functor; intros; cbn.
H: Univalence
A: AbGroup
a, b: AbGroup^op
f, g: a $-> b
X: f $== g
abses_pullback_pmap f ==* abses_pullback_pmap g
H: Univalence
A: AbGroup
a: AbGroup^op
abses_pullback_pmap grp_homo_id ==* pmap_idmap
H: Univalence
A: AbGroup
a, b, c: AbGroup^op
f: a $-> b
g: b $-> c
abses_pullback_pmap (grp_homo_compose f g) ==*
abses_pullback_pmap g o* abses_pullback_pmap f
  -
H: Univalence
A: AbGroup
a, b: AbGroup^op
f, g: a $-> b
X: f $== g
abses_pullback_pmap f ==* abses_pullback_pmap g by apply abses_pullback_phomotopic.
  -
H: Univalence
A: AbGroup
a: AbGroup^op
abses_pullback_pmap grp_homo_id ==* pmap_idmap exact abses_pullback_pmap_id.
  -
H: Univalence
A: AbGroup
a, b, c: AbGroup^op
f: a $-> b
g: b $-> c
abses_pullback_pmap (grp_homo_compose f g) ==*
abses_pullback_pmap g o* abses_pullback_pmap f symmetry; apply abses_pullback_pcompose.
Defined.