From HoTT Require Import Basics Types HSet HFiber Limits.Pullback.From HoTT Require Import Basics Types HSet HFiber Limits.Pullback.
From HoTT.WildCat Require Import Core NatTrans.
Require Import 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_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 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)
  napply (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 (0, b)) =
i (ab_biprod_pr2 (0, 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 (0, b)))) =
ab_biprod_pr2 (0, 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
  snapply 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_istrivial_kernel.
H: Univalence
A, B, C: AbGroup
E: AbSES C B
F: AbSES E A
p: abses_pullback (inclusion E) F $== pt
IsTrivialGroup (grp_kernel (grp_quotient_map $o inclusion F))
    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_kernel (grp_quotient_map $o inclusion F) a
trivial_subgroup A a
    (* 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_kernel (grp_quotient_map $o inclusion F) a
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) 0
trivial_subgroup A a
    (* 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_kernel (grp_quotient_map $o inclusion F) a
b: B
q1: abses_pullback_inclusion_transpose_map (inclusion E) F p b = - inclusion F a
trivial_subgroup A a
    (* 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_kernel (grp_quotient_map $o inclusion F) a
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_kernel (grp_quotient_map $o inclusion F) a
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)
trivial_subgroup A a
    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_kernel (grp_quotient_map $o inclusion F) a
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_kernel (grp_quotient_map $o inclusion F) a
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_kernel (grp_quotient_map $o inclusion F) a
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_kernel (grp_quotient_map $o inclusion F) a
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_kernel (grp_quotient_map $o inclusion F) a
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_kernel (grp_quotient_map $o inclusion F) a
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_kernel (grp_quotient_map $o inclusion F) a
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_kernel (grp_quotient_map $o inclusion F) a
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_kernel (grp_quotient_map $o inclusion F) a
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)
trivial_subgroup A a
    (* Using [q2], we conclude. *)
    pose proof (q3 := ap (-) (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_kernel (grp_quotient_map $o inclusion F) a
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
trivial_subgroup A a
    exact ((inverse_involutive _)^ @ q3^ @ grp_inv_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 E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) 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 E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) 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 E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) 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 E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
        X E b))
      :
      grp_homo_compose (projection E $o projection F)
        (abses_pullback_inclusion_transpose_map (inclusion E) F p) $==
      grp_homo_const)) snapply 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 E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) 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 E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) 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 E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) 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 E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) 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 E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) 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 E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) 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 E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) 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 E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) 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 E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) 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 E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) 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 E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) 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 E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) 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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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 E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in X E b))
  y =
pt
f: F
q0: grp_quotient_map f = y
merely (hfiber (inclusion E) (projection F f)) tapply 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 E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) 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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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 a0 : A =>
            ap (projection E)
              (let X :=
                 fun E0 : AbSES' E A => pointed_fun (iscomplex_abses E0) in
               X F a0) @
            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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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)))) tapply 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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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 a0 : A =>
            ap (projection E)
              (let X :=
                 fun E0 : AbSES' E A => pointed_fun (iscomplex_abses E0) in
               X F a0) @
            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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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 a0 : A =>
            ap (projection E)
              (let X :=
                 fun E0 : AbSES' E A => pointed_fun (iscomplex_abses E0) in
               X F a0) @
            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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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 a0 : A =>
      ap (projection E)
        (let X := fun E0 : AbSES' E A => pointed_fun (iscomplex_abses E0) in
         X F a0) @
      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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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 b0 : B =>
      ap (projection E)
        (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
      (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
       X E b0))
     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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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 a0 : A =>
       ap (projection E)
         (let X := fun E0 : AbSES' E A => pointed_fun (iscomplex_abses E0) in
          X F a0) @
       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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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 a0 : A =>
       ap (projection E)
         (let X := fun E0 : AbSES' E A => pointed_fun (iscomplex_abses E0) in
          X F a0) @
       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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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))) =
0
      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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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)))
  0
      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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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)) +
0
      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 b0 : B =>
   ap (projection E)
     (abses_pullback_inclusion_transpose_beta (inclusion E) F p b0) @
   (let X := fun E0 : AbSES' C B => pointed_fun (iscomplex_abses E0) in
    X E b0))
  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 (inverse_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
  tapply 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
       tapply 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))^$
  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))^$)^$ $@
(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))^$)^$) $==
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))^$)^$)) $==
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))^$)^$) $==
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))^$)^$) $o
p^$ $== abses_pullback_const' (abses_pullback_trivial_preimage E F p)
  apply equiv_ab_biprod_ind_homotopy.
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))^$)^$) $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))^$)^$) $o
  p^$).1 $o
 ab_biprod_inr ==
 (abses_pullback_const' (abses_pullback_trivial_preimage E F p)).1 $o
 ab_biprod_inr)
  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
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))
  |} (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
abses_pullback_inclusion_transpose_map (inclusion E) F p (- 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)) +
abses_pullback_inclusion_transpose_map (inclusion E) F p (- 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 - 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
0 = 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 Q0 : hfiber_abses_path X Y,
fmap (abses_pullback f) (Q0.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).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).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).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).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).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).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)
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)
abses_pullback_trivial_preimage E F p $-> (Y; Q).1 snapply (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 0) @ 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 0) @ 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 0) @ 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 0) @ 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) napply (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 0) @ 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 0) @ 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 0) @ 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 0) @ 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 0) @ 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 f0 : B =>
    ap (grp_pullback_pr1 (projection Y) (projection E))
      (induced_map_eq E F p (Y; Q) (ab_biprod_inr f0)) @
    (grp_unit_r (inclusion Y 0) @ 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 f0 : B =>
    ap (grp_pullback_pr1 (projection Y) (projection E))
      (induced_map_eq E F p (Y; Q) (ab_biprod_inr f0)) @
    (grp_unit_r (inclusion Y 0) @ 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
  tapply 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) $o
(Y.2).1
  tapply 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)
  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)
  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)).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)).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)).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)).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. *)
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.