HoTT.Algebra.AbSES.Pullback.v.alectryon.json

From HoTT Require Import Basics Types.From HoTT Require Import Basics Types.
From HoTT.WildCat Require Import Core NatTrans Universe Opposite.
Require Import HSet Limits.Pullback.
Require Import 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 x0 : E => (snd p.2 x0)^) (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 (projection pt) f)
                   (projection (abses_pullback f pt)) 
                   ((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
                 (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))).1 =
              ((a, b); b'; c).1,
             1
             :
             ((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))).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 (projection pt) f)
                   (projection (abses_pullback f pt)) 
                   ((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
                 (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))).1 =
              ((a, b); b'; c).1,
             1
             :
             ((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))).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 E0 : AbSES' B A => pointed_fun (iscomplex_abses E0) 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 E0 : AbSES' B A => pointed_fun (iscomplex_abses E0) 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.