PullbackFiberSequence.v

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

Local Open Scope pointed_scope.
Local Open Scope mc_scope.
Local Open Scope mc_add_scope.

(** * The fiber sequence induced by pulling back along a short exact sequence *)

(** We show that pulling back along a short exact sequence [E : AbSES C B] produces a fiber sequence [AbSES C A -> AbSES E A -> AbSES B A]. The associated long exact sequence of homotopy groups recovers the usual (contravariant) six-term exact sequence of Ext groups.

We will prove the analog of exactness in terms of path data, and deduce the usual notion. *)

(** If a short exact sequence [A -> F -> E] becomes trivial after pulling back along an inclusion [i : B -> E], then there is a "transpose" short exact sequence [B -> F -> F/B]. We begin by constructing the the map [B -> F]. *)
Definition abses_pullback_inclusion_transpose_map {A B E : AbGroup}
      (i : B $-> E) `{IsEmbedding i}
      (F : AbSES E A) (p : abses_pullback i F $== pt)
  : B $-> F
  := grp_pullback_pr1 _ _ $o p^$.1 $o ab_biprod_inr.

(** The comparison map [A + B $-> F] is an embedding.  This comes up twice so we factor it out as a lemma. *)
Local Instance abses_pullback_inclusion_lemma {A B E : AbGroup}
      (i : B $-> E) `{IsEmbedding i}
      (F : AbSES E A) (p : abses_pullback i F $== pt)
  : IsEmbedding (grp_pullback_pr1 _ _ $o p^$.1).A, B, E: AbGroup
i: B $-> E
IsEmbedding0: IsEmbedding i
F: AbSES E A
p: abses_pullback i F $== pt
IsEmbedding
  (grp_pullback_pr1 (projection F) i $o (p^$).1)
Proof.A, B, E: AbGroup
i: B $-> E
IsEmbedding0: IsEmbedding i
F: AbSES E A
p: abses_pullback i F $== pt
IsEmbedding
  (grp_pullback_pr1 (projection F) i $o (p^$).1)
  nrapply (istruncmap_compose (-1) p^$.1 (grp_pullback_pr1 (projection F) i)).A, B, E: AbGroup
i: B $-> E
IsEmbedding0: IsEmbedding i
F: AbSES E A
p: abses_pullback i F $== pt
IsEmbedding (grp_pullback_pr1 (projection F) i)
A, B, E: AbGroup
i: B $-> E
IsEmbedding0: IsEmbedding i
F: AbSES E A
p: abses_pullback i F $== pt
IsEmbedding (p^$).1
  all: rapply istruncmap_mapinO_tr.
Defined.

(** The map [B -> F] is an inclusion. *)
Local Instance abses_pullback_inclusion_transpose_embedding {A B E : AbGroup}
      (i : B $-> E) `{IsEmbedding i}
      (F : AbSES E A) (p : abses_pullback i F $== pt)
  : IsEmbedding (abses_pullback_inclusion_transpose_map i F p).A, B, E: AbGroup
i: B $-> E
IsEmbedding0: IsEmbedding i
F: AbSES E A
p: abses_pullback i F $== pt
IsEmbedding
  (abses_pullback_inclusion_transpose_map i F p)
Proof.A, B, E: AbGroup
i: B $-> E
IsEmbedding0: IsEmbedding i
F: AbSES E A
p: abses_pullback i F $== pt
IsEmbedding
  (abses_pullback_inclusion_transpose_map i F p)
  rapply (istruncmap_compose _ (ab_biprod_inr)).
Defined.

(** We define the cokernel [F/B], which is what we need below. *)
Definition abses_pullback_inclusion_transpose_endpoint' {A B E : AbGroup}
           (i : B $-> E) `{IsEmbedding i}
           (F : AbSES E A) (p : abses_pullback i F $== pt)
  : AbGroup
  := ab_cokernel_embedding (abses_pullback_inclusion_transpose_map i F p).

(** The composite map [B -> F -> E] is homotopic to the original inclusion [i : B -> E]. *)
Lemma abses_pullback_inclusion_transpose_beta {A B E : AbGroup}
      (i : B $-> E) `{IsEmbedding i}
      (F : AbSES E A) (p : abses_pullback i F $== pt)
  : projection F $o (abses_pullback_inclusion_transpose_map i F p) == i.A, B, E: AbGroup
i: B $-> E
IsEmbedding0: IsEmbedding i
F: AbSES E A
p: abses_pullback i F $== pt
projection F $o
abses_pullback_inclusion_transpose_map i F p == i
Proof.A, B, E: AbGroup
i: B $-> E
IsEmbedding0: IsEmbedding i
F: AbSES E A
p: abses_pullback i F $== pt
projection F $o
abses_pullback_inclusion_transpose_map i F p == i
  intro b.A, B, E: AbGroup
i: B $-> E
IsEmbedding0: IsEmbedding i
F: AbSES E A
p: abses_pullback i F $== pt
b: B
(projection F $o
 abses_pullback_inclusion_transpose_map i F p) b = 
i b
  change b with (ab_biprod_pr2 (A:=A) (mon_unit, b)).A, B, E: AbGroup
i: B $-> E
IsEmbedding0: IsEmbedding i
F: AbSES E A
p: abses_pullback i F $== pt
b: B
(projection F $o
 abses_pullback_inclusion_transpose_map i F p)
  (ab_biprod_pr2 (mon_unit, b)) =
i (ab_biprod_pr2 (mon_unit, b))
  refine (pullback_commsq _ _ _ @ ap i _).A, B, E: AbGroup
i: B $-> E
IsEmbedding0: IsEmbedding i
F: AbSES E A
p: abses_pullback i F $== pt
b: B
pullback_pr2
  ((p^$).1
     (ab_biprod_inr (ab_biprod_pr2 (mon_unit, b)))) =
ab_biprod_pr2 (mon_unit, b)
  exact (snd p^$.2 _)^.
Defined.

(** Short exact sequences in the fiber of [inclusion E] descend along [projection E]. *)
Definition abses_pullback_trivial_preimage `{Univalence} {A B C : AbGroup} (E : AbSES C B)
           (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt)
  : AbSES C A.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
AbSES C A
Proof.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
AbSES C A
  snrapply Build_AbSES.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
AbGroup
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
A $-> ?middle
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
?middle $-> C
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
IsEmbedding ?inclusion
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
IsConnMap (Tr (-1)) ?projection
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
IsExact (Tr (-1)) ?inclusion ?projection
  -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
AbGroup exact (abses_pullback_inclusion_transpose_endpoint' (inclusion E) F p).
  -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
A $->
abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p exact (grp_quotient_map $o inclusion F).
  -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p $-> C srapply (ab_cokernel_embedding_rec _ (projection E $o projection F)).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
grp_homo_compose (projection E $o projection F)
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p) $== grp_homo_const
    intro b.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
b: B
grp_homo_compose (projection E $o projection F)
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p) b = grp_homo_const b
    refine (ap (projection E) (abses_pullback_inclusion_transpose_beta (inclusion E) F p b) @ _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
b: B
projection E (inclusion E b) = grp_homo_const b
    apply iscomplex_abses.
  -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
IsEmbedding (grp_quotient_map $o inclusion F) apply isembedding_grouphomomorphism.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
forall a : A,
(grp_quotient_map $o inclusion F) a = group_unit ->
a = group_unit
    intros a q0.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
q0: (grp_quotient_map $o inclusion F) a = group_unit
a = group_unit
    (* Since [inclusion F a] is killed by [grp_quotient_map], its in the image of [B]. *)
    pose proof (in_coset := related_quotient_paths _ _ _ q0).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
q0: (grp_quotient_map $o inclusion F) a = group_unit
in_coset: in_cosetL
  {|
    normalsubgroup_subgroup :=
      grp_image_embedding
        (abses_pullback_inclusion_transpose_map
           (inclusion E) F p);
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup F
        (grp_image_embedding
           (abses_pullback_inclusion_transpose_map
              (inclusion E) F p))
  |} (inclusion F a) mon_unit
a = group_unit
    (* Cleaning up the context facilitates later steps. *)
    destruct in_coset as [b q1]; rewrite grp_unit_r in q1.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
q0: (grp_quotient_map $o inclusion F) a = group_unit
b: B
q1: abses_pullback_inclusion_transpose_map
  (inclusion E) F p b = 
- inclusion F a
a = group_unit
    (* Since both [inclusion F] and [B -> F] factor through the mono [ab_biprod A B -> F], we can lift [q1] to [ab_biprod A B]. *)
    assert (q2 : ab_biprod_inr  b = ab_biprod_inl (-a)).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
q0: (grp_quotient_map $o inclusion F) a = group_unit
b: B
q1: abses_pullback_inclusion_transpose_map
  (inclusion E) F p b = 
- inclusion F a
ab_biprod_inr b = ab_biprod_inl (- a)
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
q0: (grp_quotient_map $o inclusion F) a = group_unit
b: B
q1: abses_pullback_inclusion_transpose_map
  (inclusion E) F p b = 
- inclusion F a
q2: ab_biprod_inr b = ab_biprod_inl (- a)
a = group_unit
    1: {H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
q0: (grp_quotient_map $o inclusion F) a = group_unit
b: B
q1: abses_pullback_inclusion_transpose_map
  (inclusion E) F p b = 
- inclusion F a
ab_biprod_inr b = ab_biprod_inl (- a) apply (isinj_embedding (grp_pullback_pr1 _ _ $o p^$.1)).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
q0: (grp_quotient_map $o inclusion F) a = group_unit
b: B
q1: abses_pullback_inclusion_transpose_map
  (inclusion E) F p b = 
- inclusion F a
IsEmbedding
  (grp_pullback_pr1 (projection F) (inclusion E) $o
   (p^$).1)
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
q0: (grp_quotient_map $o inclusion F) a = group_unit
b: B
q1: abses_pullback_inclusion_transpose_map
  (inclusion E) F p b = 
- inclusion F a
(grp_pullback_pr1 (projection F) (inclusion E) $o
 (p^$).1) (ab_biprod_inr b) =
(grp_pullback_pr1 (projection F) (inclusion E) $o
 (p^$).1) (ab_biprod_inl (- a))
         -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
q0: (grp_quotient_map $o inclusion F) a = group_unit
b: B
q1: abses_pullback_inclusion_transpose_map
  (inclusion E) F p b = 
- inclusion F a
IsEmbedding
  (grp_pullback_pr1 (projection F) (inclusion E) $o
   (p^$).1) apply abses_pullback_inclusion_lemma.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
q0: (grp_quotient_map $o inclusion F) a = group_unit
b: B
q1: abses_pullback_inclusion_transpose_map
  (inclusion E) F p b = 
- inclusion F a
IsEmbedding (inclusion E) exact _.
         -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
q0: (grp_quotient_map $o inclusion F) a = group_unit
b: B
q1: abses_pullback_inclusion_transpose_map
  (inclusion E) F p b = 
- inclusion F a
(grp_pullback_pr1 (projection F) (inclusion E) $o
 (p^$).1) (ab_biprod_inr b) =
(grp_pullback_pr1 (projection F) (inclusion E) $o
 (p^$).1) (ab_biprod_inl (- a)) nrefine (q1 @ _); symmetry.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
q0: (grp_quotient_map $o inclusion F) a = group_unit
b: B
q1: abses_pullback_inclusion_transpose_map
  (inclusion E) F p b = 
- inclusion F a
(grp_pullback_pr1 (projection F) (inclusion E) $o
 (p^$).1) (ab_biprod_inl (- a)) = 
- inclusion F a
           refine (ap (grp_pullback_pr1 _ _) (fst p^$.2 (-a)) @ _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
q0: (grp_quotient_map $o inclusion F) a = group_unit
b: B
q1: abses_pullback_inclusion_transpose_map
  (inclusion E) F p b = 
- inclusion F a
grp_pullback_pr1 (projection F) 
  (inclusion E)
  (inclusion (abses_pullback (inclusion E) F) (- a)) =
- inclusion F a
           exact (grp_homo_inv _ _). }H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
q0: (grp_quotient_map $o inclusion F) a = group_unit
b: B
q1: abses_pullback_inclusion_transpose_map
  (inclusion E) F p b = 
- inclusion F a
q2: ab_biprod_inr b = ab_biprod_inl (- a)
a = group_unit
    (* Using [q2], we conclude. *)
    pose proof (q3 := ap negate (fst ((equiv_path_prod _ _)^-1 q2))); cbn in q3.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
q0: (grp_quotient_map $o inclusion F) a = group_unit
b: B
q1: abses_pullback_inclusion_transpose_map
  (inclusion E) F p b = 
- inclusion F a
q2: ab_biprod_inr b = ab_biprod_inl (- a)
q3: - group_unit = - - a
a = group_unit
    exact ((negate_involutive _)^ @ q3^ @ negate_mon_unit).
  -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
IsConnMap (Tr (-1))
  (ab_cokernel_embedding_rec
     (abses_pullback_inclusion_transpose_map
        (inclusion E) F p)
     (projection E $o projection F)
     ((fun b : B =>
       ap (projection E)
         (abses_pullback_inclusion_transpose_beta
            (inclusion E) F p b) @
       (let X :=
          fun E : AbSES' C B =>
          pointed_fun (iscomplex_abses E) in
        X E b))
      :
      grp_homo_compose 
        (projection E $o projection F)
        (abses_pullback_inclusion_transpose_map
           (inclusion E) F p) $== grp_homo_const)) apply (cancelR_conn_map (Tr (-1)) grp_quotient_map).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
IsConnMap (Tr (-1)) grp_quotient_map
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
IsConnMap (Tr (-1))
  (fun x : F =>
   ab_cokernel_embedding_rec
     (abses_pullback_inclusion_transpose_map
        (inclusion E) F p)
     (projection E $o projection F)
     (fun b : B =>
      ap (projection E)
        (abses_pullback_inclusion_transpose_beta
           (inclusion E) F p b) @
      (let X :=
         fun E : AbSES' C B =>
         pointed_fun (iscomplex_abses E) in
       X E b)) (grp_quotient_map x))
    1: exact _.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
IsConnMap (Tr (-1))
  (fun x : F =>
   ab_cokernel_embedding_rec
     (abses_pullback_inclusion_transpose_map
        (inclusion E) F p)
     (projection E $o projection F)
     (fun b : B =>
      ap (projection E)
        (abses_pullback_inclusion_transpose_beta
           (inclusion E) F p b) @
      (let X :=
         fun E : AbSES' C B =>
         pointed_fun (iscomplex_abses E) in
       X E b)) (grp_quotient_map x))
    simpl.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
IsConnMap (Tr (-1))
  (fun x : F => projection E (projection F x))
    exact _.
  -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
IsExact (Tr (-1)) (grp_quotient_map $o inclusion F)
  (ab_cokernel_embedding_rec
     (abses_pullback_inclusion_transpose_map
        (inclusion E) F p)
     (projection E $o projection F)
     ((fun b : B =>
       ap (projection E)
         (abses_pullback_inclusion_transpose_beta
            (inclusion E) F p b) @
       (let X :=
          fun E : AbSES' C B =>
          pointed_fun (iscomplex_abses E) in
        X E b))
      :
      grp_homo_compose 
        (projection E $o projection F)
        (abses_pullback_inclusion_transpose_map
           (inclusion E) F p) $== grp_homo_const)) snrapply Build_IsExact.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
IsComplex (grp_quotient_map $o inclusion F)
  (ab_cokernel_embedding_rec
     (abses_pullback_inclusion_transpose_map
        (inclusion E) F p)
     (projection E $o projection F)
     ((fun b : B =>
       ap (projection E)
         (abses_pullback_inclusion_transpose_beta
            (inclusion E) F p b) @
       (let X :=
          fun E : AbSES' C B =>
          pointed_fun (iscomplex_abses E) in
        X E b))
      :
      grp_homo_compose 
        (projection E $o projection F)
        (abses_pullback_inclusion_transpose_map
           (inclusion E) F p) $== grp_homo_const))
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
IsConnMap (Tr (-1)) (cxfib ?cx_isexact)
    +H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
IsComplex (grp_quotient_map $o inclusion F)
  (ab_cokernel_embedding_rec
     (abses_pullback_inclusion_transpose_map
        (inclusion E) F p)
     (projection E $o projection F)
     ((fun b : B =>
       ap (projection E)
         (abses_pullback_inclusion_transpose_beta
            (inclusion E) F p b) @
       (let X :=
          fun E : AbSES' C B =>
          pointed_fun (iscomplex_abses E) in
        X E b))
      :
      grp_homo_compose 
        (projection E $o projection F)
        (abses_pullback_inclusion_transpose_map
           (inclusion E) F p) $== grp_homo_const)) srapply phomotopy_homotopy_hset.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p) 
  (projection E $o projection F)
  ((fun b : B =>
    ap (projection E)
      (abses_pullback_inclusion_transpose_beta
         (inclusion E) F p b) @
    (let X :=
       fun E : AbSES' C B =>
       pointed_fun (iscomplex_abses E) in
     X E b))
   :
   grp_homo_compose (projection E $o projection F)
     (abses_pullback_inclusion_transpose_map
        (inclusion E) F p) $== grp_homo_const)
o* (grp_quotient_map $o inclusion F) == pconst
      intro a; simpl.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
projection E (projection F (inclusion F a)) = pt
      refine (ap (projection E) _ @ _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
projection F (inclusion F a) = ?Goal
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
projection E ?Goal = pt
      1: apply iscomplex_abses.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
projection E (pconst a) = pt
      apply grp_homo_unit.
    +H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
IsConnMap (Tr (-1))
  (cxfib
     (phomotopy_homotopy_hset
        ((fun a : A =>
          ap (projection E)
            (let X :=
               fun E0 : AbSES' E A =>
               pointed_fun (iscomplex_abses E0) in
             X F a) @ grp_homo_unit (projection E)
          :
          (ab_cokernel_embedding_rec
             (abses_pullback_inclusion_transpose_map
                (inclusion E) F p)
             (projection E $o projection F)
             (fun b : B =>
              ap (projection E)
                (abses_pullback_inclusion_transpose_beta
                   (inclusion E) F p b) @
              (let X :=
                 fun E : AbSES' C B =>
                 pointed_fun (iscomplex_abses E) in
               X E b))
           o* (grp_quotient_map $o inclusion F)) a =
          pconst a)
         :
         ab_cokernel_embedding_rec
           (abses_pullback_inclusion_transpose_map
              (inclusion E) F p)
           (projection E $o projection F)
           ((fun b : B =>
             ap (projection E)
               (abses_pullback_inclusion_transpose_beta
                  (inclusion E) F p b) @
             (let X :=
                fun E : AbSES' C B =>
                pointed_fun (iscomplex_abses E) in
              X E b))
            :
            grp_homo_compose
              (projection E $o projection F)
              (abses_pullback_inclusion_transpose_map
                 (inclusion E) F p) $== grp_homo_const)
         o* (grp_quotient_map $o inclusion F) ==
         pconst))) intros [y q].H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun a : A =>
            ap (projection E)
              (let X :=
                 fun E0 : AbSES' E A =>
                 pointed_fun (iscomplex_abses E0) in
               X F a) @ 
            grp_homo_unit (projection E)))) 
     (y; q))
      apply (@contr_inhabited_hprop _ _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun a : A =>
            ap (projection E)
              (let X :=
                 fun E0 : AbSES' E A =>
                 pointed_fun (iscomplex_abses E0) in
               X F a) @ 
            grp_homo_unit (projection E)))) 
     (y; q))
      (* We choose a preimage by [grp_quotient_map]. *)
      assert (f : merely (hfiber grp_quotient_map y)).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
merely (hfiber grp_quotient_map y)
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: merely (hfiber grp_quotient_map y)
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun a : A =>
            ap (projection E)
              (let X :=
                 fun E0 : AbSES' E A =>
                 pointed_fun (iscomplex_abses E0) in
               X F a) @ 
            grp_homo_unit (projection E)))) 
     (y; q))
      1: apply center, issurj_class_of.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: merely (hfiber grp_quotient_map y)
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun a : A =>
            ap (projection E)
              (let X :=
                 fun E0 : AbSES' E A =>
                 pointed_fun (iscomplex_abses E0) in
               X F a) @ 
            grp_homo_unit (projection E)))) 
     (y; q))
      revert_opaque f; apply Trunc_rec; intros [f q0].H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun a : A =>
            ap (projection E)
              (let X :=
                 fun E0 : AbSES' E A =>
                 pointed_fun (iscomplex_abses E0) in
               X F a) @ 
            grp_homo_unit (projection E)))) 
     (y; q))
      (* Since [projection F f] is in the kernel of [projection E], we find a preimage in [B]. *)
      assert (b : merely (hfiber (inclusion E) (projection F f))).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
merely (hfiber (inclusion E) (projection F f))
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: merely (hfiber (inclusion E) (projection F f))
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun a : A =>
            ap (projection E)
              (let X :=
                 fun E0 : AbSES' E A =>
                 pointed_fun (iscomplex_abses E0) in
               X F a) @ 
            grp_homo_unit (projection E)))) 
     (y; q))
      1: {H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
merely (hfiber (inclusion E) (projection F f)) rapply isexact_preimage.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
projection E (projection F f) = pt
           exact (ap _ q0 @ q). }H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: merely (hfiber (inclusion E) (projection F f))
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun a : A =>
            ap (projection E)
              (let X :=
                 fun E0 : AbSES' E A =>
                 pointed_fun (iscomplex_abses E0) in
               X F a) @ 
            grp_homo_unit (projection E)))) 
     (y; q))
      revert_opaque b; apply Trunc_rec; intros [b q1].H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun a : A =>
            ap (projection E)
              (let X :=
                 fun E0 : AbSES' E A =>
                 pointed_fun (iscomplex_abses E0) in
               X F a) @ 
            grp_homo_unit (projection E)))) 
     (y; q))
      (* The difference [f - b] in [F] is in the kernel of [projection F], hence lies in [A]. *)
      assert (a : merely (hfiber (inclusion F)
                                 (sg_op f (-(grp_pullback_pr1 _ _ (p^$.1 (ab_biprod_inr b))))))).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
merely
  (hfiber (inclusion F)
     (f +
      -
      grp_pullback_pr1 
        (projection F) 
        (inclusion E) ((p^$).1 (ab_biprod_inr b))))
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
a: merely
  (hfiber (inclusion F)
     (f +
      -
      grp_pullback_pr1 
        (projection F) 
        (inclusion E) ((p^$).1 (ab_biprod_inr b))))
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun a : A =>
            ap (projection E)
              (let X :=
                 fun E0 : AbSES' E A =>
                 pointed_fun (iscomplex_abses E0) in
               X F a) @ 
            grp_homo_unit (projection E)))) 
     (y; q))
      1: {H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
merely
  (hfiber (inclusion F)
     (f +
      -
      grp_pullback_pr1 
        (projection F) 
        (inclusion E) ((p^$).1 (ab_biprod_inr b)))) rapply isexact_preimage.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
projection F
  (f +
   -
   grp_pullback_pr1 (projection F) 
     (inclusion E) ((p^$).1 (ab_biprod_inr b))) = pt
           refine (grp_homo_op _ _ _ @ _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
projection F f +
projection F
  (-
   grp_pullback_pr1 (projection F) 
     (inclusion E) ((p^$).1 (ab_biprod_inr b))) = pt
           refine (ap (fun x => _ + x) (grp_homo_inv _ _) @ _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
projection F f +
-
projection F
  (grp_pullback_pr1 (projection F) 
     (inclusion E) ((p^$).1 (ab_biprod_inr b))) = pt
           refine (ap (fun x => _ - x) (abses_pullback_inclusion_transpose_beta (inclusion E) F p b @ q1) @ _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
projection F f - projection F f = pt
           apply right_inverse. }H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
a: merely
  (hfiber (inclusion F)
     (f +
      -
      grp_pullback_pr1 
        (projection F) 
        (inclusion E) ((p^$).1 (ab_biprod_inr b))))
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun a : A =>
            ap (projection E)
              (let X :=
                 fun E0 : AbSES' E A =>
                 pointed_fun (iscomplex_abses E0) in
               X F a) @ 
            grp_homo_unit (projection E)))) 
     (y; q))
      revert_opaque a; apply Trunc_rec; intros [a q2].H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
a: A
q2: inclusion F a =
f +
-
grp_pullback_pr1 (projection F) 
  (inclusion E) ((p^$).1 (ab_biprod_inr b))
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun a : A =>
            ap (projection E)
              (let X :=
                 fun E0 : AbSES' E A =>
                 pointed_fun (iscomplex_abses E0) in
               X F a) @ 
            grp_homo_unit (projection E)))) 
     (y; q))
      (* It remains to show that [a] is the desired preimage. *)
      refine (tr (a; _)).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
a: A
q2: inclusion F a =
f +
-
grp_pullback_pr1 (projection F) 
  (inclusion E) ((p^$).1 (ab_biprod_inr b))
cxfib
  (phomotopy_homotopy_hset
     (fun a : A =>
      ap (projection E)
        (let X :=
           fun E0 : AbSES' E A =>
           pointed_fun (iscomplex_abses E0) in
         X F a) @ grp_homo_unit (projection E))) a =
(y; q)
      let T := type of y in apply (@path_sigma_hprop T).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
a: A
q2: inclusion F a =
f +
-
grp_pullback_pr1 (projection F) 
  (inclusion E) ((p^$).1 (ab_biprod_inr b))
forall
x : abses_pullback_inclusion_transpose_endpoint'
      (inclusion E) F p,
IsHProp
  (ab_cokernel_embedding_rec
     (abses_pullback_inclusion_transpose_map
        (inclusion E) F p)
     (projection E $o projection F)
     (fun b : B =>
      ap (projection E)
        (abses_pullback_inclusion_transpose_beta
           (inclusion E) F p b) @
      (let X :=
         fun E : AbSES' C B =>
         pointed_fun (iscomplex_abses E) in
       X E b)) x = pt)
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
a: A
q2: inclusion F a =
f +
-
grp_pullback_pr1 (projection F) 
  (inclusion E) ((p^$).1 (ab_biprod_inr b))
(cxfib
   (phomotopy_homotopy_hset
      (fun a : A =>
       ap (projection E)
         (let X :=
            fun E0 : AbSES' E A =>
            pointed_fun (iscomplex_abses E0) in
          X F a) @ grp_homo_unit (projection E))) a).1 =
(y; q).1
      1: intros ?; apply istrunc_paths; apply group_isgroup.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
a: A
q2: inclusion F a =
f +
-
grp_pullback_pr1 (projection F) 
  (inclusion E) ((p^$).1 (ab_biprod_inr b))
(cxfib
   (phomotopy_homotopy_hset
      (fun a : A =>
       ap (projection E)
         (let X :=
            fun E0 : AbSES' E A =>
            pointed_fun (iscomplex_abses E0) in
          X F a) @ grp_homo_unit (projection E))) a).1 =
(y; q).1
      refine (ap grp_quotient_map q2 @ _ @ q0).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
a: A
q2: inclusion F a =
f +
-
grp_pullback_pr1 (projection F) 
  (inclusion E) ((p^$).1 (ab_biprod_inr b))
grp_quotient_map
  (f +
   -
   grp_pullback_pr1 (projection F) 
     (inclusion E) ((p^$).1 (ab_biprod_inr b))) =
grp_quotient_map f
      refine (grp_homo_op _ _ _ @ _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
a: A
q2: inclusion F a =
f +
-
grp_pullback_pr1 (projection F) 
  (inclusion E) ((p^$).1 (ab_biprod_inr b))
grp_quotient_map f +
grp_quotient_map
  (-
   grp_pullback_pr1 (projection F) 
     (inclusion E) ((p^$).1 (ab_biprod_inr b))) =
grp_quotient_map f
      apply grp_moveR_Mg.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
a: A
q2: inclusion F a =
f +
-
grp_pullback_pr1 (projection F) 
  (inclusion E) ((p^$).1 (ab_biprod_inr b))
grp_quotient_map
  (-
   grp_pullback_pr1 (projection F) 
     (inclusion E) ((p^$).1 (ab_biprod_inr b))) =
- grp_quotient_map f + grp_quotient_map f
      refine (_ @ (left_inverse _)^).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
a: A
q2: inclusion F a =
f +
-
grp_pullback_pr1 (projection F) 
  (inclusion E) ((p^$).1 (ab_biprod_inr b))
grp_quotient_map
  (-
   grp_pullback_pr1 (projection F) 
     (inclusion E) ((p^$).1 (ab_biprod_inr b))) =
congquot_mon_unit
      apply qglue.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
a: A
q2: inclusion F a =
f +
-
grp_pullback_pr1 (projection F) 
  (inclusion E) ((p^$).1 (ab_biprod_inr b))
in_cosetL
  {|
    normalsubgroup_subgroup :=
      grp_image_embedding
        (abses_pullback_inclusion_transpose_map
           (inclusion E) F p);
    normalsubgroup_isnormal :=
      isnormal_ab_subgroup F
        (grp_image_embedding
           (abses_pullback_inclusion_transpose_map
              (inclusion E) F p))
  |}
  (-
   grp_pullback_pr1 (projection F) 
     (inclusion E) ((p^$).1 (ab_biprod_inr b)))
  mon_unit
      exists b.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
a: A
q2: inclusion F a =
f +
-
grp_pullback_pr1 (projection F) 
  (inclusion E) ((p^$).1 (ab_biprod_inr b))
abses_pullback_inclusion_transpose_map 
  (inclusion E) F p b =
-
-
grp_pullback_pr1 (projection F) 
  (inclusion E) ((p^$).1 (ab_biprod_inr b)) + mon_unit
      refine (_ @ (grp_unit_r _)^).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
y: abses_pullback_inclusion_transpose_endpoint'
  (inclusion E) F p
q: ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (projection E $o projection F)
  (fun b : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta
        (inclusion E) F p b) @
   (let X :=
      fun E : AbSES' C B =>
      pointed_fun (iscomplex_abses E) in
    X E b)) y = pt
f: F
q0: grp_quotient_map f = y
b: B
q1: inclusion E b = projection F f
a: A
q2: inclusion F a =
f +
-
grp_pullback_pr1 (projection F) 
  (inclusion E) ((p^$).1 (ab_biprod_inr b))
abses_pullback_inclusion_transpose_map 
  (inclusion E) F p b =
-
-
grp_pullback_pr1 (projection F) 
  (inclusion E) ((p^$).1 (ab_biprod_inr b))
      exact (negate_involutive _)^.
Defined.

(** That [abses_pullback_trivial_preimage E F p] pulls back to [F] is immediate from [abses_pullback_component1_id] and the following map. As such, we've shown that sequences which become trivial after pulling back along [inclusion E] are in the image of pullback along [projection E]. *)

Definition abses_pullback_inclusion0_map' `{Univalence} {A B C : AbGroup} (E : AbSES C B)
           (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt)
  : AbSESMorphism F (abses_pullback_trivial_preimage E F p).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
AbSESMorphism F
  (abses_pullback_trivial_preimage E F p)
Proof.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
AbSESMorphism F
  (abses_pullback_trivial_preimage E F p)
  srapply Build_AbSESMorphism.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
A $-> A
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
F $-> abses_pullback_trivial_preimage E F p
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
E $-> C
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
inclusion (abses_pullback_trivial_preimage E F p) $o
?component1 == ?component2 $o inclusion F
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
projection (abses_pullback_trivial_preimage E F p) $o
?component2 == ?component3 $o projection F
  -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
A $-> A exact grp_homo_id.
  -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
F $-> abses_pullback_trivial_preimage E F p exact grp_quotient_map.
  -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
E $-> C exact (projection E).
  -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
inclusion (abses_pullback_trivial_preimage E F p) $o
grp_homo_id == grp_quotient_map $o inclusion F reflexivity.
  -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
projection (abses_pullback_trivial_preimage E F p) $o
grp_quotient_map == projection E $o projection F reflexivity.
Defined.

(** For exactness we need not only a preimage of [F] but a preimage of [(F,p)] along [cxfib]. We now define and prove this in terms of path data. *)

(** The analog of [cxfib] induced by pullback in terms of path data. *)
Definition cxfib' {A B C : AbGroup} (E : AbSES C B)
  : AbSES C A -> graph_hfiber (abses_pullback (A:=A) (inclusion E)) pt.A, B, C: AbGroup
E: AbSES C B
AbSES C A ->
graph_hfiber (abses_pullback (inclusion E)) pt
Proof.A, B, C: AbGroup
E: AbSES C B
AbSES C A ->
graph_hfiber (abses_pullback (inclusion E)) pt
  intro Y.A, B, C: AbGroup
E: AbSES C B
Y: AbSES C A
graph_hfiber (abses_pullback (inclusion E)) pt
  exists (abses_pullback (projection E) Y).A, B, C: AbGroup
E: AbSES C B
Y: AbSES C A
abses_pullback (inclusion E)
  (abses_pullback (projection E) Y) $-> pt
  refine (abses_pullback_compose' _ _ Y $@ _).A, B, C: AbGroup
E: AbSES C B
Y: AbSES C A
abses_pullback (projection E $o inclusion E) Y $== pt
  refine (abses_pullback_homotopic' _ grp_homo_const _ Y $@ _).A, B, C: AbGroup
E: AbSES C B
Y: AbSES C A
projection E $o inclusion E == grp_homo_const
A, B, C: AbGroup
E: AbSES C B
Y: AbSES C A
abses_pullback grp_homo_const Y $== pt
  1: rapply iscomplex_abses.A, B, C: AbGroup
E: AbSES C B
Y: AbSES C A
abses_pullback grp_homo_const Y $== pt
  symmetry; apply abses_pullback_const'.
Defined.

Definition hfiber_cxfib' {A B C : AbGroup} (E : AbSES C B)
           (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt)
  := {Y : AbSES C A & hfiber_abses_path (cxfib' E Y) (F; p)}.

(* This is just [idpath], but Coq takes too long to see that. *)
Local Definition pr2_cxfib' `{Univalence} {A B C : AbGroup} {E : AbSES C B} (U : AbSES C A)
  : equiv_ptransformation_phomotopy (iscomplex_abses_pullback' _ _ (iscomplex_abses E)) U
    = equiv_path_abses_iso (cxfib' E U).2.H: Univalence
A, B, C: AbGroup
E: AbSES C B
U: AbSES C A
equiv_ptransformation_phomotopy
  (iscomplex_abses_pullback' (inclusion E)
     (projection E) (iscomplex_abses E)) U =
equiv_path_abses_iso (cxfib' E U).2
Proof.H: Univalence
A, B, C: AbGroup
E: AbSES C B
U: AbSES C A
equiv_ptransformation_phomotopy
  (iscomplex_abses_pullback' (inclusion E)
     (projection E) (iscomplex_abses E)) U =
equiv_path_abses_iso (cxfib' E U).2
  change (equiv_ptransformation_phomotopy (iscomplex_abses_pullback' _ _ (iscomplex_abses E)) U)
    with (equiv_path_abses_iso ((iscomplex_abses_pullback' _ _ (iscomplex_abses E)).1 U)).H: Univalence
A, B, C: AbGroup
E: AbSES C B
U: AbSES C A
equiv_path_abses_iso
  ((iscomplex_abses_pullback' (inclusion E)
      (projection E) (iscomplex_abses E)).1 U) =
equiv_path_abses_iso (cxfib' E U).2
  apply (ap equiv_path_abses_iso).H: Univalence
A, B, C: AbGroup
E: AbSES C B
U: AbSES C A
(iscomplex_abses_pullback' (inclusion E)
   (projection E) (iscomplex_abses E)).1 U =
(cxfib' E U).2
  rapply path_hom.H: Univalence
A, B, C: AbGroup
E: AbSES C B
U: AbSES C A
(iscomplex_abses_pullback' (inclusion E)
   (projection E) (iscomplex_abses E)).1 U $==
(cxfib' E U).2
  refine (_ $@R abses_pullback_compose' (inclusion E) (projection E) U);
    unfold trans_comp.H: Univalence
A, B, C: AbGroup
E: AbSES C B
U: AbSES C A
(abses_pullback_pconst' ^*$).1 U $o
(abses_pullback_phomotopic'
   (projection E $o inclusion E) grp_homo_const
   (iscomplex_abses E)).1 U $==
abses_pullback_homotopic'
  (projection E $o inclusion E) grp_homo_const
  (iscomplex_abses E) U $@
symmetric_GpdHom pt (abses_pullback grp_homo_const U)
  (abses_pullback_const' U)
  refine (_ $@R abses_pullback_homotopic' (projection E $o inclusion E) grp_homo_const (iscomplex_abses E) U).H: Univalence
A, B, C: AbGroup
E: AbSES C B
U: AbSES C A
(abses_pullback_pconst'.1 U)^$ $==
symmetric_GpdHom pt (abses_pullback grp_homo_const U)
  (abses_pullback_const' U)
  reflexivity.
Defined.

(** Making [abses_pullback'] opaque speeds up the following proof. *)
Opaque abses_pullback'.

Local Definition eq_cxfib_cxfib' `{Univalence} {A B C : AbGroup} {E : AbSES C B} (U : AbSES C A)
  : cxfib (iscomplex_pullback_abses E) U = equiv_hfiber_abses _ _ (cxfib' E U).H: Univalence
A, B, C: AbGroup
E: AbSES C B
U: AbSES C A
cxfib (iscomplex_pullback_abses E) U =
equiv_hfiber_abses (abses_pullback (inclusion E)) pt
  (cxfib' E U)
Proof.H: Univalence
A, B, C: AbGroup
E: AbSES C B
U: AbSES C A
cxfib (iscomplex_pullback_abses E) U =
equiv_hfiber_abses (abses_pullback (inclusion E)) pt
  (cxfib' E U)
  srapply path_sigma.H: Univalence
A, B, C: AbGroup
E: AbSES C B
U: AbSES C A
(cxfib (iscomplex_pullback_abses E) U).1 =
(equiv_hfiber_abses (abses_pullback (inclusion E)) pt
   (cxfib' E U)).1
H: Univalence
A, B, C: AbGroup
E: AbSES C B
U: AbSES C A
transport
  (fun x : AbSES E A =>
   abses_pullback_pmap (inclusion E) x = pt) ?p
  (cxfib (iscomplex_pullback_abses E) U).2 =
(equiv_hfiber_abses (abses_pullback (inclusion E)) pt
   (cxfib' E U)).2
  1: reflexivity.H: Univalence
A, B, C: AbGroup
E: AbSES C B
U: AbSES C A
transport
  (fun x : AbSES E A =>
   abses_pullback_pmap (inclusion E) x = pt) 1
  (cxfib (iscomplex_pullback_abses E) U).2 =
(equiv_hfiber_abses (abses_pullback (inclusion E)) pt
   (cxfib' E U)).2
  nrefine (concat_p1 _ @ _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
U: AbSES C A
(to_pointed_compose (abses_pullback' (projection E))
   (abses_pullback' (inclusion E)) @*
 (let X := equiv_fun equiv_ptransformation_phomotopy
    in
  X
    (iscomplex_abses_pullback' (inclusion E)
       (projection E) (iscomplex_abses E)))) U =
(equiv_hfiber_abses (abses_pullback (inclusion E)) pt
   (cxfib' E U)).2
  nrefine (concat_1p _ @ _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
U: AbSES C A
(let X := equiv_fun equiv_ptransformation_phomotopy in
 X
   (iscomplex_abses_pullback' (inclusion E)
      (projection E) (iscomplex_abses E))) U =
(equiv_hfiber_abses (abses_pullback (inclusion E)) pt
   (cxfib' E U)).2
  cbn zeta.H: Univalence
A, B, C: AbGroup
E: AbSES C B
U: AbSES C A
equiv_ptransformation_phomotopy
  (iscomplex_abses_pullback' (inclusion E)
     (projection E) (iscomplex_abses E)) U =
(equiv_hfiber_abses (abses_pullback (inclusion E)) pt
   (cxfib' E U)).2
  unfold equiv_hfiber_abses, equiv_functor_sigma_id, equiv_functor_sigma', equiv_functor_sigma, equiv_fun, functor_sigma, ".2".H: Univalence
A, B, C: AbGroup
E: AbSES C B
U: AbSES C A
equiv_ptransformation_phomotopy
  (iscomplex_abses_pullback' (inclusion E)
     (projection E) (iscomplex_abses E)) U =
equiv_path_abses_iso (cxfib' E U).2
  (* The goal looks identical to [pr2_cxfib'], but the implicit argument to [@paths] is expressed differently, which is why the next line isn't faster. *)
  exact (@pr2_cxfib' _ A B C E U).
Defined.

Transparent abses_pullback'.

Definition equiv_hfiber_cxfib' `{Univalence} {A B C : AbGroup} {E : AbSES C B}
           (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt)
  : hfiber_cxfib' E F p <~> hfiber (cxfib (iscomplex_pullback_abses E))
                  (equiv_hfiber_abses _ pt (F;p)).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
hfiber_cxfib' E F p <~>
hfiber (cxfib (iscomplex_pullback_abses E))
  (equiv_hfiber_abses (abses_pullback (inclusion E))
     pt (F; p))
Proof.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
hfiber_cxfib' E F p <~>
hfiber (cxfib (iscomplex_pullback_abses E))
  (equiv_hfiber_abses (abses_pullback (inclusion E))
     pt (F; p))
  srapply equiv_functor_sigma_id; intro U; lazy beta.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U: AbSES C A
hfiber_abses_path (cxfib' E U) (F; p) <~>
cxfib (iscomplex_pullback_abses E) U =
equiv_hfiber_abses (abses_pullback (inclusion E)) pt
  (F; p)
  refine (_ oE equiv_hfiber_abses_pullback _ _ _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U: AbSES C A
cxfib' E U = (F; p) <~>
cxfib (iscomplex_pullback_abses E) U =
equiv_hfiber_abses (abses_pullback (inclusion E)) pt
  (F; p)
  refine (_ oE equiv_ap' (equiv_hfiber_abses _ pt) _ _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U: AbSES C A
equiv_hfiber_abses (abses_pullback (inclusion E)) pt
  (cxfib' E U) =
equiv_hfiber_abses (abses_pullback (inclusion E)) pt
  (F; p) <~>
cxfib (iscomplex_pullback_abses E) U =
equiv_hfiber_abses (abses_pullback (inclusion E)) pt
  (F; p)
  apply equiv_concat_l.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U: AbSES C A
cxfib (iscomplex_pullback_abses E) U =
equiv_hfiber_abses (abses_pullback (inclusion E)) pt
  (cxfib' E U)
  apply eq_cxfib_cxfib'.
Defined.

(** The type of paths in [hfiber_cxfib'] in terms of path data. *)
Definition path_hfiber_cxfib' {A B C : AbGroup} {E : AbSES C B}
           {F : AbSES (middle E) A} {p : abses_pullback (inclusion E) F $== pt}
           (X Y : hfiber_cxfib' (B:=B) E F p)
  : Type.A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
X, Y: hfiber_cxfib' E F p
Type
Proof.A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
X, Y: hfiber_cxfib' E F p
Type
  refine (sig (fun q0 : X.1 $== Y.1 => _)).A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
X, Y: hfiber_cxfib' E F p
q0: X.1 $== Y.1
Type
  exact ((fmap (abses_pullback (projection E)) q0)^$ $@ X.2.1 $== Y.2.1).
Defined.

Definition transport_hfiber_abses_path_cxfib'_l `{Univalence} {A B C : AbGroup} {E : AbSES C B}
           (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt)
           (U V : hfiber_cxfib' E F p) (q : U.1 = V.1)
  : (transport (fun Y : AbSES C A => hfiber_abses_path (cxfib' E Y) (F; p)) q U.2).1
    = fmap (abses_pullback (projection E)) (equiv_path_abses_iso^-1 q^) $@ U.2.1.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
q: U.1 = V.1
(transport
   (fun Y : AbSES C A =>
    hfiber_abses_path (cxfib' E Y) (F; p)) q U.2).1 =
fmap (abses_pullback (projection E))
  (equiv_path_abses_iso^-1 q^) $@ (U.2).1
Proof.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
q: U.1 = V.1
(transport
   (fun Y : AbSES C A =>
    hfiber_abses_path (cxfib' E Y) (F; p)) q U.2).1 =
fmap (abses_pullback (projection E))
  (equiv_path_abses_iso^-1 q^) $@ (U.2).1
  induction q.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
(transport
   (fun Y : AbSES C A =>
    hfiber_abses_path (cxfib' E Y) (F; p)) 1 U.2).1 =
fmap (abses_pullback (projection E))
  (equiv_path_abses_iso^-1 1^) $@ (U.2).1
  refine (ap pr1 (transport_1 _ _) @ _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
(U.2).1 =
fmap (abses_pullback (projection E))
  (equiv_path_abses_iso^-1 1^) $@ (U.2).1
  refine (_ @ ap (fun x => fmap (abses_pullback (projection E)) x $@ _) equiv_path_absesV_1^).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
(U.2).1 =
fmap (abses_pullback (projection E)) (Id U.1) $@
(U.2).1
  refine (_ @ ap (fun x => x $@ _) (fmap_id_strong _ _)^).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
(U.2).1 =
Id (abses_pullback (projection E) U.1) $@ (U.2).1
  exact (cat_idr_strong _)^.
Defined.

Definition equiv_path_hfiber_cxfib' `{Univalence} {A B C : AbGroup} {E : AbSES C B}
           (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt)
           (U V : hfiber_cxfib' E F p)
  : path_hfiber_cxfib' U V <~> U = V.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
path_hfiber_cxfib' U V <~> U = V
Proof.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
path_hfiber_cxfib' U V <~> U = V
  refine (equiv_path_sigma _ _ _ oE _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
path_hfiber_cxfib' U V <~>
{p0 : U.1 = V.1 &
transport
  (fun Y : AbSES C A =>
   hfiber_abses_path (cxfib' E Y) (F; p)) p0 U.2 = V.2}
  srapply (equiv_functor_sigma' equiv_path_abses_iso);
    intro q; lazy beta.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
q: abses_path_data_iso U.1 V.1
(fmap (abses_pullback (projection E)) q)^$ $@ (U.2).1 $==
(V.2).1 <~>
transport
  (fun Y : AbSES C A =>
   hfiber_abses_path (cxfib' E Y) (F; p))
  (equiv_path_abses_iso q) U.2 = V.2
  refine (equiv_path_sigma_hprop _ _ oE _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
q: abses_path_data_iso U.1 V.1
(fmap (abses_pullback (projection E)) q)^$ $@ (U.2).1 $==
(V.2).1 <~>
(transport
   (fun Y : AbSES C A =>
    hfiber_abses_path (cxfib' E Y) (F; p))
   (equiv_path_abses_iso q) U.2).1 = (V.2).1
  refine (equiv_concat_l _ _ oE _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
q: abses_path_data_iso U.1 V.1
(transport
   (fun Y : AbSES C A =>
    hfiber_abses_path (cxfib' E Y) (F; p))
   (equiv_path_abses_iso q) U.2).1 = ?Goal
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
q: abses_path_data_iso U.1 V.1
(fmap (abses_pullback (projection E)) q)^$ $@ (U.2).1 $==
(V.2).1 <~> ?Goal = (V.2).1
  1: apply transport_hfiber_abses_path_cxfib'_l.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
q: abses_path_data_iso U.1 V.1
(fmap (abses_pullback (projection E)) q)^$ $@ (U.2).1 $==
(V.2).1 <~>
fmap (abses_pullback (projection E))
  (equiv_path_abses_iso^-1 (equiv_path_abses_iso q)^) $@
(U.2).1 = (V.2).1
  refine (equiv_path_sigma_hprop _ _ oE equiv_concat_l _ _ oE _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
q: abses_path_data_iso U.1 V.1
(fmap (abses_pullback (projection E))
   (equiv_path_abses_iso^-1 (equiv_path_abses_iso q)^) $@
 (U.2).1).1 = ?Goal
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
q: abses_path_data_iso U.1 V.1
(fmap (abses_pullback (projection E)) q)^$ $@ (U.2).1 $==
(V.2).1 <~> ?Goal = ((V.2).1).1
  1: {H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
q: abses_path_data_iso U.1 V.1
(fmap (abses_pullback (projection E))
   (equiv_path_abses_iso^-1 (equiv_path_abses_iso q)^) $@
 (U.2).1).1 = ?Goal refine (ap (fun x => (fmap (abses_pullback _) x $@ _).1) _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
q: abses_path_data_iso U.1 V.1
equiv_path_abses_iso^-1 (equiv_path_abses_iso q)^ =
?Goal0
       nrefine (ap _ (abses_path_data_V q) @ _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
q: abses_path_data_iso U.1 V.1
equiv_path_abses_iso^-1
  (equiv_path_abses_iso (abses_path_data_inverse q)) =
?Goal0
       apply eissect. }H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
q: abses_path_data_iso U.1 V.1
(fmap (abses_pullback (projection E)) q)^$ $@ (U.2).1 $==
(V.2).1 <~>
(fmap (abses_pullback (projection E))
   (abses_path_data_inverse q) $@ (U.2).1).1 =
((V.2).1).1
  refine (equiv_concat_l _ _ oE _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
q: abses_path_data_iso U.1 V.1
(fmap (abses_pullback (projection E))
   (abses_path_data_inverse q) $@ (U.2).1).1 = ?Goal
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
q: abses_path_data_iso U.1 V.1
(fmap (abses_pullback (projection E)) q)^$ $@ (U.2).1 $==
(V.2).1 <~> ?Goal = ((V.2).1).1
  1: {H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
q: abses_path_data_iso U.1 V.1
(fmap (abses_pullback (projection E))
   (abses_path_data_inverse q) $@ (U.2).1).1 = ?Goal refine (ap (fun x => (x $@ _).1) _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
q: abses_path_data_iso U.1 V.1
fmap (abses_pullback (projection E))
  (abses_path_data_inverse q) = ?Goal0
       rapply gpd_strong_1functor_V. }H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
U, V: hfiber_cxfib' E F p
q: abses_path_data_iso U.1 V.1
(fmap (abses_pullback (projection E)) q)^$ $@ (U.2).1 $==
(V.2).1 <~>
((fmap (abses_pullback (projection E)) q)^$ $@ (U.2).1).1 =
((V.2).1).1
  apply equiv_path_groupisomorphism.
Defined.

(** The fibre of [cxfib'] over [(F;p)] is inhabited. *)
Definition hfiber_cxfib'_inhabited `{Univalence} {A B C : AbGroup} (E : AbSES C B)
      (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt)
  : hfiber_cxfib' E F p.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
hfiber_cxfib' E F p
Proof.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
hfiber_cxfib' E F p
  exists (abses_pullback_trivial_preimage E F p).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
hfiber_abses_path
  (cxfib' E (abses_pullback_trivial_preimage E F p))
  (F; p)
  srefine (_^$; _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
(F; p).1 $->
(cxfib' E (abses_pullback_trivial_preimage E F p)).1
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
(fun
   p0 : (cxfib' E
           (abses_pullback_trivial_preimage E F p)).1 $->
        (F; p).1 =>
 (fmap (abses_pullback (inclusion E)) p0)^$ $@
 (cxfib' E (abses_pullback_trivial_preimage E F p)).2 $->
 (F; p).2) ?Goal^$
  1: by rapply (abses_pullback_component1_id' (abses_pullback_inclusion0_map' E F p)).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
(fun
   p0 : (cxfib' E
           (abses_pullback_trivial_preimage E F p)).1 $->
        (F; p).1 =>
 (fmap (abses_pullback (inclusion E)) p0)^$ $@
 (cxfib' E (abses_pullback_trivial_preimage E F p)).2 $->
 (F; p).2)
  (abses_pullback_component1_id'
     (abses_pullback_inclusion0_map' E F p)
     (fun x0 : A => 1%path))^$
  lazy beta; unfold pr2.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
(fmap (abses_pullback (inclusion E))
   (abses_pullback_component1_id'
      (abses_pullback_inclusion0_map' E F p)
      (fun x0 : A => 1%path))^$)^$ $@
(cxfib' E (abses_pullback_trivial_preimage E F p)).2 $->
p
  refine (cat_assoc _ _ _ $@ _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
abses_pullback_homotopic'
  (projection E $o inclusion E) grp_homo_const
  (iscomplex_abses E)
  (abses_pullback_trivial_preimage E F p) $@
symmetric_GpdHom pt
  (abses_pullback grp_homo_const
     (abses_pullback_trivial_preimage E F p))
  (abses_pullback_const'
     (abses_pullback_trivial_preimage E F p)) $o
(abses_pullback_compose' (inclusion E) (projection E)
   (abses_pullback_trivial_preimage E F p) $o
 (fmap (abses_pullback (inclusion E))
    (abses_pullback_component1_id'
       (abses_pullback_inclusion0_map' E F p)
       (fun x0 : A => 1%path))^$)^$) $== p
  refine (cat_assoc _ _ _ $@ _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
symmetric_GpdHom pt
  (abses_pullback grp_homo_const
     (abses_pullback_trivial_preimage E F p))
  (abses_pullback_const'
     (abses_pullback_trivial_preimage E F p)) $o
(abses_pullback_homotopic'
   (projection E $o inclusion E) grp_homo_const
   (iscomplex_abses E)
   (abses_pullback_trivial_preimage E F p) $o
 (abses_pullback_compose' (inclusion E) (projection E)
    (abses_pullback_trivial_preimage E F p) $o
  (fmap (abses_pullback (inclusion E))
     (abses_pullback_component1_id'
        (abses_pullback_inclusion0_map' E F p)
        (fun x0 : A => 1%path))^$)^$)) $== p
  apply gpd_moveR_Vh.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
abses_pullback_homotopic'
  (projection E $o inclusion E) grp_homo_const
  (iscomplex_abses E)
  (abses_pullback_trivial_preimage E F p) $o
(abses_pullback_compose' (inclusion E) (projection E)
   (abses_pullback_trivial_preimage E F p) $o
 (fmap (abses_pullback (inclusion E))
    (abses_pullback_component1_id'
       (abses_pullback_inclusion0_map' E F p)
       (fun x0 : A => 1%path))^$)^$) $==
abses_pullback_const'
  (abses_pullback_trivial_preimage E F p) $o p
  apply gpd_moveL_hM.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
abses_pullback_homotopic'
  (projection E $o inclusion E) grp_homo_const
  (iscomplex_abses E)
  (abses_pullback_trivial_preimage E F p) $o
(abses_pullback_compose' (inclusion E) (projection E)
   (abses_pullback_trivial_preimage E F p) $o
 (fmap (abses_pullback (inclusion E))
    (abses_pullback_component1_id'
       (abses_pullback_inclusion0_map' E F p)
       (fun x0 : A => 1%path))^$)^$) $o p^$ $==
abses_pullback_const'
  (abses_pullback_trivial_preimage E F p)
  apply equiv_path_biprod_corec.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
(((abses_pullback_homotopic'
     (projection E $o inclusion E) grp_homo_const
     (iscomplex_abses E)
     (abses_pullback_trivial_preimage E F p) $o
   (abses_pullback_compose' (inclusion E)
      (projection E)
      (abses_pullback_trivial_preimage E F p) $o
    (fmap (abses_pullback (inclusion E))
       (abses_pullback_component1_id'
          (abses_pullback_inclusion0_map' E F p)
          (fun x0 : A => 1%path))^$)^$) $o p^$).1 $o
  ab_biprod_inl ==
  (abses_pullback_const'
     (abses_pullback_trivial_preimage E F p)).1 $o
  ab_biprod_inl) *
 ((abses_pullback_homotopic'
     (projection E $o inclusion E) grp_homo_const
     (iscomplex_abses E)
     (abses_pullback_trivial_preimage E F p) $o
   (abses_pullback_compose' (inclusion E)
      (projection E)
      (abses_pullback_trivial_preimage E F p) $o
    (fmap (abses_pullback (inclusion E))
       (abses_pullback_component1_id'
          (abses_pullback_inclusion0_map' E F p)
          (fun x0 : A => 1%path))^$)^$) $o p^$).1 $o
  ab_biprod_inr ==
  (abses_pullback_const'
     (abses_pullback_trivial_preimage E F p)).1 $o
  ab_biprod_inr))%type
  split; apply equiv_path_pullback_rec_hset; split; cbn.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
(fun x : A =>
 class_of
   (fun x0 y : F =>
    hfiber
      (fun x1 : B =>
       pullback_pr1 ((p.1)^-1 (group_unit, x1)))
      (- x0 + y))
   (pullback_pr1 ((p.1)^-1 (x, group_unit)))) ==
(fun x : A =>
 class_of
   (fun x0 y : F =>
    hfiber
      (fun x1 : B =>
       pullback_pr1 ((p.1)^-1 (group_unit, x1)))
      (- x0 + y)) (inclusion F x))
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
(fun x : A => pullback_pr2 ((p.1)^-1 (x, group_unit))) ==
(fun _ : A => group_unit)
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
(fun x : B =>
 class_of
   (fun x0 y : F =>
    hfiber
      (fun x1 : B =>
       pullback_pr1 ((p.1)^-1 (group_unit, x1)))
      (- x0 + y))
   (pullback_pr1 ((p.1)^-1 (group_unit, x)))) ==
(fun _ : B =>
 class_of
   (fun x y : F =>
    hfiber
      (fun x0 : B =>
       pullback_pr1 ((p.1)^-1 (group_unit, x0)))
      (- x + y)) (inclusion F group_unit))
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
(fun x : B => pullback_pr2 ((p.1)^-1 (group_unit, x))) ==
idmap
  -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
(fun x : A =>
 class_of
   (fun x0 y : F =>
    hfiber
      (fun x1 : B =>
       pullback_pr1 ((p.1)^-1 (group_unit, x1)))
      (- x0 + y))
   (pullback_pr1 ((p.1)^-1 (x, group_unit)))) ==
(fun x : A =>
 class_of
   (fun x0 y : F =>
    hfiber
      (fun x1 : B =>
       pullback_pr1 ((p.1)^-1 (group_unit, x1)))
      (- x0 + y)) (inclusion F x)) intro a.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
class_of
  (fun x y : F =>
   hfiber
     (fun x0 : B =>
      pullback_pr1 ((p.1)^-1 (group_unit, x0)))
     (- x + y))
  (pullback_pr1 ((p.1)^-1 (a, group_unit))) =
class_of
  (fun x y : F =>
   hfiber
     (fun x0 : B =>
      pullback_pr1 ((p.1)^-1 (group_unit, x0)))
     (- x + y)) (inclusion F a)
    exact (ap (class_of _ o pullback_pr1) (fst p^$.2 a)).
  -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
(fun x : A => pullback_pr2 ((p.1)^-1 (x, group_unit))) ==
(fun _ : A => group_unit) intro a.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
a: A
pullback_pr2 ((p.1)^-1 (a, group_unit)) = group_unit
    exact ((snd p^$.2 _)^).
  -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
(fun x : B =>
 class_of
   (fun x0 y : F =>
    hfiber
      (fun x1 : B =>
       pullback_pr1 ((p.1)^-1 (group_unit, x1)))
      (- x0 + y))
   (pullback_pr1 ((p.1)^-1 (group_unit, x)))) ==
(fun _ : B =>
 class_of
   (fun x y : F =>
    hfiber
      (fun x0 : B =>
       pullback_pr1 ((p.1)^-1 (group_unit, x0)))
      (- x + y)) (inclusion F group_unit)) intro b; apply qglue.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
b: B
hfiber
  (fun x : B =>
   pullback_pr1 ((p.1)^-1 (group_unit, x)))
  (- pullback_pr1 ((p.1)^-1 (group_unit, b)) +
   inclusion F group_unit)
    exists (-b).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
b: B
pullback_pr1 ((p.1)^-1 (group_unit, - b)) =
- pullback_pr1 ((p.1)^-1 (group_unit, b)) +
inclusion F group_unit
    apply grp_moveL_Vg.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
b: B
pullback_pr1 ((p.1)^-1 (group_unit, b)) +
pullback_pr1 ((p.1)^-1 (group_unit, - b)) =
inclusion F group_unit
    refine ((grp_homo_op (grp_pullback_pr1 _ _ $o p^$.1 $o ab_biprod_inr) _ _)^ @ _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
b: B
(grp_pullback_pr1 (projection F) (inclusion E) $o
 (p^$).1 $o ab_biprod_inr) (b + group_inverse b) =
inclusion F group_unit
    exact (ap _ (right_inverse _) @ grp_homo_unit _ @ (grp_homo_unit _)^).
  -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
(fun x : B => pullback_pr2 ((p.1)^-1 (group_unit, x))) ==
idmap intro b.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
b: B
pullback_pr2 ((p.1)^-1 (group_unit, b)) = b
    exact (snd p^$.2 _)^.
Defined.

(** To conclude exactness in terms of path data, we show that the fibre is a proposition, hence contractible. *)

(** Given a point [(Y;Q)] in the fiber of [cxfib'] over [(F;p)] there is an induced map as follows. *)
Local Definition hfiber_cxfib'_induced_map {A B C : AbGroup} (E : AbSES C B)
      (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt)
      (Y : hfiber_cxfib' E F p)
  : ab_biprod A B $-> abses_pullback (projection E) Y.1.A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
ab_biprod A B $-> abses_pullback (projection E) Y.1
Proof.A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
ab_biprod A B $-> abses_pullback (projection E) Y.1
  destruct Y as [Y q].A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
q: hfiber_abses_path (cxfib' E Y) (F; p)
ab_biprod A B $->
abses_pullback (projection E) (Y; q).1
  refine (grp_homo_compose _ (grp_iso_inverse p.1)).A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
q: hfiber_abses_path (cxfib' E Y) (F; p)
GroupHomomorphism (abses_pullback (inclusion E) F)
  (abses_pullback (projection E) (Y; q).1)
  refine (_ $o grp_pullback_pr1 _ _).A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
q: hfiber_abses_path (cxfib' E Y) (F; p)
F $-> abses_pullback (projection E) (Y; q).1
  exact (q.1^$.1).
Defined.

(** There is "another" obvious induced map. *)
Definition abses_pullback_splits_induced_map' {A B C : AbGroup}
           (E : AbSES C B) (Y : AbSES C A)
  : ab_biprod A B $-> abses_pullback (projection E) Y.A, B, C: AbGroup
E: AbSES C B
Y: AbSES C A
ab_biprod A B $-> abses_pullback (projection E) Y
Proof.A, B, C: AbGroup
E: AbSES C B
Y: AbSES C A
ab_biprod A B $-> abses_pullback (projection E) Y
  srapply (ab_biprod_rec (inclusion _)).A, B, C: AbGroup
E: AbSES C B
Y: AbSES C A
B $-> abses_pullback (projection E) Y
  srapply grp_pullback_corec.A, B, C: AbGroup
E: AbSES C B
Y: AbSES C A
B $-> Y
A, B, C: AbGroup
E: AbSES C B
Y: AbSES C A
B $-> E
A, B, C: AbGroup
E: AbSES C B
Y: AbSES C A
projection Y o ?b == projection E o ?c
  -A, B, C: AbGroup
E: AbSES C B
Y: AbSES C A
B $-> Y exact grp_homo_const.
  -A, B, C: AbGroup
E: AbSES C B
Y: AbSES C A
B $-> E exact (inclusion E).
  -A, B, C: AbGroup
E: AbSES C B
Y: AbSES C A
projection Y o grp_homo_const ==
projection E o inclusion E intro x.A, B, C: AbGroup
E: AbSES C B
Y: AbSES C A
x: B
projection Y (grp_homo_const x) =
projection E (inclusion E x)
    refine (grp_homo_unit _ @ _).A, B, C: AbGroup
E: AbSES C B
Y: AbSES C A
x: B
mon_unit = projection E (inclusion E x)
    symmetry; apply iscomplex_abses.
Defined.

Lemma fmap_hfiber_abses_lemma `{Univalence} {A B B' : AbGroup} (f : B' $-> B)
           (X Y : graph_hfiber (abses_pullback (A:=A) f) pt) (Q : hfiber_abses_path X Y)
  : fmap (abses_pullback f) Q.1^$ $o Y.2^$ $== X.2^$.H: Univalence
A, B, B': AbGroup
f: B' $-> B
X, Y: graph_hfiber (abses_pullback f) pt
Q: hfiber_abses_path X Y
fmap (abses_pullback f) (Q.1)^$ $o (Y.2)^$ $== (X.2)^$
Proof.H: Univalence
A, B, B': AbGroup
f: B' $-> B
X, Y: graph_hfiber (abses_pullback f) pt
Q: hfiber_abses_path X Y
fmap (abses_pullback f) (Q.1)^$ $o (Y.2)^$ $== (X.2)^$
  generalize Q.H: Univalence
A, B, B': AbGroup
f: B' $-> B
X, Y: graph_hfiber (abses_pullback f) pt
Q: hfiber_abses_path X Y
forall Q : hfiber_abses_path X Y,
fmap (abses_pullback f) (Q.1)^$ $o (Y.2)^$ $== (X.2)^$
  equiv_intro (equiv_hfiber_abses_pullback _ X Y)^-1%equiv p;
    induction p.H: Univalence
A, B, B': AbGroup
f: B' $-> B
X: graph_hfiber (abses_pullback f) pt
Q: hfiber_abses_path X X
fmap (abses_pullback f)
  ((((equiv_hfiber_abses_pullback pt X X)^-1)%equiv
      1%path).1)^$ $o (X.2)^$ $== (X.2)^$
  refine ((_ $@R _) $@ _).H: Univalence
A, B, B': AbGroup
f: B' $-> B
X: graph_hfiber (abses_pullback f) pt
Q: hfiber_abses_path X X
fmap (abses_pullback f)
  ((((equiv_hfiber_abses_pullback pt X X)^-1)%equiv
      1%path).1)^$ $== ?Goal
H: Univalence
A, B, B': AbGroup
f: B' $-> B
X: graph_hfiber (abses_pullback f) pt
Q: hfiber_abses_path X X
?Goal $o (X.2)^$ $== (X.2)^$
  {H: Univalence
A, B, B': AbGroup
f: B' $-> B
X: graph_hfiber (abses_pullback f) pt
Q: hfiber_abses_path X X
fmap (abses_pullback f)
  ((((equiv_hfiber_abses_pullback pt X X)^-1)%equiv
      1%path).1)^$ $== ?Goal Unshelve.H: Univalence
A, B, B': AbGroup
f: B' $-> B
X: graph_hfiber (abses_pullback f) pt
Q: hfiber_abses_path X X
fmap (abses_pullback f)
  ((((equiv_hfiber_abses_pullback pt X X)^-1)%equiv
      1%path).1)^$ $== ?Goal
H: Univalence
A, B, B': AbGroup
f: B' $-> B
X: graph_hfiber (abses_pullback f) pt
Q: hfiber_abses_path X X
abses_pullback f X.1 $-> abses_pullback f X.1
    2: exact (Id _).H: Univalence
A, B, B': AbGroup
f: B' $-> B
X: graph_hfiber (abses_pullback f) pt
Q: hfiber_abses_path X X
fmap (abses_pullback f)
  ((((equiv_hfiber_abses_pullback pt X X)^-1)%equiv
      1%path).1)^$ $== Id (abses_pullback f X.1)
    refine (fmap2 _ _ $@ fmap_id _ _).H: Univalence
A, B, B': AbGroup
f: B' $-> B
X: graph_hfiber (abses_pullback f) pt
Q: hfiber_abses_path X X
((((equiv_hfiber_abses_pullback pt X X)^-1)%equiv
    1%path).1)^$ $== Id X.1
    intro x; reflexivity. }H: Univalence
A, B, B': AbGroup
f: B' $-> B
X: graph_hfiber (abses_pullback f) pt
Q: hfiber_abses_path X X
Id (abses_pullback f X.1) $o (X.2)^$ $== (X.2)^$
  exact (cat_idl _).
Defined.

Lemma induced_map_eq `{Univalence} {A B C : AbGroup} (E : AbSES C B)
      (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt)
      (Y : hfiber_cxfib' E F p)
  : hfiber_cxfib'_induced_map E F p Y == abses_pullback_splits_induced_map' E Y.1.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
hfiber_cxfib'_induced_map E F p Y ==
abses_pullback_splits_induced_map' E Y.1
Proof.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
hfiber_cxfib'_induced_map E F p Y ==
abses_pullback_splits_induced_map' E Y.1
  intros [a b]; cbn.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
a: A
b: B
(((Y.2).1).1)^-1 (pullback_pr1 ((p.1)^-1 (a, b))) =
grp_pullback_sgop (projection Y.1) (projection E)
  (inclusion Y.1 a; group_unit;
  cx_isexact a @ (grp_homo_unit (projection E))^)
  (group_unit; inclusion E b;
  grp_homo_unit (projection Y.1) @
  (iscomplex_abses E b)^)
  refine (ap pullback_pr1 (fmap_hfiber_abses_lemma _ _ (F;p) Y.2 _) @ _).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
a: A
b: B
pullback_pr1 ((((cxfib' E Y.1).2)^$).1 (a, b)) =
grp_pullback_sgop (projection Y.1) (projection E)
  (inclusion Y.1 a; group_unit;
  cx_isexact a @ (grp_homo_unit (projection E))^)
  (group_unit; inclusion E b;
  grp_homo_unit (projection Y.1) @
  (iscomplex_abses E b)^)
  srapply equiv_path_pullback_hset; split; cbn.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
a: A
b: B
inclusion Y.1 a = inclusion Y.1 a + group_unit
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
a: A
b: B
inclusion E b = group_unit + inclusion E b
  -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
a: A
b: B
inclusion Y.1 a = inclusion Y.1 a + group_unit exact (grp_unit_r _)^.
  -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
a: A
b: B
inclusion E b = group_unit + inclusion E b exact (grp_unit_l _)^.
Defined.

(** Given another point [(Y,Q)] in the fibre of [cxfib'] over [(F;p)], we get path data in [AbSES C A]. *)
Lemma hfiber_cxfib'_induced_path'0 `{Univalence} {A B C : AbGroup} (E : AbSES C B)
      (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt)
      (Y : hfiber_cxfib' E F p)
  : abses_pullback_trivial_preimage E F p $== Y.1.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
abses_pullback_trivial_preimage E F p $== Y.1
Proof.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
abses_pullback_trivial_preimage E F p $== Y.1
  destruct Y as [Y Q].H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
abses_pullback_trivial_preimage E F p $== (Y; Q).1
  apply abses_path_data_to_iso;
    srefine (_; (_,_)).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
GroupHomomorphism
  (abses_pullback_trivial_preimage E F p) (Y; Q).1
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
?proj1 $o
inclusion (abses_pullback_trivial_preimage E F p) ==
inclusion (Y; Q).1
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
projection (abses_pullback_trivial_preimage E F p) ==
projection (Y; Q).1 $o ?proj1
  -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
GroupHomomorphism
  (abses_pullback_trivial_preimage E F p) (Y; Q).1 snrapply (ab_cokernel_embedding_rec _ (grp_pullback_pr1 _ _$o (Q.1^$).1)).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
Is01Cat Group
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
Is01Cat (AbSES E A)
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
Is0Gpd (AbSES E A)
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
grp_homo_compose
  (grp_pullback_pr1 (projection Y) (projection E) $o
   ((Q.1)^$).1)
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p) $== grp_homo_const
    1-3: exact _.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
grp_homo_compose
  (grp_pullback_pr1 (projection Y) (projection E) $o
   ((Q.1)^$).1)
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p) $== grp_homo_const
    intro f.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
f: B
grp_homo_compose
  (grp_pullback_pr1 (projection Y) (projection E) $o
   ((Q.1)^$).1)
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p) f = grp_homo_const f
    nrefine (ap _ (induced_map_eq E F p (Y;Q) _) @ _); cbn.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
f: B
inclusion Y group_unit + group_unit = group_unit
    exact (grp_unit_r _ @ grp_homo_unit _).
  -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (grp_pullback_pr1 (projection Y) (projection E) $o
   ((Q.1)^$).1)
  ((fun f : B =>
    ap
      (grp_pullback_pr1 (projection Y) (projection E))
      (induced_map_eq E F p (Y; Q) (ab_biprod_inr f)) @
    (grp_unit_r (inclusion Y mon_unit) @
     grp_homo_unit (inclusion Y)
     :
     grp_pullback_pr1 (projection Y) (projection E)
       (abses_pullback_splits_induced_map' E (Y; Q).1
          (ab_biprod_inr f)) = grp_homo_const f))
   :
   grp_homo_compose
     (grp_pullback_pr1 (projection Y) (projection E) $o
      ((Q.1)^$).1)
     (abses_pullback_inclusion_transpose_map
        (inclusion E) F p) $== grp_homo_const) $o
inclusion (abses_pullback_trivial_preimage E F p) ==
inclusion (Y; Q).1 intro a.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
a: A
(ab_cokernel_embedding_rec
   (abses_pullback_inclusion_transpose_map
      (inclusion E) F p)
   (grp_pullback_pr1 (projection Y) (projection E) $o
    ((Q.1)^$).1)
   (fun f : B =>
    ap
      (grp_pullback_pr1 (projection Y) (projection E))
      (induced_map_eq E F p (Y; Q) (ab_biprod_inr f)) @
    (grp_unit_r (inclusion Y mon_unit) @
     grp_homo_unit (inclusion Y))) $o
 inclusion (abses_pullback_trivial_preimage E F p)) a =
inclusion (Y; Q).1 a
    refine (_ @ ap (grp_pullback_pr1 _ _) (fst (Q.1^$).2 a)).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
a: A
(ab_cokernel_embedding_rec
   (abses_pullback_inclusion_transpose_map
      (inclusion E) F p)
   (grp_pullback_pr1 (projection Y) (projection E) $o
    ((Q.1)^$).1)
   (fun f : B =>
    ap
      (grp_pullback_pr1 (projection Y) (projection E))
      (induced_map_eq E F p (Y; Q) (ab_biprod_inr f)) @
    (grp_unit_r (inclusion Y mon_unit) @
     grp_homo_unit (inclusion Y))) $o
 inclusion (abses_pullback_trivial_preimage E F p)) a =
grp_pullback_pr1 (projection Y) (projection E)
  ((((Q.1)^$).1 $o inclusion (F; p).1) a)
    exact (grp_quotient_rec_beta' _ F _ _ (inclusion F a)).
  -H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
projection (abses_pullback_trivial_preimage E F p) ==
projection (Y; Q).1 $o
ab_cokernel_embedding_rec
  (abses_pullback_inclusion_transpose_map
     (inclusion E) F p)
  (grp_pullback_pr1 (projection Y) (projection E) $o
   ((Q.1)^$).1)
  ((fun f : B =>
    ap
      (grp_pullback_pr1 (projection Y) (projection E))
      (induced_map_eq E F p (Y; Q) (ab_biprod_inr f)) @
    (grp_unit_r (inclusion Y mon_unit) @
     grp_homo_unit (inclusion Y)
     :
     grp_pullback_pr1 (projection Y) (projection E)
       (abses_pullback_splits_induced_map' E (Y; Q).1
          (ab_biprod_inr f)) = grp_homo_const f))
   :
   grp_homo_compose
     (grp_pullback_pr1 (projection Y) (projection E) $o
      ((Q.1)^$).1)
     (abses_pullback_inclusion_transpose_map
        (inclusion E) F p) $== grp_homo_const) nrapply (conn_map_elim _ grp_quotient_map).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
IsConnMap ?Goal grp_quotient_map
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
forall
b : QuotientGroup F
      {|
        normalsubgroup_subgroup :=
          grp_image_embedding
            (abses_pullback_inclusion_transpose_map
               (inclusion E) F p);
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup F
            (grp_image_embedding
               (abses_pullback_inclusion_transpose_map
                  (inclusion E) F p))
      |},
In ?Goal
  (projection (abses_pullback_trivial_preimage E F p)
     b =
   (projection (Y; Q).1 $o
    ab_cokernel_embedding_rec
      (abses_pullback_inclusion_transpose_map
         (inclusion E) F p)
      (grp_pullback_pr1 (projection Y) (projection E) $o
       ((Q.1)^$).1)
      (fun f : B =>
       ap
         (grp_pullback_pr1 (projection Y)
            (projection E))
         (induced_map_eq E F p (Y; Q)
            (ab_biprod_inr f)) @
       (grp_unit_r (inclusion Y mon_unit) @
        grp_homo_unit (inclusion Y)))) b)
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
forall a : F,
projection (abses_pullback_trivial_preimage E F p)
  (grp_quotient_map a) =
(projection (Y; Q).1 $o
 ab_cokernel_embedding_rec
   (abses_pullback_inclusion_transpose_map
      (inclusion E) F p)
   (grp_pullback_pr1 (projection Y) (projection E) $o
    ((Q.1)^$).1)
   (fun f : B =>
    ap
      (grp_pullback_pr1 (projection Y) (projection E))
      (induced_map_eq E F p (Y; Q) (ab_biprod_inr f)) @
    (grp_unit_r (inclusion Y mon_unit) @
     grp_homo_unit (inclusion Y))))
  (grp_quotient_map a)
    1: apply issurj_class_of.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
forall
b : QuotientGroup F
      {|
        normalsubgroup_subgroup :=
          grp_image_embedding
            (abses_pullback_inclusion_transpose_map
               (inclusion E) F p);
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup F
            (grp_image_embedding
               (abses_pullback_inclusion_transpose_map
                  (inclusion E) F p))
      |},
In (Tr (-1))
  (projection (abses_pullback_trivial_preimage E F p)
     b =
   (projection (Y; Q).1 $o
    ab_cokernel_embedding_rec
      (abses_pullback_inclusion_transpose_map
         (inclusion E) F p)
      (grp_pullback_pr1 (projection Y) (projection E) $o
       ((Q.1)^$).1)
      (fun f : B =>
       ap
         (grp_pullback_pr1 (projection Y)
            (projection E))
         (induced_map_eq E F p (Y; Q)
            (ab_biprod_inr f)) @
       (grp_unit_r (inclusion Y mon_unit) @
        grp_homo_unit (inclusion Y)))) b)
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
forall a : F,
projection (abses_pullback_trivial_preimage E F p)
  (grp_quotient_map a) =
(projection (Y; Q).1 $o
 ab_cokernel_embedding_rec
   (abses_pullback_inclusion_transpose_map
      (inclusion E) F p)
   (grp_pullback_pr1 (projection Y) (projection E) $o
    ((Q.1)^$).1)
   (fun f : B =>
    ap
      (grp_pullback_pr1 (projection Y) (projection E))
      (induced_map_eq E F p (Y; Q) (ab_biprod_inr f)) @
    (grp_unit_r (inclusion Y mon_unit) @
     grp_homo_unit (inclusion Y))))
  (grp_quotient_map a)
    1: intros ?; apply istrunc_paths; apply group_isgroup.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
forall a : F,
projection (abses_pullback_trivial_preimage E F p)
  (grp_quotient_map a) =
(projection (Y; Q).1 $o
 ab_cokernel_embedding_rec
   (abses_pullback_inclusion_transpose_map
      (inclusion E) F p)
   (grp_pullback_pr1 (projection Y) (projection E) $o
    ((Q.1)^$).1)
   (fun f : B =>
    ap
      (grp_pullback_pr1 (projection Y) (projection E))
      (induced_map_eq E F p (Y; Q) (ab_biprod_inr f)) @
    (grp_unit_r (inclusion Y mon_unit) @
     grp_homo_unit (inclusion Y))))
  (grp_quotient_map a)
    intro f.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
f: F
projection (abses_pullback_trivial_preimage E F p)
  (grp_quotient_map f) =
(projection (Y; Q).1 $o
 ab_cokernel_embedding_rec
   (abses_pullback_inclusion_transpose_map
      (inclusion E) F p)
   (grp_pullback_pr1 (projection Y) (projection E) $o
    ((Q.1)^$).1)
   (fun f : B =>
    ap
      (grp_pullback_pr1 (projection Y) (projection E))
      (induced_map_eq E F p (Y; Q) (ab_biprod_inr f)) @
    (grp_unit_r (inclusion Y mon_unit) @
     grp_homo_unit (inclusion Y))))
  (grp_quotient_map f)
    refine (ap (projection E) (snd (Q.1^$).2 f) @ _); unfold pr1.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
Q: hfiber_abses_path (cxfib' E Y) (F; p)
f: F
projection E
  ((projection (cxfib' E Y).1 $o ((Q.1)^$).1) f) =
(projection Y $o
 ab_cokernel_embedding_rec
   (abses_pullback_inclusion_transpose_map
      (inclusion E) F p)
   (grp_pullback_pr1 (projection Y) (projection E) $o
    ((Q.1)^$).1)
   (fun f : B =>
    ap
      (grp_pullback_pr1 (projection Y) (projection E))
      (induced_map_eq E F p (Y; Q) (ab_biprod_inr f)) @
    (grp_unit_r (inclusion Y mon_unit) @
     grp_homo_unit (inclusion Y))))
  (grp_quotient_map f)
    exact (pullback_commsq _ _ ((Q.1^$).1 f))^.
Defined.

Lemma hfiber_cxfib'_induced_path' `{Univalence} {A B C : AbGroup} (E : AbSES C B)
      (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt)
      (Y : hfiber_cxfib' E F p)
  : path_hfiber_cxfib' (hfiber_cxfib'_inhabited E F p) Y.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
path_hfiber_cxfib' (hfiber_cxfib'_inhabited E F p) Y
Proof.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
path_hfiber_cxfib' (hfiber_cxfib'_inhabited E F p) Y
  exists (hfiber_cxfib'_induced_path'0 E F p Y).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
(fmap (abses_pullback (projection E))
   (hfiber_cxfib'_induced_path'0 E F p Y))^$ $@
((hfiber_cxfib'_inhabited E F p).2).1 $== (Y.2).1
  rapply gpd_moveR_Vh.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
(fmap (abses_pullback (projection E))
   (hfiber_cxfib'_induced_path'0 E F p Y))^$ $==
abses_pullback_component1_id'
  (abses_pullback_inclusion0_map' E F p)
  (fun x0 : A => 1%path) $o (Y.2).1
  rapply gpd_moveL_hM.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
(fmap (abses_pullback (projection E))
   (hfiber_cxfib'_induced_path'0 E F p Y))^$ $o
((Y.2).1)^$ $==
abses_pullback_component1_id'
  (abses_pullback_inclusion0_map' E F p)
  (fun x0 : A => 1%path)
  rapply gpd_moveR_Vh.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
((Y.2).1)^$ $==
fmap (abses_pullback (projection E))
  (hfiber_cxfib'_induced_path'0 E F p Y) $o
abses_pullback_component1_id'
  (abses_pullback_inclusion0_map' E F p)
  (fun x0 : A => 1%path)
  intro x.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
x: (F; p).1
(((Y.2).1)^$).1 x =
(fmap (abses_pullback (projection E))
   (hfiber_cxfib'_induced_path'0 E F p Y) $o
 abses_pullback_component1_id'
   (abses_pullback_inclusion0_map' E F p)
   (fun x0 : A => 1%path)).1 x
  srapply equiv_path_pullback_hset; split.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
x: (F; p).1
((((Y.2).1)^$).1 x).1 =
((fmap (abses_pullback (projection E))
    (hfiber_cxfib'_induced_path'0 E F p Y) $o
  abses_pullback_component1_id'
    (abses_pullback_inclusion0_map' E F p)
    (fun x0 : A => 1%path)).1 x).1
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
x: (F; p).1
(((((Y.2).1)^$).1 x).2).1 =
(((fmap (abses_pullback (projection E))
     (hfiber_cxfib'_induced_path'0 E F p Y) $o
   abses_pullback_component1_id'
     (abses_pullback_inclusion0_map' E F p)
     (fun x0 : A => 1%path)).1 x).2).1
  2: exact (snd Y.2.1^$.2 x)^.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: hfiber_cxfib' E F p
x: (F; p).1
((((Y.2).1)^$).1 x).1 =
((fmap (abses_pullback (projection E))
    (hfiber_cxfib'_induced_path'0 E F p Y) $o
  abses_pullback_component1_id'
    (abses_pullback_inclusion0_map' E F p)
    (fun x0 : A => 1%path)).1 x).1
  reflexivity.
Defined.

(** It follows that [hfiber_cxfib'] is contractible. *)
Lemma contr_hfiber_cxfib' `{Univalence} {A B C : AbGroup} (E : AbSES C B)
      (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt)
  : Contr (hfiber_cxfib' E F p).H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Contr (hfiber_cxfib' E F p)
Proof.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Contr (hfiber_cxfib' E F p)
  srapply Build_Contr.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
hfiber_cxfib' E F p
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
forall y : hfiber_cxfib' E F p, ?center = y
  1: apply hfiber_cxfib'_inhabited.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
forall y : hfiber_cxfib' E F p,
hfiber_cxfib'_inhabited E F p = y
  intros [Y q].H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
q: hfiber_abses_path (cxfib' E Y) (F; p)
hfiber_cxfib'_inhabited E F p = (Y; q)
  apply equiv_path_hfiber_cxfib'.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
Y: AbSES C A
q: hfiber_abses_path (cxfib' E Y) (F; p)
path_hfiber_cxfib' (hfiber_cxfib'_inhabited E F p)
  (Y; q)
  apply hfiber_cxfib'_induced_path'.
Defined.

(** From this we deduce exactness. *)
Global Instance isexact_abses_pullback `{Univalence} {A B C : AbGroup} {E : AbSES C B}
  : IsExact purely (abses_pullback_pmap (A:=A) (projection E)) (abses_pullback_pmap (inclusion E)).H: Univalence
A, B, C: AbGroup
E: AbSES C B
IsExact purely (abses_pullback_pmap (projection E))
  (abses_pullback_pmap (inclusion E))
Proof.H: Univalence
A, B, C: AbGroup
E: AbSES C B
IsExact purely (abses_pullback_pmap (projection E))
  (abses_pullback_pmap (inclusion E))
  srapply Build_IsExact.H: Univalence
A, B, C: AbGroup
E: AbSES C B
IsComplex (abses_pullback_pmap (projection E))
  (abses_pullback_pmap (inclusion E))
H: Univalence
A, B, C: AbGroup
E: AbSES C B
IsConnMap purely (cxfib ?cx_isexact)
  1: apply iscomplex_pullback_abses.H: Univalence
A, B, C: AbGroup
E: AbSES C B
IsConnMap purely (cxfib (iscomplex_pullback_abses E))
  srapply (equiv_ind (equiv_hfiber_abses (abses_pullback (inclusion E)) (point (AbSES B A)))).H: Univalence
A, B, C: AbGroup
E: AbSES C B
forall
x : graph_hfiber (abses_pullback (inclusion E)) pt,
(fun y : hfiber (abses_pullback (inclusion E)) pt =>
 IsConnected purely
   (hfiber (cxfib (iscomplex_pullback_abses E)) y))
  (equiv_hfiber_abses (abses_pullback (inclusion E))
     pt x)
  intros [F p].H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $-> pt
IsConnected purely
  (hfiber (cxfib (iscomplex_pullback_abses E))
     (equiv_hfiber_abses
        (abses_pullback (inclusion E)) pt (F; p)))
  rapply contr_equiv'.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $-> pt
?Goal <~>
purely
  (hfiber (cxfib (iscomplex_pullback_abses E))
     (equiv_hfiber_abses
        (abses_pullback (inclusion E)) pt (F; p)))
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $-> pt
Contr ?Goal
  1: apply equiv_hfiber_cxfib'.H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $-> pt
Contr (hfiber_cxfib' E F p)
  apply contr_hfiber_cxfib'.
Defined.