From HoTT Require Import Basics Types.From HoTT Require Import Basics Types.
From HoTT.WildCat Require Import Core Opposite Equiv Bifunctor.
Require Import Pointed.Core Pointed.pTrunc Pointed.pEquiv
  Modalities.ReflectiveSubuniverse Truncations.Core Truncations.SeparatedTrunc
  AbGroups Homotopy.ExactSequence Spaces.Int Spaces.FreeInt.
From HoTT.Algebra.AbSES Require Import Core Pullback Pushout BaerSum
  Ext PullbackFiberSequence.
Require Import HSet.

(** * The contravariant six-term sequence of Ext *)

(** We construct the contravariant six-term exact sequence of Ext groups associated to any short exact sequence [A -> E -> B] and coefficient group [G]. The existence of this exact sequence follows from the final result in [PullbackFiberSequence]. However, with that definition it becomes a bit tricky to show that the connecting map is given by pushing out [E]. Instead, we give a direct proof.

  As an application, we use the six-term exact sequence to show that [Ext Z/n A] is isomorphic to [A/n], for nonzero natural numbers [n]. (See [ext_cyclic_ab].) *)

(** Exactness of [0 -> ab_hom B G -> ab_hom E G] follows from the rightmost map being an embedding. *)
Definition isexact_abses_sixterm_i `{Funext}
  {B A G : AbGroup} (E : AbSES B A)
  : IsExact (Tr (-1))
      (pconst : pUnit ->* ab_hom B G)
      (fmap10 (A:=Group^op) ab_hom (projection E) G).
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1)) (pconst : pUnit ->* ab_hom B G)
  (fmap10 ab_hom (projection E) G)
Proof.
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1)) (pconst : pUnit ->* ab_hom B G)
  (fmap10 ab_hom (projection E) G)
  apply isexact_purely_O.
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsExact Identity.purely pconst (fmap10 ab_hom (projection E) G)
  rapply isexact_homotopic_i.
H: Funext
B, A, G: AbGroup
E: AbSES B A
pconst ==* ?Goal
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsExact Identity.purely ?Goal (fmap10 ab_hom (projection E) G)
  2: apply iff_grp_isexact_isembedding.
H: Funext
B, A, G: AbGroup
E: AbSES B A
pconst ==* grp_trivial_rec (ab_hom B G)
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsEmbedding (fmap10 ab_hom (projection E) G)
  1: by apply phomotopy_homotopy_hset.
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsEmbedding (fmap10 ab_hom (projection E) G)
  exact _. (* [isembedding_precompose_surjection_ab] *)
Defined.

(** Exactness of [ab_hom B G -> ab_hom E G -> ab_hom A G]. One can also deduce this from [isexact_abses_pullback]. *)
Definition isexact_ext_contra_sixterm_ii `{Funext}
  {B A G : AbGroup} (E : AbSES B A)
  : IsExact (Tr (-1))
      (fmap10 (A:=Group^op) ab_hom (projection E) G)
      (fmap10 (A:=Group^op) ab_hom (inclusion E) G).
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1)) (fmap10 ab_hom (projection E) G)
  (fmap10 ab_hom (inclusion E) G)
Proof.
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1)) (fmap10 ab_hom (projection E) G)
  (fmap10 ab_hom (inclusion E) G)
  snapply Build_IsExact.
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsComplex (fmap10 ab_hom (projection E) G) (fmap10 ab_hom (inclusion E) G)
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsConnMap (Tr (-1)) (cxfib ?cx_isexact)
  {
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsComplex (fmap10 ab_hom (projection E) G) (fmap10 ab_hom (inclusion E) G) apply phomotopy_homotopy_hset; intro f.
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom B G
(fmap10 ab_hom (inclusion E) G o* fmap10 ab_hom (projection E) G) f =
pconst f
    apply equiv_path_grouphomomorphism; intro b; cbn.
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom B G
b: A
f (projection E (inclusion E b)) = group_unit
    refine (ap f _ @ grp_homo_unit f).
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom B G
b: A
projection E (inclusion E b) = mon_unit
    apply isexact_inclusion_projection. }
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsConnMap (Tr (-1))
  (cxfib
     (phomotopy_homotopy_hset
        ((fun f : ab_hom B G =>
          let X := equiv_fun equiv_path_grouphomomorphism in
          X
            ((fun b : A =>
              ap f
                (let X0 := fun a : AbSES' B A => cx_isexact in
                 let X1 := fun a : AbSES' B A => pointed_fun (X0 a) in X1 E b) @
              grp_homo_unit f
              :
              (fmap10 ab_hom (inclusion E) G
               o* fmap10 ab_hom (projection E) G) f b =
              pconst f b)
             :
             (fmap10 ab_hom (inclusion E) G o* fmap10 ab_hom (projection E) G)
               f ==
             pconst f))
         :
         fmap10 ab_hom (inclusion E) G o* fmap10 ab_hom (projection E) G ==
         pconst)))
  hnf.
H: Funext
B, A, G: AbGroup
E: AbSES B A
forall b : pFiber.pfiber (fmap10 ab_hom (inclusion E) G),
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun f : ab_hom B G =>
            let X := equiv_fun equiv_path_grouphomomorphism in
            X
              (fun b0 : A =>
               ap f
                 (let X0 := fun a : AbSES' B A => cx_isexact in
                  let X1 := fun a : AbSES' B A => pointed_fun (X0 a) in
                  X1 E b0) @
               grp_homo_unit f))))
     b) intros [f q]; rapply contr_inhabited_hprop.
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun f0 : ab_hom B G =>
            let X := equiv_fun equiv_path_grouphomomorphism in
            X
              (fun b : A =>
               ap f0
                 (let X0 := fun a : AbSES' B A => cx_isexact in
                  let X1 := fun a : AbSES' B A => pointed_fun (X0 a) in
                  X1 E b) @
               grp_homo_unit f0))))
     (f; q))
  srefine (tr (_; _)).
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
ab_hom B G
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
(fun x : ab_hom B G =>
 cxfib
   (phomotopy_homotopy_hset
      (fun f0 : ab_hom B G =>
       let X := equiv_fun equiv_path_grouphomomorphism in
       X
         (fun b : A =>
          ap f0
            (let X0 := fun a : AbSES' B A => cx_isexact in
             let X1 := fun a : AbSES' B A => pointed_fun (X0 a) in X1 E b) @
          grp_homo_unit f0)))
   x =
 (f; q)) ?proj1
  {
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
ab_hom B G refine (grp_homo_compose _ (abses_cokernel_iso (inclusion E) (projection E))^-1$).
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
GroupHomomorphism (ab_cokernel (inclusion E)) G
    apply (quotient_abgroup_rec _ _ f).
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
forall n : E, grp_image (inclusion E) n -> f n = mon_unit
    intros e; rapply Trunc_ind.
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
e: E
{x : A & inclusion E x = e} -> f e = mon_unit
    intros [b r].
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
e: E
b: A
r: inclusion E b = e
f e = mon_unit
    refine (ap f r^ @ _).
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
e: E
b: A
r: inclusion E b = e
f (inclusion E b) = mon_unit
    exact (equiv_path_grouphomomorphism^-1 q _). }
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
(fun x : ab_hom B G =>
 cxfib
   (phomotopy_homotopy_hset
      (fun f0 : ab_hom B G =>
       let X := equiv_fun equiv_path_grouphomomorphism in
       X
         (fun b : A =>
          ap f0
            (let X0 := fun a : AbSES' B A => cx_isexact in
             let X1 := fun a : AbSES' B A => pointed_fun (X0 a) in X1 E b) @
          grp_homo_unit f0)))
   x =
 (f; q))
  (grp_homo_compose
     (quotient_abgroup_rec (grp_image (inclusion E)) G f
        (fun e : E =>
         Trunc_ind
           (fun _ : Trunc (-1) {x : A & inclusion E x = e} => f e = mon_unit)
           (fun a : {x : A & inclusion E x = e} =>
            (fun (b : A) (r : inclusion E b = e) =>
             ap f r^ @ equiv_path_grouphomomorphism^-1 q b) a.1 a.2)))
     (abses_cokernel_iso (inclusion E) (projection E))^-1$)
  lazy beta.
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
cxfib
  (phomotopy_homotopy_hset
     (fun f0 : ab_hom B G =>
      let X := equiv_fun equiv_path_grouphomomorphism in
      X
        (fun b : A =>
         ap f0
           (let X0 := fun a : AbSES' B A => cx_isexact in
            let X1 := fun a : AbSES' B A => pointed_fun (X0 a) in X1 E b) @
         grp_homo_unit f0)))
  (grp_homo_compose
     (quotient_abgroup_rec (grp_image (inclusion E)) G f
        (fun e : E =>
         Trunc_ind
           (fun _ : Trunc (-1) {x : A & inclusion E x = e} => f e = mon_unit)
           (fun a : {x : A & inclusion E x = e} =>
            ap f (a.2)^ @ equiv_path_grouphomomorphism^-1 q a.1)))
     (abses_cokernel_iso (inclusion E) (projection E))^-1$) =
(f; q)
  apply path_sigma_hprop.
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
(cxfib
   (phomotopy_homotopy_hset
      (fun f0 : ab_hom B G =>
       let X := equiv_fun equiv_path_grouphomomorphism in
       X
         (fun b : A =>
          ap f0
            (let X0 := fun a : AbSES' B A => cx_isexact in
             let X1 := fun a : AbSES' B A => pointed_fun (X0 a) in X1 E b) @
          grp_homo_unit f0)))
   (grp_homo_compose
      (quotient_abgroup_rec (grp_image (inclusion E)) G f
         (fun e : E =>
          Trunc_ind
            (fun _ : Trunc (-1) {x : A & inclusion E x = e} => f e = mon_unit)
            (fun a : {x : A & inclusion E x = e} =>
             ap f (a.2)^ @ equiv_path_grouphomomorphism^-1 q a.1)))
      (abses_cokernel_iso (inclusion E) (projection E))^-1$)).1 =
(f; q).1
  apply equiv_path_grouphomomorphism; unfold pr1.
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
(cxfib
   (phomotopy_homotopy_hset
      (fun f0 : ab_hom B G =>
       equiv_path_grouphomomorphism
         (fun b : A => ap f0 (cx_isexact b) @ grp_homo_unit f0)))
   (grp_homo_compose
      (quotient_abgroup_rec (grp_image (inclusion E)) G f
         (fun e : E =>
          Trunc_ind
            (fun _ : Trunc (-1) {x : A & inclusion E x = e} => f e = mon_unit)
            (fun a : {x : A & inclusion E x = e} =>
             ap f (a.2)^ @ equiv_path_grouphomomorphism^-1 q a.1)))
      (abses_cokernel_iso (inclusion E) (projection E))^-1$)).1 ==
f
  intro x.
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
x: E
(cxfib
   (phomotopy_homotopy_hset
      (fun f0 : ab_hom B G =>
       equiv_path_grouphomomorphism
         (fun b : A => ap f0 (cx_isexact b) @ grp_homo_unit f0)))
   (grp_homo_compose
      (quotient_abgroup_rec (grp_image (inclusion E)) G f
         (fun e : E =>
          Trunc_ind
            (fun _ : Trunc (-1) {x0 : A & inclusion E x0 = e} =>
             f e = mon_unit)
            (fun a : {x0 : A & inclusion E x0 = e} =>
             ap f (a.2)^ @ equiv_path_grouphomomorphism^-1 q a.1)))
      (abses_cokernel_iso (inclusion E) (projection E))^-1$)).1
  x =
f x
  exact (ap (quotient_abgroup_rec _ _ f _)
            (abses_cokernel_iso_inv_beta _ _ _)).
Defined.

(** *** Exactness of [ab_hom E G -> ab_hom A G -> Ext B G] *)

(** If a pushout [abses_pushout alpha E] is trivial, then [alpha] factors through [inclusion E]. *)
Lemma abses_pushout_trivial_factors_inclusion `{Univalence}
  {B A A' : AbGroup} (alpha : A $-> A') (E : AbSES B A)
  : abses_pushout alpha E = pt -> exists phi, alpha = phi $o inclusion E.
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
abses_pushout alpha E = pt -> {phi : E $-> A' & alpha = phi $o inclusion E}
Proof.
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
abses_pushout alpha E = pt -> {phi : E $-> A' & alpha = phi $o inclusion E}
  equiv_intros (equiv_path_abses (E:=abses_pushout alpha E) (F:=pt)) p.
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
p: abses_path_data (abses_pushout alpha E) pt
{phi : E $-> A' & alpha = phi $o inclusion E}
  destruct p as [phi [p q]].
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: abses_pushout alpha E $-> pt
p: phi $o inclusion (abses_pushout alpha E) == inclusion pt
q: projection (abses_pushout alpha E) == projection pt $o phi
{phi0 : E $-> A' & alpha = phi0 $o inclusion E}
  exists (ab_biprod_pr1 $o phi $o ab_pushout_inr).
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: abses_pushout alpha E $-> pt
p: phi $o inclusion (abses_pushout alpha E) == inclusion pt
q: projection (abses_pushout alpha E) == projection pt $o phi
alpha = ab_biprod_pr1 $o phi $o ab_pushout_inr $o inclusion E
  apply equiv_path_grouphomomorphism; intro a.
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: abses_pushout alpha E $-> pt
p: phi $o inclusion (abses_pushout alpha E) == inclusion pt
q: projection (abses_pushout alpha E) == projection pt $o phi
a: A
alpha a = (ab_biprod_pr1 $o phi $o ab_pushout_inr $o inclusion E) a
  (* We embed into the biproduct and prove equality there. *)
  apply (isinj_embedding (@ab_biprod_inl A' B) _).
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: abses_pushout alpha E $-> pt
p: phi $o inclusion (abses_pushout alpha E) == inclusion pt
q: projection (abses_pushout alpha E) == projection pt $o phi
a: A
ab_biprod_inl (alpha a) =
ab_biprod_inl ((ab_biprod_pr1 $o phi $o ab_pushout_inr $o inclusion E) a)
  refine ((p (alpha a))^ @ _).
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: abses_pushout alpha E $-> pt
p: phi $o inclusion (abses_pushout alpha E) == inclusion pt
q: projection (abses_pushout alpha E) == projection pt $o phi
a: A
(phi $o inclusion (abses_pushout alpha E)) (alpha a) =
ab_biprod_inl ((ab_biprod_pr1 $o phi $o ab_pushout_inr $o inclusion E) a)
  refine (ap phi _ @ _).
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: abses_pushout alpha E $-> pt
p: phi $o inclusion (abses_pushout alpha E) == inclusion pt
q: projection (abses_pushout alpha E) == projection pt $o phi
a: A
inclusion (abses_pushout alpha E) (alpha a) = ?Goal
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: abses_pushout alpha E $-> pt
p: phi $o inclusion (abses_pushout alpha E) == inclusion pt
q: projection (abses_pushout alpha E) == projection pt $o phi
a: A
phi ?Goal =
ab_biprod_inl ((ab_biprod_pr1 $o phi $o ab_pushout_inr $o inclusion E) a)
  1: exact (left_square (abses_pushout_morphism E alpha) a).
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: abses_pushout alpha E $-> pt
p: phi $o inclusion (abses_pushout alpha E) == inclusion pt
q: projection (abses_pushout alpha E) == projection pt $o phi
a: A
phi ((component2 (abses_pushout_morphism E alpha) $o inclusion E) a) =
ab_biprod_inl ((ab_biprod_pr1 $o phi $o ab_pushout_inr $o inclusion E) a)
  apply (path_prod' idpath).
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: abses_pushout alpha E $-> pt
p: phi $o inclusion (abses_pushout alpha E) == inclusion pt
q: projection (abses_pushout alpha E) == projection pt $o phi
a: A
snd (phi ((component2 (abses_pushout_morphism E alpha) $o inclusion E) a)) =
grp_homo_const ((ab_biprod_pr1 $o phi $o ab_pushout_inr $o inclusion E) a)
  refine ((q _)^ @ _).
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: abses_pushout alpha E $-> pt
p: phi $o inclusion (abses_pushout alpha E) == inclusion pt
q: projection (abses_pushout alpha E) == projection pt $o phi
a: A
projection (abses_pushout alpha E)
  ((component2 (abses_pushout_morphism E alpha) $o inclusion E) a) =
grp_homo_const ((ab_biprod_pr1 $o phi $o ab_pushout_inr $o inclusion E) a)
  refine (right_square (abses_pushout_morphism E alpha) _ @ _); cbn.
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: abses_pushout alpha E $-> pt
p: phi $o inclusion (abses_pushout alpha E) == inclusion pt
q: projection (abses_pushout alpha E) == projection pt $o phi
a: A
projection E (inclusion E a) = group_unit
  apply isexact_inclusion_projection.
Defined.

Instance isexact_ext_contra_sixterm_iii@{u v +} `{Univalence}
  {B A G : AbGroup@{u}} (E : AbSES@{u v} B A)
  : IsExact (Tr (-1))
      (fmap10 (A:=Group^op) ab_hom (inclusion E) G)
      (abses_pushout_ext E).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1)) (fmap10 ab_hom (inclusion E) G) (abses_pushout_ext E)
Proof.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1)) (fmap10 ab_hom (inclusion E) G) (abses_pushout_ext E)
  snapply Build_IsExact.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsComplex (fmap10 ab_hom (inclusion E) G) (abses_pushout_ext E)
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsConnMap (Tr (-1)) (cxfib ?cx_isexact)
  -
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsComplex (fmap10 ab_hom (inclusion E) G) (abses_pushout_ext E) apply phomotopy_homotopy_hset; intro g; cbn.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
g: ab_hom E G
tr (abses_pushout (grp_homo_compose g (inclusion E)) E) = tr ispointed_abses
    (* this equation holds purely *)
    apply (ap tr@{v}).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
g: ab_hom E G
abses_pushout (grp_homo_compose g (inclusion E)) E = ispointed_abses
    refine (abses_pushout_compose _ _ _ @ ap _ _ @ _).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
g: ab_hom E G
abses_pushout (inclusion E) E = ?Goal
H: Univalence
B, A, G: AbGroup
E: AbSES B A
g: ab_hom E G
abses_pushout g ?Goal = ispointed_abses
    1: apply abses_pushout_inclusion.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
g: ab_hom E G
abses_pushout g pt = ispointed_abses
    apply abses_pushout_point.
  -
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsConnMap (Tr (-1))
  (cxfib
     (phomotopy_homotopy_hset
        ((fun g : ab_hom E G =>
          ap tr
            ((abses_pushout_compose (inclusion E) g E @
              ap (abses_pushout g) (abses_pushout_inclusion E)) @
             abses_pushout_point g)
          :
          (abses_pushout_ext E o* fmap10 ab_hom (inclusion E) G) g = pconst g)
         :
         abses_pushout_ext E o* fmap10 ab_hom (inclusion E) G == pconst))) intros [F p].
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: ab_hom A G
p: abses_pushout_ext E F = pt
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun g : ab_hom E G =>
            ap tr
              ((abses_pushout_compose (inclusion E) g E @
                ap (abses_pushout g) (abses_pushout_inclusion E)) @
               abses_pushout_point g))))
     (F; p))
    (* since we are proving a proposition, we may convert [p] to an actual path *)
    pose proof (p' := (equiv_path_Tr _ _)^-1 p).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: ab_hom A G
p: abses_pushout_ext E F = pt
p': Tr (-1) (fmap ((AbSES' : AbGroup^op -> AbGroup -> Type) B) F E = pt)
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun g : ab_hom E G =>
            ap tr
              ((abses_pushout_compose (inclusion E) g E @
                ap (abses_pushout g) (abses_pushout_inclusion E)) @
               abses_pushout_point g))))
     (F; p))
    (* slightly faster than [strip_truncations]: *)
    revert p'; apply Trunc_rec; intro p'.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: ab_hom A G
p: abses_pushout_ext E F = pt
p': fmap ((AbSES' : AbGroup^op -> AbGroup -> Type) B) F E = pt
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun g : ab_hom E G =>
            ap tr
              ((abses_pushout_compose (inclusion E) g E @
                ap (abses_pushout g) (abses_pushout_inclusion E)) @
               abses_pushout_point g))))
     (F; p))
    rapply contr_inhabited_hprop; apply tr.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: ab_hom A G
p: abses_pushout_ext E F = pt
p': fmap ((AbSES' : AbGroup^op -> AbGroup -> Type) B) F E = pt
hfiber
  (cxfib
     (phomotopy_homotopy_hset
        (fun g : ab_hom E G =>
         ap tr
           ((abses_pushout_compose (inclusion E) g E @
             ap (abses_pushout g) (abses_pushout_inclusion E)) @
            abses_pushout_point g))))
  (F; p)
    (* now we construct a preimage *)
    pose (g := abses_pushout_trivial_factors_inclusion _ E p');
      destruct g as [g k].
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: ab_hom A G
p: abses_pushout_ext E F = pt
p': fmap ((AbSES' : AbGroup^op -> AbGroup -> Type) B) F E = pt
g: E $-> G
k: F = g $o inclusion E
hfiber
  (cxfib
     (phomotopy_homotopy_hset
        (fun g0 : ab_hom E G =>
         ap tr
           ((abses_pushout_compose (inclusion E) g0 E @
             ap (abses_pushout g0) (abses_pushout_inclusion E)) @
            abses_pushout_point g0))))
  (F; p)
    exists g.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: ab_hom A G
p: abses_pushout_ext E F = pt
p': fmap ((AbSES' : AbGroup^op -> AbGroup -> Type) B) F E = pt
g: E $-> G
k: F = g $o inclusion E
cxfib
  (phomotopy_homotopy_hset
     (fun g0 : ab_hom E G =>
      ap tr
        ((abses_pushout_compose (inclusion E) g0 E @
          ap (abses_pushout g0) (abses_pushout_inclusion E)) @
         abses_pushout_point g0)))
  g =
(F; p)
    apply path_sigma_hprop; cbn.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: ab_hom A G
p: abses_pushout_ext E F = pt
p': fmap ((AbSES' : AbGroup^op -> AbGroup -> Type) B) F E = pt
g: E $-> G
k: F = g $o inclusion E
grp_homo_compose g (inclusion E) = F
    exact k^.
Defined.

(** *** Exactness of [ab_hom A G -> Ext1 B G -> Ext1 E G]. *)

(** We construct a morphism which witnesses exactness. *)
Definition isexact_ext_contra_sixterm_iv_mor `{Univalence}
  {B A G : AbGroup} (E : AbSES B A)
  (F : AbSES B G) (p : abses_pullback (projection E) F = pt)
  : AbSESMorphism E F.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
AbSESMorphism E F
Proof.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
AbSESMorphism E F
  pose (p' := equiv_path_abses^-1 p^);
    destruct p' as [p' [pl pr]].
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': pt $-> abses_pullback (projection E) F
pl: p' $o inclusion pt == inclusion (abses_pullback (projection E) F)
pr: projection pt == projection (abses_pullback (projection E) F) $o p'
AbSESMorphism E F
  srefine (Build_AbSESMorphism _ _ grp_homo_id _ _).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': pt $-> abses_pullback (projection E) F
pl: p' $o inclusion pt == inclusion (abses_pullback (projection E) F)
pr: projection pt == projection (abses_pullback (projection E) F) $o p'
A $-> G
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': pt $-> abses_pullback (projection E) F
pl: p' $o inclusion pt == inclusion (abses_pullback (projection E) F)
pr: projection pt == projection (abses_pullback (projection E) F) $o p'
E $-> F
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': pt $-> abses_pullback (projection E) F
pl: p' $o inclusion pt == inclusion (abses_pullback (projection E) F)
pr: projection pt == projection (abses_pullback (projection E) F) $o p'
inclusion F $o ?component1 == ?component2 $o inclusion E
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': pt $-> abses_pullback (projection E) F
pl: p' $o inclusion pt == inclusion (abses_pullback (projection E) F)
pr: projection pt == projection (abses_pullback (projection E) F) $o p'
projection F $o ?component2 == grp_homo_id $o projection E
  -
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': pt $-> abses_pullback (projection E) F
pl: p' $o inclusion pt == inclusion (abses_pullback (projection E) F)
pr: projection pt == projection (abses_pullback (projection E) F) $o p'
A $-> G refine (grp_homo_compose
              (grp_iso_inverse
                 (abses_kernel_iso (inclusion F) (projection F))) _).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': pt $-> abses_pullback (projection E) F
pl: p' $o inclusion pt == inclusion (abses_pullback (projection E) F)
pr: projection pt == projection (abses_pullback (projection E) F) $o p'
GroupHomomorphism A (ab_kernel (projection F))
    (* now it's easy to construct map into the kernel *)
    snapply grp_kernel_corec.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': pt $-> abses_pullback (projection E) F
pl: p' $o inclusion pt == inclusion (abses_pullback (projection E) F)
pr: projection pt == projection (abses_pullback (projection E) F) $o p'
A $-> F
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': pt $-> abses_pullback (projection E) F
pl: p' $o inclusion pt == inclusion (abses_pullback (projection E) F)
pr: projection pt == projection (abses_pullback (projection E) F) $o p'
projection F $o ?g == grp_homo_const
    1: exact (grp_pullback_pr1 _ _ $o p' $o ab_biprod_inr $o inclusion E).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': pt $-> abses_pullback (projection E) F
pl: p' $o inclusion pt == inclusion (abses_pullback (projection E) F)
pr: projection pt == projection (abses_pullback (projection E) F) $o p'
projection F $o
(grp_pullback_pr1 (projection F) (projection E) $o p' $o ab_biprod_inr $o
 inclusion E) ==
grp_homo_const
    intro x.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': pt $-> abses_pullback (projection E) F
pl: p' $o inclusion pt == inclusion (abses_pullback (projection E) F)
pr: projection pt == projection (abses_pullback (projection E) F) $o p'
x: A
(projection F $o
 (grp_pullback_pr1 (projection F) (projection E) $o p' $o ab_biprod_inr $o
  inclusion E)) x =
grp_homo_const x
    refine (right_square (abses_pullback_morphism F _) _ @ _).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': pt $-> abses_pullback (projection E) F
pl: p' $o inclusion pt == inclusion (abses_pullback (projection E) F)
pr: projection pt == projection (abses_pullback (projection E) F) $o p'
x: A
(component3 (abses_pullback_morphism F (projection E)) $o
 projection (abses_pullback (projection E) F))
  (p' (ab_biprod_inr (inclusion E x))) =
grp_homo_const x
    refine (ap (projection E) (pr _)^ @ _); cbn.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': pt $-> abses_pullback (projection E) F
pl: p' $o inclusion pt == inclusion (abses_pullback (projection E) F)
pr: projection pt == projection (abses_pullback (projection E) F) $o p'
x: A
projection E (inclusion E x) = group_unit
    apply isexact_inclusion_projection.
  -
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': pt $-> abses_pullback (projection E) F
pl: p' $o inclusion pt == inclusion (abses_pullback (projection E) F)
pr: projection pt == projection (abses_pullback (projection E) F) $o p'
E $-> F exact (grp_pullback_pr1 _ _ $o p' $o ab_biprod_inr).
  -
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': pt $-> abses_pullback (projection E) F
pl: p' $o inclusion pt == inclusion (abses_pullback (projection E) F)
pr: projection pt == projection (abses_pullback (projection E) F) $o p'
inclusion F $o
grp_homo_compose
  (grp_iso_inverse (abses_kernel_iso (inclusion F) (projection F)))
  (grp_kernel_corec
     (grp_pullback_pr1 (projection F) (projection E) $o p' $o ab_biprod_inr $o
      inclusion E)
     ((fun x : A =>
       right_square (abses_pullback_morphism F (projection E))
         (p' (ab_biprod_inr (inclusion E x))) @
       (ap (projection E) (pr (ab_biprod_inr (inclusion E x)))^ @
        ((let X := fun a : AbSES' B A => cx_isexact in
          let X0 := fun a : AbSES' B A => pointed_fun (X a) in X0 E x)
         :
         projection E (projection pt (ab_biprod_inr (inclusion E x))) =
         grp_homo_const x)))
      :
      projection F $o
      (grp_pullback_pr1 (projection F) (projection E) $o p' $o ab_biprod_inr $o
       inclusion E) ==
      grp_homo_const)) ==
grp_pullback_pr1 (projection F) (projection E) $o p' $o ab_biprod_inr $o
inclusion E intro a.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': pt $-> abses_pullback (projection E) F
pl: p' $o inclusion pt == inclusion (abses_pullback (projection E) F)
pr: projection pt == projection (abses_pullback (projection E) F) $o p'
a: A
(inclusion F $o
 grp_homo_compose
   (grp_iso_inverse (abses_kernel_iso (inclusion F) (projection F)))
   (grp_kernel_corec
      (grp_pullback_pr1 (projection F) (projection E) $o p' $o ab_biprod_inr $o
       inclusion E)
      (fun x : A =>
       right_square (abses_pullback_morphism F (projection E))
         (p' (ab_biprod_inr (inclusion E x))) @
       (ap (projection E) (pr (ab_biprod_inr (inclusion E x)))^ @
        (let X := fun a0 : AbSES' B A => cx_isexact in
         let X0 := fun a0 : AbSES' B A => pointed_fun (X a0) in X0 E x)))))
  a =
(grp_pullback_pr1 (projection F) (projection E) $o p' $o ab_biprod_inr $o
 inclusion E) a
    napply abses_kernel_iso_inv_beta.
  -
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': pt $-> abses_pullback (projection E) F
pl: p' $o inclusion pt == inclusion (abses_pullback (projection E) F)
pr: projection pt == projection (abses_pullback (projection E) F) $o p'
projection F $o
(grp_pullback_pr1 (projection F) (projection E) $o p' $o ab_biprod_inr) ==
grp_homo_id $o projection E intro e.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': pt $-> abses_pullback (projection E) F
pl: p' $o inclusion pt == inclusion (abses_pullback (projection E) F)
pr: projection pt == projection (abses_pullback (projection E) F) $o p'
e: E
(projection F $o
 (grp_pullback_pr1 (projection F) (projection E) $o p' $o ab_biprod_inr)) e =
(grp_homo_id $o projection E) e
    refine (right_square (abses_pullback_morphism F _) _
              @ ap (projection E) _).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': pt $-> abses_pullback (projection E) F
pl: p' $o inclusion pt == inclusion (abses_pullback (projection E) F)
pr: projection pt == projection (abses_pullback (projection E) F) $o p'
e: E
projection (abses_pullback (projection E) F) (p' (ab_biprod_inr e)) = e
    exact (pr _)^.
Defined.

Instance isexact_ext_contra_sixterm_iv `{Univalence}
  {B A G : AbGroup@{u}} (E : AbSES@{u v} B A)
  : IsExact (Tr (-1)) (abses_pushout_ext E)
      (fmap (pTr 0) (abses_pullback_pmap (A:=G) (projection E))).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1)) (abses_pushout_ext E)
  (fmap (pTr 0) (abses_pullback_pmap (projection E)))
Proof.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1)) (abses_pushout_ext E)
  (fmap (pTr 0) (abses_pullback_pmap (projection E)))
  snapply Build_IsExact.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsComplex (abses_pushout_ext E)
  (fmap (pTr 0) (abses_pullback_pmap (projection E)))
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsConnMap (Tr (-1)) (cxfib ?cx_isexact)
  -
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsComplex (abses_pushout_ext E)
  (fmap (pTr 0) (abses_pullback_pmap (projection E))) apply phomotopy_homotopy_hset; intro g; cbn.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
g: ab_hom A G
tr (abses_pullback (projection E) (abses_pushout g E)) = tr ispointed_abses
    (* this equation holds purely *)
    apply (ap tr@{v}).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
g: ab_hom A G
abses_pullback (projection E) (abses_pushout g E) = ispointed_abses
    refine ((abses_pushout_pullback_reorder _ _ _)^
              @ ap _ _ @ _).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
g: ab_hom A G
abses_pullback (projection E) E = ?Goal
H: Univalence
B, A, G: AbGroup
E: AbSES B A
g: ab_hom A G
abses_pushout g ?Goal = ispointed_abses
    1: exact (abses_pullback_projection _)^.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
g: ab_hom A G
abses_pushout g pt = ispointed_abses
    apply abses_pushout_point.
  (* since we are proving a proposition, we may convert [p] to an actual path *)
  -
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsConnMap (Tr (-1))
  (cxfib
     (phomotopy_homotopy_hset
        ((fun g : ab_hom A G =>
          ap tr
            (((abses_pushout_pullback_reorder E g (projection E))^ @
              ap (abses_pushout g) (abses_pullback_projection E)^) @
             abses_pushout_point g)
          :
          (fmap (pTr 0) (abses_pullback_pmap (projection E))
           o* abses_pushout_ext E) g =
          pconst g)
         :
         fmap (pTr 0) (abses_pullback_pmap (projection E))
         o* abses_pushout_ext E == pconst))) intros [F p].
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: ab_ext B G
p: fmap (pTr 0) (abses_pullback_pmap (projection E)) F = pt
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun g : ab_hom A G =>
            ap tr
              (((abses_pushout_pullback_reorder E g (projection E))^ @
                ap (abses_pushout g) (abses_pullback_projection E)^) @
               abses_pushout_point g))))
     (F; p))
    revert dependent F; napply (Trunc_ind (n:=0) (A:=AbSES B G)).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
forall aa : Trunc 0 (AbSES B G),
IsHSet
  (forall p : fmap (pTr 0) (abses_pullback_pmap (projection E)) aa = pt,
   IsConnected (Tr (-1))
     (hfiber
        (cxfib
           (phomotopy_homotopy_hset
              (fun g : ab_hom A G =>
               ap tr
                 (((abses_pushout_pullback_reorder E g (projection E))^ @
                   ap (abses_pushout g) (abses_pullback_projection E)^) @
                  abses_pushout_point g))))
        (aa; p)))
H: Univalence
B, A, G: AbGroup
E: AbSES B A
forall (a : AbSES B G)
(p : fmap (pTr 0) (abses_pullback_pmap (projection E)) (tr a) = pt),
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun g : ab_hom A G =>
            ap tr
              (((abses_pushout_pullback_reorder E g (projection E))^ @
                ap (abses_pushout g) (abses_pullback_projection E)^) @
               abses_pushout_point g))))
     (tr a; p))
    (* [exact _.] works here, but is slow. *)
    {
H: Univalence
B, A, G: AbGroup
E: AbSES B A
forall aa : Trunc 0 (AbSES B G),
IsHSet
  (forall p : fmap (pTr 0) (abses_pullback_pmap (projection E)) aa = pt,
   IsConnected (Tr (-1))
     (hfiber
        (cxfib
           (phomotopy_homotopy_hset
              (fun g : ab_hom A G =>
               ap tr
                 (((abses_pushout_pullback_reorder E g (projection E))^ @
                   ap (abses_pushout g) (abses_pullback_projection E)^) @
                  abses_pushout_point g))))
        (aa; p))) intro x; napply istrunc_forall.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
x: Trunc 0 (AbSES B G)
forall a : fmap (pTr 0) (abses_pullback_pmap (projection E)) x = pt,
IsHSet
  (IsConnected (Tr (-1))
     (hfiber
        (cxfib
           (phomotopy_homotopy_hset
              (fun g : ab_hom A G =>
               ap tr
                 (((abses_pushout_pullback_reorder E g (projection E))^ @
                   ap (abses_pushout g) (abses_pullback_projection E)^) @
                  abses_pushout_point g))))
        (x; a)))
      intro y; exact (istrunc_leq (trunc_index_leq_succ _)). }
H: Univalence
B, A, G: AbGroup
E: AbSES B A
forall (a : AbSES B G)
(p : fmap (pTr 0) (abses_pullback_pmap (projection E)) (tr a) = pt),
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun g : ab_hom A G =>
            ap tr
              (((abses_pushout_pullback_reorder E g (projection E))^ @
                ap (abses_pushout g) (abses_pullback_projection E)^) @
               abses_pushout_point g))))
     (tr a; p))
    intro F.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
forall p : fmap (pTr 0) (abses_pullback_pmap (projection E)) (tr F) = pt,
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun g : ab_hom A G =>
            ap tr
              (((abses_pushout_pullback_reorder E g (projection E))^ @
                ap (abses_pushout g) (abses_pullback_projection E)^) @
               abses_pushout_point g))))
     (tr F; p))
    equiv_intros (equiv_path_Tr (n:=-1) (abses_pullback (projection E) F) pt) p.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: Tr (-1) (abses_pullback (projection E) F = pt)
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun g : ab_hom A G =>
            ap tr
              (((abses_pushout_pullback_reorder E g (projection E))^ @
                ap (abses_pushout g) (abses_pullback_projection E)^) @
               abses_pushout_point g))))
     (tr F; equiv_path_Tr (abses_pullback (projection E) F) pt p))
    strip_truncations.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun g : ab_hom A G =>
            ap tr
              (((abses_pushout_pullback_reorder E g (projection E))^ @
                ap (abses_pushout g) (abses_pullback_projection E)^) @
               abses_pushout_point g))))
     (tr F; equiv_path_Tr (abses_pullback (projection E) F) pt (tr p)))
    rapply contr_inhabited_hprop; apply tr.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
hfiber
  (cxfib
     (phomotopy_homotopy_hset
        (fun g : ab_hom A G =>
         ap tr
           (((abses_pushout_pullback_reorder E g (projection E))^ @
             ap (abses_pushout g) (abses_pullback_projection E)^) @
            abses_pushout_point g))))
  (tr F; equiv_path_Tr (abses_pullback (projection E) F) pt (tr p))
    pose (g := isexact_ext_contra_sixterm_iv_mor E F p).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
g:= isexact_ext_contra_sixterm_iv_mor E F p: AbSESMorphism E F
hfiber
  (cxfib
     (phomotopy_homotopy_hset
        (fun g0 : ab_hom A G =>
         ap tr
           (((abses_pushout_pullback_reorder E g0 (projection E))^ @
             ap (abses_pushout g0) (abses_pullback_projection E)^) @
            abses_pushout_point g0))))
  (tr F; equiv_path_Tr (abses_pullback (projection E) F) pt (tr p))
    exists (component1 g).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
g:= isexact_ext_contra_sixterm_iv_mor E F p: AbSESMorphism E F
cxfib
  (phomotopy_homotopy_hset
     (fun g0 : ab_hom A G =>
      ap tr
        (((abses_pushout_pullback_reorder E g0 (projection E))^ @
          ap (abses_pushout g0) (abses_pullback_projection E)^) @
         abses_pushout_point g0)))
  (component1 g) =
(tr F; equiv_path_Tr (abses_pullback (projection E) F) pt (tr p))
    apply path_sigma_hprop, (ap tr).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
g:= isexact_ext_contra_sixterm_iv_mor E F p: AbSESMorphism E F
fmap ((AbSES' : AbGroup^op -> AbGroup -> Type) B) (component1 g) E = F
    by rapply (abses_pushout_component3_id g).
Defined.

(** *** Exactness of [Ext B G -> Ext E G -> Ext A G] *)

(** This is an immediate consequence of [isexact_abses_pullback]. *)
Instance isexact_ext_contra_sixterm_v `{Univalence}
  {B A G : AbGroup} (E : AbSES B A)
  : IsExact (Tr (-1))
      (fmap (pTr 0) (abses_pullback_pmap (A:=G) (projection E)))
      (fmap (pTr 0) (abses_pullback_pmap (A:=G) (inclusion E))).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1)) (fmap (pTr 0) (abses_pullback_pmap (projection E)))
  (fmap (pTr 0) (abses_pullback_pmap (inclusion E)))
Proof.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1)) (fmap (pTr 0) (abses_pullback_pmap (projection E)))
  (fmap (pTr 0) (abses_pullback_pmap (inclusion E)))
  rapply isexact_ptr.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1)) (abses_pullback_pmap (projection E))
  (abses_pullback_pmap (inclusion E))
  rapply isexact_purely_O.
Defined.

(** *** [Ext Z/n A] is isomorphic to [A/n] *)

(** An easy consequence of the contravariant six-term exact sequence is that [Ext Z/n A] is isomorphic to the cokernel of the multiplication-by-n endomorphism [A -> A], for any abelian group [A]. This falls out of the six-term exact sequence associated to [Z -> Z -> Z/n] and projectivity of [Z]. A minor point is that the library does not currently contain a proof that multiplication by a nonzero natural number is a self-injection of [Z]. Thus we work directly with the assumption that [Z1_mul_nat n] is an embedding. *)

(** We define our own cyclic groups using [ab_cokernel_embedding] under the assumption that [Z1_mul_nat n] is an embedding. *)
Definition cyclic' `{Funext} (n : nat) `{IsEmbedding (Z1_mul_nat n)}
  : AbGroup := ab_cokernel_embedding (Z1_mul_nat n).

(** We first show that [ab_hom Z A -> ab_hom Z A -> Ext (cyclic n) A] is exact. We could inline the proof below, but factoring it out is faster. *)
Local Definition isexact_ext_cyclic_ab_iii@{u v w | u < v, v < w} `{Univalence}
  (n : nat) `{IsEmbedding (Z1_mul_nat n)} {A : AbGroup@{u}}
  : IsExact (Tr (-1))
      (fmap10 (A:=Group^op) ab_hom (Z1_mul_nat n) A)
      (abses_pushout_ext (abses_from_inclusion (Z1_mul_nat n)))
  := isexact_ext_contra_sixterm_iii
       (abses_from_inclusion (Z1_mul_nat n)).

(** We show exactness of [A -> A -> Ext Z/n A] where the first map is multiplication by [n], but considered in universe [v]. *)
Local Definition ext_cyclic_exact@{u v w} `{Univalence}
  (n : nat) `{IsEmbedding (Z1_mul_nat n)} {A : AbGroup@{u}}
  : IsExact@{v v v v v} (Tr (-1))
      (ab_mul (A:=A) n)
      (abses_pushout_ext@{u w v} (abses_from_inclusion (Z1_mul_nat n))
         o* (pequiv_groupisomorphism (equiv_Z1_hom A))^-1*).
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
IsExact (Tr (-1)) (ab_mul n)
  (abses_pushout_ext (abses_from_inclusion (Z1_mul_nat n))
   o* (equiv_Z1_hom A)^-1*)
Proof.
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
IsExact (Tr (-1)) (ab_mul n)
  (abses_pushout_ext (abses_from_inclusion (Z1_mul_nat n))
   o* (equiv_Z1_hom A)^-1*)
  (* we first move [equiv_Z1_hom] across the total space *)
  apply moveL_isexact_equiv.
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
IsExact (Tr (-1)) ((equiv_Z1_hom A)^-1* o* ab_mul n)
  (abses_pushout_ext (abses_from_inclusion (Z1_mul_nat n)))
  (* now we change the left map so as to apply exactness at iii from above *)
  snapply (isexact_homotopic_i (Tr (-1))).
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
A ->* ab_hom ab_Z1 A
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
(equiv_Z1_hom A)^-1* o* ab_mul n ==* ?i
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
IsExact (Tr (-1)) ?i
  (abses_pushout_ext (abses_from_inclusion (Z1_mul_nat n)))
  1: exact (fmap10 (A:=Group^op) ab_hom (Z1_mul_nat n) A o*
              (pequiv_inverse
                 (pequiv_groupisomorphism (equiv_Z1_hom A)))).
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
(equiv_Z1_hom A)^-1* o* ab_mul n ==*
fmap10 ab_hom (Z1_mul_nat n) A o* pequiv_inverse (equiv_Z1_hom A)
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
IsExact (Tr (-1))
  (fmap10 ab_hom (Z1_mul_nat n) A o* pequiv_inverse (equiv_Z1_hom A))
  (abses_pushout_ext (abses_from_inclusion (Z1_mul_nat n)))
  -
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
(equiv_Z1_hom A)^-1* o* ab_mul n ==*
fmap10 ab_hom (Z1_mul_nat n) A o* pequiv_inverse (equiv_Z1_hom A) apply phomotopy_homotopy_hset.
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
(equiv_Z1_hom A)^-1* o* ab_mul n ==
fmap10 ab_hom (Z1_mul_nat n) A o* pequiv_inverse (equiv_Z1_hom A)
    rapply (equiv_ind (equiv_Z1_hom A)); intro f.
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
f: ab_hom ab_Z1 A
((equiv_Z1_hom A)^-1* o* ab_mul n) (equiv_Z1_hom A f) =
(fmap10 ab_hom (Z1_mul_nat n) A o* pequiv_inverse (equiv_Z1_hom A))
  (equiv_Z1_hom A f)
    refine (_ @ ap _ (eissect _ _)^).
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
f: ab_hom ab_Z1 A
((equiv_Z1_hom A)^-1* o* ab_mul n) (equiv_Z1_hom A f) =
fmap10 ab_hom (Z1_mul_nat n) A f
    apply moveR_equiv_V; symmetry.
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
f: ab_hom ab_Z1 A
equiv_Z1_hom A (fmap10 ab_hom (Z1_mul_nat n) A f) =
ab_mul n (equiv_Z1_hom A f)
    refine (ap f _ @ _).
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
f: ab_hom ab_Z1 A
Z1_mul_nat n (freegroup_in tt) = ?Goal
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
f: ab_hom ab_Z1 A
f ?Goal = ab_mul n (equiv_Z1_hom A f)
    1: apply Z1_rec_beta.
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
f: ab_hom ab_Z1 A
f (nat_to_Z1 n) = ab_mul n (equiv_Z1_hom A f)
    exact (ab_mul_natural f n Z1_gen).
  - (* we get rid of [equiv_Z1_hom] *)
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
IsExact (Tr (-1))
  (fmap10 ab_hom (Z1_mul_nat n) A o* pequiv_inverse (equiv_Z1_hom A))
  (abses_pushout_ext (abses_from_inclusion (Z1_mul_nat n)))
    apply isexact_equiv_fiber.
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
IsExact (Tr (-1)) (fmap10 ab_hom (Z1_mul_nat n) A)
  (abses_pushout_ext (abses_from_inclusion (Z1_mul_nat n)))
    apply isexact_ext_cyclic_ab_iii.
Defined.

(** The main result of this section. *)
Theorem ext_cyclic_ab@{u v w | u < v, v < w} `{Univalence}
  (n : nat) `{emb : IsEmbedding (Z1_mul_nat n)} {A : AbGroup@{u}}
  : ab_cokernel@{v w} (ab_mul (A:=A) n)
      $<~> ab_ext@{u v} (cyclic'@{u v} n) A.
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
ab_cokernel (ab_mul n) $<~> ab_ext (cyclic' n) A
  (* We take a large cokernel in order to apply [abses_cokernel_iso]. *)
Proof.
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
ab_cokernel (ab_mul n) $<~> ab_ext (cyclic' n) A
  pose (E := abses_from_inclusion (Z1_mul_nat n)).
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES (QuotientAbGroup ab_Z1 (grp_image_embedding (Z1_mul_nat n))) ab_Z1
ab_cokernel (ab_mul n) $<~> ab_ext (cyclic' n) A
  snrefine (abses_cokernel_iso (ab_mul n) _).
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES (QuotientAbGroup ab_Z1 (grp_image_embedding (Z1_mul_nat n))) ab_Z1
GroupHomomorphism A (ab_ext (cyclic' n) A)
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES (QuotientAbGroup ab_Z1 (grp_image_embedding (Z1_mul_nat n))) ab_Z1
IsConnMap (Tr (-1)) ?g
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES (QuotientAbGroup ab_Z1 (grp_image_embedding (Z1_mul_nat n))) ab_Z1
IsExact (Tr (-1)) (ab_mul n) ?g
  -
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES (QuotientAbGroup ab_Z1 (grp_image_embedding (Z1_mul_nat n))) ab_Z1
GroupHomomorphism A (ab_ext (cyclic' n) A) exact (grp_homo_compose
             (abses_pushout_ext E)
             (grp_iso_inverse (equiv_Z1_hom A))).
  -
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES (QuotientAbGroup ab_Z1 (grp_image_embedding (Z1_mul_nat n))) ab_Z1
IsConnMap (Tr (-1))
  (grp_homo_compose (abses_pushout_ext E) (grp_iso_inverse (equiv_Z1_hom A))) apply (conn_map_compose _ (grp_iso_inverse (equiv_Z1_hom A))).
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES (QuotientAbGroup ab_Z1 (grp_image_embedding (Z1_mul_nat n))) ab_Z1
IsConnMap (Tr (-1)) (grp_iso_inverse (equiv_Z1_hom A))
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES (QuotientAbGroup ab_Z1 (grp_image_embedding (Z1_mul_nat n))) ab_Z1
IsConnMap (Tr (-1)) (abses_pushout_ext E)
    1: rapply conn_map_isequiv.
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES (QuotientAbGroup ab_Z1 (grp_image_embedding (Z1_mul_nat n))) ab_Z1
IsConnMap (Tr (-1)) (abses_pushout_ext E)
    (* Coq knows that [Ext Z1 A] is contractible since [Z1] is projective, so exactness at spot iv gives us this: *)
    exact (isconnmap_O_isexact_base_contr _ _
             (fmap (pTr 0)
                (abses_pullback_pmap (A:=A)
                   (projection E)))).
  - (* we change [grp_homo_compose] to [o*] *)
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES (QuotientAbGroup ab_Z1 (grp_image_embedding (Z1_mul_nat n))) ab_Z1
IsExact (Tr (-1)) (ab_mul n)
  (grp_homo_compose (abses_pushout_ext E) (grp_iso_inverse (equiv_Z1_hom A)))
    srapply isexact_homotopic_f.
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES (QuotientAbGroup ab_Z1 (grp_image_embedding (Z1_mul_nat n))) ab_Z1
A ->* ab_ext (cyclic' n) A
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES (QuotientAbGroup ab_Z1 (grp_image_embedding (Z1_mul_nat n))) ab_Z1
grp_homo_compose (abses_pushout_ext E) (grp_iso_inverse (equiv_Z1_hom A)) ==*
?f
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES (QuotientAbGroup ab_Z1 (grp_image_embedding (Z1_mul_nat n))) ab_Z1
IsExact (Tr (-1)) (ab_mul n) ?f
    1: exact (abses_pushout_ext (abses_from_inclusion (Z1_mul_nat n))
                o* (pequiv_groupisomorphism (equiv_Z1_hom A))^-1*).
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES (QuotientAbGroup ab_Z1 (grp_image_embedding (Z1_mul_nat n))) ab_Z1
grp_homo_compose (abses_pushout_ext E) (grp_iso_inverse (equiv_Z1_hom A)) ==*
abses_pushout_ext (abses_from_inclusion (Z1_mul_nat n))
o* (equiv_Z1_hom A)^-1*
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES (QuotientAbGroup ab_Z1 (grp_image_embedding (Z1_mul_nat n))) ab_Z1
IsExact (Tr (-1)) (ab_mul n)
  (abses_pushout_ext (abses_from_inclusion (Z1_mul_nat n))
   o* (equiv_Z1_hom A)^-1*)
    1: by apply phomotopy_homotopy_hset.
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES (QuotientAbGroup ab_Z1 (grp_image_embedding (Z1_mul_nat n))) ab_Z1
IsExact (Tr (-1)) (ab_mul n)
  (abses_pushout_ext (abses_from_inclusion (Z1_mul_nat n))
   o* (equiv_Z1_hom A)^-1*)
    apply ext_cyclic_exact.
Defined.