Require Import Basics Types Truncations.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import HSet WildCat.
Require Import Groups.QuotientGroup Groups.ShortExactSequence.
Require Import AbelianGroup AbGroups.Biproduct AbHom.
Require Import Homotopy.ExactSequence Pointed.
Require Import Modalities.ReflectiveSubuniverse.

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

(** * Short exact sequences of abelian groups *)

(** A short exact sequence of abelian groups consists of a monomorphism [i : A -> E] and an epimorphism [p : E -> B] such that the image of [i] equals the kernel of [p]. Later we will consider short exact sequences up to isomorphism by 0-truncating the type [AbSES] defined below. An isomorphism class of short exact sequences is called an extension. *)

Declare Scope abses_scope.
Local Open Scope abses_scope.

(** The type of short exact sequences [A -> E -> B] of abelian groups. We decorate it with (') to reserve the undecorated name for the structured version. *)
Record AbSES' {B A : AbGroup@{u}} := Build_AbSES {
    middle :  AbGroup@{u};
    inclusion : A $-> middle;
    projection : middle $-> B;
    isembedding_inclusion : IsEmbedding inclusion;
    issurjection_projection : IsSurjection projection;
    isexact_inclusion_projection : IsExact (Tr (-1)) inclusion projection;
  }.

(** Given a short exact sequence [A -> E -> B : AbSES B A], we coerce it to [E]. *)
Coercion middle : AbSES' >-> AbGroup.

Global Existing Instances isembedding_inclusion issurjection_projection isexact_inclusion_projection.

Arguments AbSES' B A : clear implicits.
Arguments Build_AbSES {B A}.

(** TODO Figure out why printing this term eats memory and seems to never finish. *)
Local Definition issig_abses_do_not_print {B A : AbGroup} : _ <~> AbSES' B A := ltac:(issig).

(** [make_equiv] is slow if used in the context of the next result, so we give the abstract form of the goal here. *)
Local Definition issig_abses_helper {AG : Type} {P : AG -> Type} {Q : AG -> Type}
      {R : forall E, P E -> Type} {S : forall E, Q E -> Type} {T : forall E, P E -> Q E -> Type}
  : {X : {E : AG & P E * Q E} & R _ (fst X.2) * S _ (snd X.2) * T _ (fst X.2) (snd X.2)}
      <~> {E : AG & {H0 : P E & {H1 : Q E & {_ : R _ H0 & {_ : S _ H1 & T _ H0 H1}}}}}
  := ltac:(make_equiv).

(** A more useful organization of [AbSES'] as a sigma-type. *)
Definition issig_abses {B A : AbGroup}
  : {X : {E : AbGroup & (A $-> E) * (E $-> B)} &
           (IsEmbedding (fst X.2)
            * IsSurjection (snd X.2)
            * IsExact (Tr (-1)) (fst X.2) (snd X.2))}
      <~> AbSES' B A
  := issig_abses_do_not_print oE issig_abses_helper.

Definition iscomplex_abses {A B : AbGroup} (E : AbSES' B A)
  : IsComplex (inclusion E) (projection E)
  := cx_isexact.

(** [AbSES' B A] is pointed by the split sequence [A -> A+B -> B]. *)
Global Instance ispointed_abses {B A : AbGroup@{u}}
  : IsPointed (AbSES' B A).
B, A: AbGroup
IsPointed (AbSES' B A)
Proof.
B, A: AbGroup
IsPointed (AbSES' B A)
  rapply (Build_AbSES (ab_biprod A B) ab_biprod_inl ab_biprod_pr2).
B, A: AbGroup
IsExact (Tr (-1)) ab_biprod_inl ab_biprod_pr2
  snrapply Build_IsExact.
B, A: AbGroup
IsComplex ab_biprod_inl ab_biprod_pr2
B, A: AbGroup
IsConnMap (Tr (-1)) (cxfib ?cx_isexact)
  -
B, A: AbGroup
IsComplex ab_biprod_inl ab_biprod_pr2 srapply phomotopy_homotopy_hset; reflexivity.
  -
B, A: AbGroup
IsConnMap (Tr (-1))
  (cxfib
     (phomotopy_homotopy_hset (fun x0 : A => 1%path))) intros [[a b] p]; cbn; cbn in p.
B, A: AbGroup
a: A
b: B
p: b = ispointed_group B
IsConnected (Tr (-1))
  (hfiber (fun x : A => ((x, group_unit); 1%path))
     ((a, b); p))
    rapply contr_inhabited_hprop.
B, A: AbGroup
a: A
b: B
p: b = ispointed_group B
Tr (-1)
  (hfiber (fun x : A => ((x, group_unit); 1%path))
     ((a, b); p))
    apply tr.
B, A: AbGroup
a: A
b: B
p: b = ispointed_group B
hfiber (fun x : A => ((x, group_unit); 1%path))
  ((a, b); p)
    exists a.
B, A: AbGroup
a: A
b: B
p: b = ispointed_group B
((a, group_unit); 1%path) = ((a, b); p)
    rapply path_sigma_hprop; cbn.
B, A: AbGroup
a: A
b: B
p: b = ispointed_group B
(a, group_unit) = (a, b)
    exact (path_prod' idpath p^).
Defined.

(** The pointed type of short exact sequences. *)
Definition AbSES (B A : AbGroup@{u}) : pType
  := [AbSES' B A, _].

(** ** Paths in [AbSES B A] *)

Definition abses_path_data_iso
  {B A : AbGroup@{u}} (E F : AbSES B A)
  := {phi : GroupIsomorphism E F
            & (phi $o inclusion _ == inclusion _)
              * (projection _ == projection _ $o phi)}.

(** Having the path data in a slightly different form is useful for [equiv_path_abses_iso]. *)
Local Lemma shuffle_abses_path_data_iso `{Funext}
  {B A : AbGroup@{u}} (E F : AbSES B A)
  : (abses_path_data_iso E F)
      <~> {phi : GroupIsomorphism E F
                 & (phi $o inclusion _ == inclusion _)
                   * (projection _ $o grp_iso_inverse phi
                      == projection _)}.
H: Funext
B, A: AbGroup
E, F: AbSES B A
abses_path_data_iso E F <~>
{phi : GroupIsomorphism E F &
(phi $o inclusion E == inclusion F) *
(projection E $o grp_iso_inverse phi == projection F)}
Proof.
H: Funext
B, A: AbGroup
E, F: AbSES B A
abses_path_data_iso E F <~>
{phi : GroupIsomorphism E F &
(phi $o inclusion E == inclusion F) *
(projection E $o grp_iso_inverse phi == projection F)}
  srapply equiv_functor_sigma_id; intro phi.
H: Funext
B, A: AbGroup
E, F: AbSES B A
phi: GroupIsomorphism E F
(fun phi : GroupIsomorphism E F =>
 (phi $o inclusion E == inclusion F) *
 (projection E == projection F $o phi)) phi <~>
(fun phi : GroupIsomorphism E F =>
 (phi $o inclusion E == inclusion F) *
 (projection E $o grp_iso_inverse phi == projection F))
  phi
  srapply equiv_functor_prod'.
H: Funext
B, A: AbGroup
E, F: AbSES B A
phi: GroupIsomorphism E F
phi $o inclusion E == inclusion F <~>
phi $o inclusion E == inclusion F
H: Funext
B, A: AbGroup
E, F: AbSES B A
phi: GroupIsomorphism E F
projection E == projection F $o phi <~>
projection E $o grp_iso_inverse phi == projection F
  1: exact equiv_idmap.
H: Funext
B, A: AbGroup
E, F: AbSES B A
phi: GroupIsomorphism E F
projection E == projection F $o phi <~>
projection E $o grp_iso_inverse phi == projection F
  srapply (equiv_functor_forall' phi^-1); intro e; cbn.
H: Funext
B, A: AbGroup
E, F: AbSES B A
phi: GroupIsomorphism E F
e: F
projection E (phi^-1 e) =
projection F (phi (phi^-1 e)) <~>
projection E (phi^-1 e) = projection F e
  apply equiv_concat_r.
H: Funext
B, A: AbGroup
E, F: AbSES B A
phi: GroupIsomorphism E F
e: F
projection F (phi (phi^-1 e)) = projection F e
  exact (ap _ (eisretr _ _)).
Defined.

(** Paths in [AbSES] correspond to isomorphisms between the [middle]s respecting [inclusion] and [projection]. Below we prove the stronger statement [equiv_path_abses], which uses this result. *)
Proposition equiv_path_abses_iso `{Univalence}
  {B A : AbGroup@{u}} {E F : AbSES' B A}
  : abses_path_data_iso E F <~> E = F.
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
abses_path_data_iso E F <~> E = F
Proof.
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
abses_path_data_iso E F <~> E = F
  refine (_ oE shuffle_abses_path_data_iso E F).
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
{phi : GroupIsomorphism E F &
(phi $o inclusion E == inclusion F) *
(projection E $o grp_iso_inverse phi == projection F)} <~>
E = F
  refine (equiv_ap_inv issig_abses _ _ oE _).
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
{phi : GroupIsomorphism E F &
(phi $o inclusion E == inclusion F) *
(projection E $o grp_iso_inverse phi == projection F)} <~>
issig_abses^-1 E = issig_abses^-1 F
  refine (equiv_path_sigma_hprop _ _ oE _).
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
{phi : GroupIsomorphism E F &
(phi $o inclusion E == inclusion F) *
(projection E $o grp_iso_inverse phi == projection F)} <~>
(issig_abses^-1 E).1 = (issig_abses^-1 F).1
  refine (equiv_path_sigma _ _ _ oE _).
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
{phi : GroupIsomorphism E F &
(phi $o inclusion E == inclusion F) *
(projection E $o grp_iso_inverse phi == projection F)} <~>
{p
: ((issig_abses^-1 E).1).1 = ((issig_abses^-1 F).1).1
&
transport (fun E : AbGroup => (A $-> E) * (E $-> B)) p
  ((issig_abses^-1 E).1).2 = ((issig_abses^-1 F).1).2}
  srapply equiv_functor_sigma'.
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
GroupIsomorphism E F <~>
((issig_abses^-1 E).1).1 = ((issig_abses^-1 F).1).1
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
forall a : GroupIsomorphism E F,
(fun phi : GroupIsomorphism E F =>
 (phi $o inclusion E == inclusion F) *
 (projection E $o grp_iso_inverse phi == projection F))
  a <~>
(fun
   p : ((issig_abses^-1 E).1).1 =
       ((issig_abses^-1 F).1).1 =>
 transport (fun E : AbGroup => (A $-> E) * (E $-> B))
   p ((issig_abses^-1 E).1).2 =
 ((issig_abses^-1 F).1).2) (?f a)
  1: exact equiv_path_abgroup.
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
forall a : GroupIsomorphism E F,
(fun phi : GroupIsomorphism E F =>
 (phi $o inclusion E == inclusion F) *
 (projection E $o grp_iso_inverse phi == projection F))
  a <~>
(fun
   p : ((issig_abses^-1 E).1).1 =
       ((issig_abses^-1 F).1).1 =>
 transport (fun E : AbGroup => (A $-> E) * (E $-> B))
   p ((issig_abses^-1 E).1).2 =
 ((issig_abses^-1 F).1).2) (equiv_path_abgroup a)
  intro q; lazy beta.
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
q: GroupIsomorphism E F
(q $o inclusion E == inclusion F) *
(projection E $o grp_iso_inverse q == projection F) <~>
transport (fun E : AbGroup => (A $-> E) * (E $-> B))
  (equiv_path_abgroup q) ((issig_abses^-1 E).1).2 =
((issig_abses^-1 F).1).2
  snrefine (equiv_concat_l _ _ oE _).
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
q: GroupIsomorphism E F
(A $-> ((issig_abses^-1 F).1).1) *
(((issig_abses^-1 F).1).1 $-> B)
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
q: GroupIsomorphism E F
transport (fun E : AbGroup => (A $-> E) * (E $-> B))
  (equiv_path_abgroup q) ((issig_abses^-1 E).1).2 = 
?y
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
q: GroupIsomorphism E F
(q $o inclusion E == inclusion F) *
(projection E $o grp_iso_inverse q == projection F) <~>
?y = ((issig_abses^-1 F).1).2
  1: exact (q $o inclusion _, projection _ $o grp_iso_inverse q).
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
q: GroupIsomorphism E F
transport (fun E : AbGroup => (A $-> E) * (E $-> B))
  (equiv_path_abgroup q) ((issig_abses^-1 E).1).2 =
(q $o inclusion E, projection E $o grp_iso_inverse q)
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
q: GroupIsomorphism E F
(q $o inclusion E == inclusion F) *
(projection E $o grp_iso_inverse q == projection F) <~>
(q $o inclusion E, projection E $o grp_iso_inverse q) =
((issig_abses^-1 F).1).2
  2: {
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
q: GroupIsomorphism E F
(q $o inclusion E == inclusion F) *
(projection E $o grp_iso_inverse q == projection F) <~>
(q $o inclusion E, projection E $o grp_iso_inverse q) =
((issig_abses^-1 F).1).2 refine (equiv_path_prod _ _ oE _).
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
q: GroupIsomorphism E F
(q $o inclusion E == inclusion F) *
(projection E $o grp_iso_inverse q == projection F) <~>
(fst
   (q $o inclusion E,
   projection E $o grp_iso_inverse q) =
 fst ((issig_abses^-1 F).1).2) *
(snd
   (q $o inclusion E,
   projection E $o grp_iso_inverse q) =
 snd ((issig_abses^-1 F).1).2)
       exact (equiv_functor_prod'
                equiv_path_grouphomomorphism
                equiv_path_grouphomomorphism). }
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
q: GroupIsomorphism E F
transport (fun E : AbGroup => (A $-> E) * (E $-> B))
  (equiv_path_abgroup q) ((issig_abses^-1 E).1).2 =
(q $o inclusion E, projection E $o grp_iso_inverse q)
  refine (transport_prod _ _ @ _).
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
q: GroupIsomorphism E F
(transport (Hom A) (equiv_path_abgroup q)
   (fst ((issig_abses^-1 E).1).2),
transport (fun a : AbGroup => a $-> B)
  (equiv_path_abgroup q)
  (snd ((issig_abses^-1 E).1).2)) =
(q $o inclusion E, projection E $o grp_iso_inverse q)
  apply path_prod'.
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
q: GroupIsomorphism E F
transport (Hom A) (equiv_path_abgroup q)
  (fst ((issig_abses^-1 E).1).2) = q $o inclusion E
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
q: GroupIsomorphism E F
transport (fun a : AbGroup => a $-> B)
  (equiv_path_abgroup q)
  (snd ((issig_abses^-1 E).1).2) =
projection E $o grp_iso_inverse q
  -
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
q: GroupIsomorphism E F
transport (Hom A) (equiv_path_abgroup q)
  (fst ((issig_abses^-1 E).1).2) = q $o inclusion E apply transport_iso_abgrouphomomorphism_from_const.
  -
H: Univalence
B, A: AbGroup
E, F: AbSES' B A
q: GroupIsomorphism E F
transport (fun a : AbGroup => a $-> B)
  (equiv_path_abgroup q)
  (snd ((issig_abses^-1 E).1).2) =
projection E $o grp_iso_inverse q apply transport_iso_abgrouphomomorphism_to_const.
Defined.

(** It follows that [AbSES B A] is 1-truncated. *)
Global Instance istrunc_abses `{Univalence} {B A : AbGroup@{u}}
  : IsTrunc 1 (AbSES B A).
H: Univalence
B, A: AbGroup
IsTrunc 1 (AbSES B A)
Proof.
H: Univalence
B, A: AbGroup
IsTrunc 1 (AbSES B A)
  apply istrunc_S.
H: Univalence
B, A: AbGroup
forall x y : AbSES B A, IsHSet (x = y)
  intros E F.
H: Univalence
B, A: AbGroup
E, F: AbSES B A
IsHSet (E = F)
  refine (istrunc_equiv_istrunc _ equiv_path_abses_iso (n:=0)).
H: Univalence
B, A: AbGroup
E, F: AbSES B A
IsHSet (abses_path_data_iso E F)
  rapply istrunc_sigma.
H: Univalence
B, A: AbGroup
E, F: AbSES B A
IsHSet (GroupIsomorphism E F)
  apply ishset_groupisomorphism.
Defined.

Definition path_abses_iso `{Univalence} {B A : AbGroup@{u}}
  {E F : AbSES B A}
  (phi : GroupIsomorphism E F) (p : phi $o inclusion _ == inclusion _)
  (q : projection _ == projection _ $o phi)
  : E = F := equiv_path_abses_iso (phi; (p,q)).

(** Given [p] and [q], the map [phi] just above is automatically an isomorphism. Showing this requires the "short five lemma." *)

(** A special case of the "short 5-lemma" where the two outer maps are (definitionally) identities. *)
Lemma short_five_lemma {B A : AbGroup@{u}}
  {E F : AbSES B A} (phi : GroupHomomorphism E F)
  (p0 : phi $o inclusion E == inclusion F) (p1 : projection E == projection F $o phi)
  : IsEquiv phi.
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
IsEquiv phi
Proof.
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
IsEquiv phi
  apply isequiv_surj_emb.
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
IsConnMap (Tr (-1)) phi
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
IsEmbedding phi
  -
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
IsConnMap (Tr (-1)) phi intro f.
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
f: F
IsConnected (Tr (-1)) (hfiber phi f)
    rapply contr_inhabited_hprop.
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
f: F
Tr (-1) (hfiber phi f)
    (** Since [projection E] is epi, we can pull [projection F f] back to [e0 : E].*)
    assert (e0 : Tr (-1) (hfiber (projection E) (projection F f))).
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
f: F
Tr (-1) (hfiber (projection E) (projection F f))
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
f: F
e0: Tr (-1) (hfiber (projection E) (projection F f))
Tr (-1) (hfiber phi f)
    1: apply center, issurjection_projection.
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
f: F
e0: Tr (-1) (hfiber (projection E) (projection F f))
Tr (-1) (hfiber phi f)
    strip_truncations.
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
f: F
e0: hfiber (projection E) (projection F f)
Tr (-1) (hfiber phi f)
    (** The difference [f - (phi e0.1)] is sent to [0] by [projection F], hence lies in [A]. *)
    assert (a : Tr (-1) (hfiber (inclusion F) (f + (- phi e0.1)))).
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
f: F
e0: hfiber (projection E) (projection F f)
Tr (-1) (hfiber (inclusion F) (f + - phi e0.1))
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
f: F
e0: hfiber (projection E) (projection F f)
a: Tr (-1) (hfiber (inclusion F) (f + - phi e0.1))
Tr (-1) (hfiber phi f)
    1: {
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
f: F
e0: hfiber (projection E) (projection F f)
Tr (-1) (hfiber (inclusion F) (f + - phi e0.1)) refine (isexact_preimage (Tr (-1)) (inclusion F) (projection F) _ _).
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
f: F
e0: hfiber (projection E) (projection F f)
projection F (f + - phi e0.1) = pt
         refine (grp_homo_op _ _ _ @ _).
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
f: F
e0: hfiber (projection E) (projection F f)
projection F f + projection F (- phi e0.1) = pt
         refine (ap _ (grp_homo_inv _ _) @ _).
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
f: F
e0: hfiber (projection E) (projection F f)
projection F f + - projection F (phi e0.1) = pt
         apply (grp_moveL_1M)^-1.
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
f: F
e0: hfiber (projection E) (projection F f)
projection F f = projection F (phi e0.1)
         exact (e0.2^ @ p1 e0.1). }
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
f: F
e0: hfiber (projection E) (projection F f)
a: Tr (-1) (hfiber (inclusion F) (f + - phi e0.1))
Tr (-1) (hfiber phi f)
    strip_truncations.
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
f: F
e0: hfiber (projection E) (projection F f)
a: hfiber (inclusion F) (f + - phi e0.1)
Tr (-1) (hfiber phi f)
    refine (tr (inclusion E a.1 + e0.1; _)).
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
f: F
e0: hfiber (projection E) (projection F f)
a: hfiber (inclusion F) (f + - phi e0.1)
phi (inclusion E a.1 + e0.1) = f
    refine (grp_homo_op _ _ _ @ _).
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
f: F
e0: hfiber (projection E) (projection F f)
a: hfiber (inclusion F) (f + - phi e0.1)
phi (inclusion E a.1) + phi e0.1 = f
    refine (ap (fun x => x + phi e0.1) (p0 a.1 @ a.2) @ _).
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
f: F
e0: hfiber (projection E) (projection F f)
a: hfiber (inclusion F) (f + - phi e0.1)
f + - phi e0.1 + phi e0.1 = f
    refine ((grp_assoc _ _ _)^ @ _).
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
f: F
e0: hfiber (projection E) (projection F f)
a: hfiber (inclusion F) (f + - phi e0.1)
f + (- phi e0.1 + phi e0.1) = f
    refine (ap _ (left_inverse (phi e0.1)) @ _).
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
f: F
e0: hfiber (projection E) (projection F f)
a: hfiber (inclusion F) (f + - phi e0.1)
f + mon_unit = f
    apply grp_unit_r.
  -
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
IsEmbedding phi apply isembedding_grouphomomorphism.
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
forall a : E, phi a = group_unit -> a = group_unit
    intros e p.
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
e: E
p: phi e = group_unit
e = group_unit
    assert (a : Tr (-1) (hfiber (inclusion E) e)).
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
e: E
p: phi e = group_unit
Tr (-1) (hfiber (inclusion E) e)
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
e: E
p: phi e = group_unit
a: Tr (-1) (hfiber (inclusion E) e)
e = group_unit
    1: {
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
e: E
p: phi e = group_unit
Tr (-1) (hfiber (inclusion E) e) refine (isexact_preimage _ (inclusion E) (projection E) _ _).
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
e: E
p: phi e = group_unit
projection E e = pt
         exact (p1 e @ ap (projection F) p @ grp_homo_unit _). }
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
e: E
p: phi e = group_unit
a: Tr (-1) (hfiber (inclusion E) e)
e = group_unit
    strip_truncations.
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
e: E
p: phi e = group_unit
a: hfiber (inclusion E) e
e = group_unit
    refine (a.2^ @ ap (inclusion E ) _ @ grp_homo_unit (inclusion E)).
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
e: E
p: phi e = group_unit
a: hfiber (inclusion E) e
a.1 = mon_unit
    rapply (isinj_embedding (inclusion F) _ _).
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
e: E
p: phi e = group_unit
a: hfiber (inclusion E) e
inclusion F a.1 = inclusion F mon_unit
    refine ((p0 a.1)^ @ (ap phi a.2) @ p @ (grp_homo_unit _)^).
Defined.

(** Below we prove that homomorphisms respecting [projection] and [inclusion] correspond to paths in [AbSES B A]. We refer to such homomorphisms simply as path data in [AbSES B A]. *)
Definition abses_path_data {B A : AbGroup@{u}} (E F : AbSES B A)
  := {phi : GroupHomomorphism E F
            & (phi $o inclusion _ == inclusion _)
              * (projection _ == projection _ $o phi)}.

Definition abses_path_data_to_iso {B A : AbGroup@{u}} (E F: AbSES B A)
  : abses_path_data E F -> abses_path_data_iso E F.
B, A: AbGroup
E, F: AbSES B A
abses_path_data E F -> abses_path_data_iso E F
Proof.
B, A: AbGroup
E, F: AbSES B A
abses_path_data E F -> abses_path_data_iso E F
  -
B, A: AbGroup
E, F: AbSES B A
abses_path_data E F -> abses_path_data_iso E F intros [phi [p q]].
B, A: AbGroup
E, F: AbSES B A
phi: GroupHomomorphism E F
p: phi $o inclusion E == inclusion F
q: projection E == projection F $o phi
abses_path_data_iso E F
    exact ({| grp_iso_homo := phi; isequiv_group_iso := short_five_lemma phi p q |}; (p, q)).
Defined.

Proposition equiv_path_abses_data `{Funext} {B A : AbGroup@{u}} (E F: AbSES B A)
  : abses_path_data E F <~> abses_path_data_iso E F.
H: Funext
B, A: AbGroup
E, F: AbSES B A
abses_path_data E F <~> abses_path_data_iso E F
Proof.
H: Funext
B, A: AbGroup
E, F: AbSES B A
abses_path_data E F <~> abses_path_data_iso E F
  srapply equiv_adjointify.
H: Funext
B, A: AbGroup
E, F: AbSES B A
abses_path_data E F -> abses_path_data_iso E F
H: Funext
B, A: AbGroup
E, F: AbSES B A
abses_path_data_iso E F -> abses_path_data E F
H: Funext
B, A: AbGroup
E, F: AbSES B A
?f o ?g == idmap
H: Funext
B, A: AbGroup
E, F: AbSES B A
?g o ?f == idmap
  -
H: Funext
B, A: AbGroup
E, F: AbSES B A
abses_path_data E F -> abses_path_data_iso E F apply abses_path_data_to_iso.
  -
H: Funext
B, A: AbGroup
E, F: AbSES B A
abses_path_data_iso E F -> abses_path_data E F srapply (functor_sigma (grp_iso_homo _ _)).
H: Funext
B, A: AbGroup
E, F: AbSES B A
forall a : GroupIsomorphism E F,
(fun phi : GroupIsomorphism E F =>
 (phi $o inclusion E == inclusion F) *
 (projection E == projection F $o phi)) a ->
(fun phi : GroupHomomorphism E F =>
 (phi $o inclusion E == inclusion F) *
 (projection E == projection F $o phi)) a
    exact (fun _ => idmap).
  -
H: Funext
B, A: AbGroup
E, F: AbSES B A
abses_path_data_to_iso E F
o functor_sigma (grp_iso_homo E F)
    (fun a : GroupIsomorphism E F => idmap) == idmap intros [phi [p q]].
H: Funext
B, A: AbGroup
E, F: AbSES B A
phi: GroupIsomorphism E F
p: phi $o inclusion E == inclusion F
q: projection E == projection F $o phi
abses_path_data_to_iso E F
  (functor_sigma (grp_iso_homo E F)
     (fun a : GroupIsomorphism E F => idmap)
     (phi; (p, q))) = (phi; (p, q))
    apply path_sigma_hprop.
H: Funext
B, A: AbGroup
E, F: AbSES B A
phi: GroupIsomorphism E F
p: phi $o inclusion E == inclusion F
q: projection E == projection F $o phi
(abses_path_data_to_iso E F
   (functor_sigma (grp_iso_homo E F)
      (fun a : GroupIsomorphism E F => idmap)
      (phi; (p, q)))).1 = (phi; (p, q)).1
    by apply equiv_path_groupisomorphism.
  -
H: Funext
B, A: AbGroup
E, F: AbSES B A
functor_sigma (grp_iso_homo E F)
  (fun a : GroupIsomorphism E F => idmap)
o abses_path_data_to_iso E F == idmap reflexivity.
Defined.

Definition equiv_path_abses `{Univalence} {B A : AbGroup@{u}} {E F : AbSES B A}
  : abses_path_data E F <~> E = F
  := equiv_path_abses_iso oE equiv_path_abses_data E F.

Definition path_abses `{Univalence} {B A : AbGroup@{u}}
  {E F : AbSES B A} (phi : middle E $-> F)
  (p : phi $o inclusion _ == inclusion _) (q : projection _ == projection _ $o phi)
  : E = F := equiv_path_abses (phi; (p,q)).

(** *** The wildcat of short exact sequences *)

Global Instance isgraph_abses_path_data {A B : AbGroup@{u}} (E F : AbSES B A)
  : IsGraph (abses_path_data_iso E F)
  := isgraph_induced (grp_iso_homo _ _ o pr1).

Global Instance is01cat_abses_path_data {A B : AbGroup@{u}} (E F : AbSES B A)
  : Is01Cat (abses_path_data_iso E F)
  := is01cat_induced (grp_iso_homo _ _ o pr1).

Global Instance is0gpd_abses_path_data {A B : AbGroup@{u}} (E F : AbSES B A)
  : Is0Gpd (abses_path_data_iso E F)
  := is0gpd_induced (grp_iso_homo _ _ o pr1).

Global Instance isgraph_abses {A B : AbGroup@{u}} : IsGraph (AbSES B A)
  := Build_IsGraph _ abses_path_data_iso.

(** The path data corresponding to [idpath]. *)
Definition abses_path_data_1 {B A : AbGroup@{u}} (E : AbSES B A)
  : E $-> E := (grp_iso_id; (fun _ => idpath, fun _ => idpath)).

(** We can compose path data in [AbSES B A]. *)
Definition abses_path_data_compose {B A : AbGroup@{u}} {E F G : AbSES B A}
           (p : E $-> F) (q : F $-> G) : E $-> G
  := (q.1 $oE p.1; ((fun x => ap q.1 (fst p.2 x) @ fst q.2 x),
                     (fun x => snd p.2 x @ snd q.2 (p.1 x)))).

Global Instance is01cat_abses {A B : AbGroup@{u}}
  : Is01Cat (AbSES B A)
  := Build_Is01Cat _ _ abses_path_data_1
       (fun _ _ _ q p => abses_path_data_compose p q).

Definition abses_path_data_inverse
  {B A : AbGroup@{u}} {E F : AbSES B A}
  : (E $-> F) -> (F $-> E).
B, A: AbGroup
E, F: AbSES B A
(E $-> F) -> F $-> E
Proof.
B, A: AbGroup
E, F: AbSES B A
(E $-> F) -> F $-> E
  intros [phi [p q]].
B, A: AbGroup
E, F: AbSES B A
phi: GroupIsomorphism E F
p: phi $o inclusion E == inclusion F
q: projection E == projection F $o phi
F $-> E
  srefine (_; (_,_)).
B, A: AbGroup
E, F: AbSES B A
phi: GroupIsomorphism E F
p: phi $o inclusion E == inclusion F
q: projection E == projection F $o phi
GroupIsomorphism F E
B, A: AbGroup
E, F: AbSES B A
phi: GroupIsomorphism E F
p: phi $o inclusion E == inclusion F
q: projection E == projection F $o phi
?proj1 $o inclusion F == inclusion E
B, A: AbGroup
E, F: AbSES B A
phi: GroupIsomorphism E F
p: phi $o inclusion E == inclusion F
q: projection E == projection F $o phi
projection F == projection E $o ?proj1
  -
B, A: AbGroup
E, F: AbSES B A
phi: GroupIsomorphism E F
p: phi $o inclusion E == inclusion F
q: projection E == projection F $o phi
GroupIsomorphism F E exact (grp_iso_inverse phi).
  -
B, A: AbGroup
E, F: AbSES B A
phi: GroupIsomorphism E F
p: phi $o inclusion E == inclusion F
q: projection E == projection F $o phi
grp_iso_inverse phi $o inclusion F == inclusion E intro a.
B, A: AbGroup
E, F: AbSES B A
phi: GroupIsomorphism E F
p: phi $o inclusion E == inclusion F
q: projection E == projection F $o phi
a: A
(grp_iso_inverse phi $o inclusion F) a = inclusion E a
    exact (ap _ (p a)^ @ eissect _ (inclusion E a)).
  -
B, A: AbGroup
E, F: AbSES B A
phi: GroupIsomorphism E F
p: phi $o inclusion E == inclusion F
q: projection E == projection F $o phi
projection F == projection E $o grp_iso_inverse phi intro a; simpl.
B, A: AbGroup
E, F: AbSES B A
phi: GroupIsomorphism E F
p: phi $o inclusion E == inclusion F
q: projection E == projection F $o phi
a: F
projection F a = projection E (phi^-1 a)
    exact (ap (projection F) (eisretr _ _)^ @ (q _)^).
Defined.

Global Instance is0gpd_abses
  {A B : AbGroup@{u}} : Is0Gpd (AbSES B A)
  := {| gpd_rev := fun _ _ => abses_path_data_inverse |}.

Global Instance is2graph_abses
  {A B : AbGroup@{u}} : Is2Graph (AbSES B A)
  := fun E F => isgraph_abses_path_data E F.

(** [AbSES B A] forms a 1Cat *)
Global Instance is1cat_abses {A B : AbGroup@{u}}
  : Is1Cat (AbSES B A).
A, B: AbGroup
Is1Cat (AbSES B A)
Proof.
A, B: AbGroup
Is1Cat (AbSES B A)
  snrapply Build_Is1Cat'.
A, B: AbGroup
forall a b : AbSES B A, Is01Cat (a $-> b)
A, B: AbGroup
forall a b : AbSES B A, Is0Gpd (a $-> b)
A, B: AbGroup
forall (a b c : AbSES B A) (g : b $-> c),
Is0Functor (cat_postcomp a g)
A, B: AbGroup
forall (a b c : AbSES B A) (f : a $-> b),
Is0Functor (cat_precomp c f)
A, B: AbGroup
forall (a b c d : AbSES B A) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o g $o f $== h $o (g $o f)
A, B: AbGroup
forall (a b : AbSES B A) (f : a $-> b),
Id b $o f $== f
A, B: AbGroup
forall (a b : AbSES B A) (f : a $-> b),
f $o Id a $== f
  1: intros ? ?; apply is01cat_abses_path_data.
A, B: AbGroup
forall a b : AbSES B A, Is0Gpd (a $-> b)
A, B: AbGroup
forall (a b c : AbSES B A) (g : b $-> c),
Is0Functor (cat_postcomp a g)
A, B: AbGroup
forall (a b c : AbSES B A) (f : a $-> b),
Is0Functor (cat_precomp c f)
A, B: AbGroup
forall (a b c d : AbSES B A) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o g $o f $== h $o (g $o f)
A, B: AbGroup
forall (a b : AbSES B A) (f : a $-> b),
Id b $o f $== f
A, B: AbGroup
forall (a b : AbSES B A) (f : a $-> b),
f $o Id a $== f
  1: intros ? ?; apply is0gpd_abses_path_data.
A, B: AbGroup
forall (a b c : AbSES B A) (g : b $-> c),
Is0Functor (cat_postcomp a g)
A, B: AbGroup
forall (a b c : AbSES B A) (f : a $-> b),
Is0Functor (cat_precomp c f)
A, B: AbGroup
forall (a b c d : AbSES B A) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o g $o f $== h $o (g $o f)
A, B: AbGroup
forall (a b : AbSES B A) (f : a $-> b),
Id b $o f $== f
A, B: AbGroup
forall (a b : AbSES B A) (f : a $-> b),
f $o Id a $== f
  3-5: cbn; reflexivity.
A, B: AbGroup
forall (a b c : AbSES B A) (g : b $-> c),
Is0Functor (cat_postcomp a g)
A, B: AbGroup
forall (a b c : AbSES B A) (f : a $-> b),
Is0Functor (cat_precomp c f)
  1,2: intros E F G f;
  srapply Build_Is0Functor;
  intros p q h e; cbn.
A, B: AbGroup
E, F, G: AbSES B A
f: F $-> G
p, q: E $-> F
h: p $-> q
e: E
f.1 (p.1 e) = f.1 (q.1 e)
A, B: AbGroup
E, F, G: AbSES B A
f: E $-> F
p, q: F $-> G
h: p $-> q
e: E
p.1 (f.1 e) = q.1 (f.1 e)
  -
A, B: AbGroup
E, F, G: AbSES B A
f: F $-> G
p, q: E $-> F
h: p $-> q
e: E
f.1 (p.1 e) = f.1 (q.1 e) exact (ap f.1 (h e)).
  -
A, B: AbGroup
E, F, G: AbSES B A
f: E $-> F
p, q: F $-> G
h: p $-> q
e: E
p.1 (f.1 e) = q.1 (f.1 e) exact (h (f.1 e)).
Defined.

Global Instance is1gpd_abses {A B : AbGroup@{u}}
  : Is1Gpd (AbSES B A).
A, B: AbGroup
Is1Gpd (AbSES B A)
Proof.
A, B: AbGroup
Is1Gpd (AbSES B A)
  rapply Build_Is1Gpd;
    intros E F p e; cbn.
A, B: AbGroup
E, F: AbSES B A
p: E $-> F
e: E
(p.1)^-1 (p.1 e) = e
A, B: AbGroup
E, F: AbSES B A
p: E $-> F
e: F
p.1 ((p.1)^-1 e) = e
  -
A, B: AbGroup
E, F: AbSES B A
p: E $-> F
e: E
(p.1)^-1 (p.1 e) = e apply eissect.
  -
A, B: AbGroup
E, F: AbSES B A
p: E $-> F
e: F
p.1 ((p.1)^-1 e) = e apply eisretr.
Defined.

Global Instance hasmorext_abses `{Funext} {A B : AbGroup@{u}}
  : HasMorExt (AbSES B A).
H: Funext
A, B: AbGroup
HasMorExt (AbSES B A)
Proof.
H: Funext
A, B: AbGroup
HasMorExt (AbSES B A)
  srapply Build_HasMorExt;
    intros E F f g.
H: Funext
A, B: AbGroup
E, F: AbSES B A
f, g: E $-> F
IsEquiv GpdHom_path
  srapply isequiv_homotopic'; cbn.
H: Funext
A, B: AbGroup
E, F: AbSES B A
f, g: E $-> F
f = g <~> f.1 == g.1
H: Funext
A, B: AbGroup
E, F: AbSES B A
f, g: E $-> F
?Goal == GpdHom_path
  1: exact (((equiv_path_groupisomorphism _ _)^-1%equiv)
              oE (equiv_path_sigma_hprop _ _)^-1%equiv).
H: Funext
A, B: AbGroup
E, F: AbSES B A
f, g: E $-> F
(equiv_path_groupisomorphism f.1 g.1)^-1
oE (equiv_path_sigma_hprop f g)^-1 == GpdHom_path
  intro p; by induction p.
Defined.

(** *** Path data lemmas *)

(** We need to be able to work with path data as if they're paths. Our preference is to state things in terms of [abses_path_data_iso], since this lets us keep track of isomorphisms whose inverses compute. The "abstract" inverses produced by [short_five_lemma] do not compute well. *)

Definition equiv_path_abses_1 `{Univalence} {B A : AbGroup@{u}} {E : AbSES B A}
  : equiv_path_abses_iso (abses_path_data_1 E) = idpath.
H: Univalence
B, A: AbGroup
E: AbSES B A
equiv_path_abses_iso (abses_path_data_1 E) = 1%path
Proof.
H: Univalence
B, A: AbGroup
E: AbSES B A
equiv_path_abses_iso (abses_path_data_1 E) = 1%path
  apply (equiv_ap_inv' equiv_path_abses_iso).
H: Univalence
B, A: AbGroup
E: AbSES B A
equiv_path_abses_iso^-1
  (equiv_path_abses_iso (abses_path_data_1 E)) =
equiv_path_abses_iso^-1 1%path
  refine (eissect _ _ @ _).
H: Univalence
B, A: AbGroup
E: AbSES B A
abses_path_data_1 E = equiv_path_abses_iso^-1 1%path
  srapply path_sigma_hprop; simpl.
H: Univalence
B, A: AbGroup
E: AbSES B A
grp_iso_id =
{|
  grp_iso_homo :=
    {|
      grp_homo_map := idmap;
      grp_homo_ishomo :=
        {|
          monmor_sgmor := fun x y : E => 1%path;
          monmor_unitmor := 1%path
        |}
    |};
  isequiv_group_iso :=
    {|
      equiv_inv := idmap;
      eisretr := fun x : E => 1%path;
      eissect := fun x : E => 1%path;
      eisadj := fun x : E => 1%path
    |}
|}
  srapply equiv_path_groupisomorphism.
H: Univalence
B, A: AbGroup
E: AbSES B A
grp_iso_id ==
{|
  grp_iso_homo :=
    {|
      grp_homo_map := idmap;
      grp_homo_ishomo :=
        {|
          monmor_sgmor := fun x y : E => 1%path;
          monmor_unitmor := 1%path
        |}
    |};
  isequiv_group_iso :=
    {|
      equiv_inv := idmap;
      eisretr := fun x : E => 1%path;
      eissect := fun x : E => 1%path;
      eisadj := fun x : E => 1%path
    |}
|}
  reflexivity.
Defined.

Definition equiv_path_absesV_1 `{Univalence} {B A : AbGroup@{u}} {E : AbSES B A}
  : (@equiv_path_abses_iso _ B A E E)^-1 idpath = Id E.
H: Univalence
B, A: AbGroup
E: AbSES B A
equiv_path_abses_iso^-1 1%path = Id E
Proof.
H: Univalence
B, A: AbGroup
E: AbSES B A
equiv_path_abses_iso^-1 1%path = Id E
  apply moveR_equiv_M; symmetry.
H: Univalence
B, A: AbGroup
E: AbSES B A
(equiv_path_abses_iso^-1)^-1 (Id E) = 1%path
  apply equiv_path_abses_1.
Defined.

Definition abses_path_data_V `{Univalence} {B A : AbGroup@{u}} {E F : AbSES B A}
           (p : abses_path_data_iso E F)
  : (equiv_path_abses_iso p)^ = equiv_path_abses_iso (abses_path_data_inverse p).
H: Univalence
B, A: AbGroup
E, F: AbSES B A
p: abses_path_data_iso E F
(equiv_path_abses_iso p)^ =
equiv_path_abses_iso (abses_path_data_inverse p)
Proof.
H: Univalence
B, A: AbGroup
E, F: AbSES B A
p: abses_path_data_iso E F
(equiv_path_abses_iso p)^ =
equiv_path_abses_iso (abses_path_data_inverse p)
  revert p.
H: Univalence
B, A: AbGroup
E, F: AbSES B A
forall p : abses_path_data_iso E F,
(equiv_path_abses_iso p)^ =
equiv_path_abses_iso (abses_path_data_inverse p)
  equiv_intro (equiv_path_abses_iso (E:=E) (F:=F))^-1 p; induction p.
H: Univalence
B, A: AbGroup
E: AbSES B A
(equiv_path_abses_iso (equiv_path_abses_iso^-1 1))^ =
equiv_path_abses_iso
  (abses_path_data_inverse
     (equiv_path_abses_iso^-1 1%path))
  refine (ap _ (eisretr _ _) @ _); symmetry.
H: Univalence
B, A: AbGroup
E: AbSES B A
equiv_path_abses_iso
  (abses_path_data_inverse
     (equiv_path_abses_iso^-1 1%path)) = 1^
  nrefine (ap (equiv_path_abses_iso o abses_path_data_inverse) equiv_path_absesV_1 @ _).
H: Univalence
B, A: AbGroup
E: AbSES B A
equiv_path_abses_iso (abses_path_data_inverse (Id E)) =
1^
  refine (ap equiv_path_abses_iso gpd_strong_rev_1 @ _).
H: Univalence
B, A: AbGroup
E: AbSES B A
equiv_path_abses_iso (Id E) = 1^
  exact equiv_path_abses_1.
Defined.

(** Composition of path data corresponds to composition of paths. *)
Definition abses_path_compose_beta `{Univalence} {B A : AbGroup@{u}} {E F G : AbSES B A}
          (p : E = F) (q : F = G)
 : p @ q = equiv_path_abses_iso
             (abses_path_data_compose
                (equiv_path_abses_iso^-1 p) (equiv_path_abses_iso^-1 q)).
H: Univalence
B, A: AbGroup
E, F, G: AbSES B A
p: E = F
q: F = G
p @ q =
equiv_path_abses_iso
  (abses_path_data_compose (equiv_path_abses_iso^-1 p)
     (equiv_path_abses_iso^-1 q))
Proof.
H: Univalence
B, A: AbGroup
E, F, G: AbSES B A
p: E = F
q: F = G
p @ q =
equiv_path_abses_iso
  (abses_path_data_compose (equiv_path_abses_iso^-1 p)
     (equiv_path_abses_iso^-1 q))
  induction p, q.
H: Univalence
B, A: AbGroup
E: AbSES B A
1 @ 1 =
equiv_path_abses_iso
  (abses_path_data_compose
     (equiv_path_abses_iso^-1 1%path)
     (equiv_path_abses_iso^-1 1%path))
  refine (equiv_path_abses_1^ @ _).
H: Univalence
B, A: AbGroup
E: AbSES B A
equiv_path_abses_iso (abses_path_data_1 E) =
equiv_path_abses_iso
  (abses_path_data_compose
     (equiv_path_abses_iso^-1 1%path)
     (equiv_path_abses_iso^-1 1%path))
  apply (ap equiv_path_abses_iso).
H: Univalence
B, A: AbGroup
E: AbSES B A
abses_path_data_1 E =
abses_path_data_compose
  (equiv_path_abses_iso^-1 1%path)
  (equiv_path_abses_iso^-1 1%path)
  apply path_sigma_hprop.
H: Univalence
B, A: AbGroup
E: AbSES B A
(abses_path_data_1 E).1 =
(abses_path_data_compose
   (equiv_path_abses_iso^-1 1%path)
   (equiv_path_abses_iso^-1 1%path)).1
  by apply equiv_path_groupisomorphism.
Defined.

(** A second beta-principle where you start with path data instead of actual paths. *)
Definition abses_path_data_compose_beta `{Univalence} {B A : AbGroup@{u}} {E F G : AbSES B A}
           (p : abses_path_data_iso E F) (q : abses_path_data_iso F G)
  : equiv_path_abses_iso p @ equiv_path_abses_iso q
    = equiv_path_abses_iso (abses_path_data_compose p q).
H: Univalence
B, A: AbGroup
E, F, G: AbSES B A
p: abses_path_data_iso E F
q: abses_path_data_iso F G
equiv_path_abses_iso p @ equiv_path_abses_iso q =
equiv_path_abses_iso (abses_path_data_compose p q)
Proof.
H: Univalence
B, A: AbGroup
E, F, G: AbSES B A
p: abses_path_data_iso E F
q: abses_path_data_iso F G
equiv_path_abses_iso p @ equiv_path_abses_iso q =
equiv_path_abses_iso (abses_path_data_compose p q)
  generalize p, q.
H: Univalence
B, A: AbGroup
E, F, G: AbSES B A
p: abses_path_data_iso E F
q: abses_path_data_iso F G
forall (p : abses_path_data_iso E F)
(q : abses_path_data_iso F G),
equiv_path_abses_iso p @ equiv_path_abses_iso q =
equiv_path_abses_iso (abses_path_data_compose p q)
  equiv_intro ((equiv_path_abses_iso (E:=E) (F:=F))^-1) x.
H: Univalence
B, A: AbGroup
E, F, G: AbSES B A
p: abses_path_data_iso E F
q: abses_path_data_iso F G
x: E = F
forall q : abses_path_data_iso F G,
equiv_path_abses_iso (equiv_path_abses_iso^-1 x) @
equiv_path_abses_iso q =
equiv_path_abses_iso
  (abses_path_data_compose (equiv_path_abses_iso^-1 x)
     q)
  equiv_intro ((equiv_path_abses_iso (E:=F) (F:=G))^-1) y.
H: Univalence
B, A: AbGroup
E, F, G: AbSES B A
p: abses_path_data_iso E F
q: abses_path_data_iso F G
x: E = F
y: F = G
equiv_path_abses_iso (equiv_path_abses_iso^-1 x) @
equiv_path_abses_iso (equiv_path_abses_iso^-1 y) =
equiv_path_abses_iso
  (abses_path_data_compose (equiv_path_abses_iso^-1 x)
     (equiv_path_abses_iso^-1 y))
  refine ((eisretr _ _ @@ eisretr _ _) @ _).
H: Univalence
B, A: AbGroup
E, F, G: AbSES B A
p: abses_path_data_iso E F
q: abses_path_data_iso F G
x: E = F
y: F = G
x @ y =
equiv_path_abses_iso
  (abses_path_data_compose (equiv_path_abses_iso^-1 x)
     (equiv_path_abses_iso^-1 y))
  rapply abses_path_compose_beta.
Defined.

(** *** Homotopies of path data *)

Definition equiv_path_data_homotopy `{Univalence} {X : Type} {B A : AbGroup@{u}}
           (f g : X -> AbSES B A) : (f $=> g) <~> f == g.
H: Univalence
X: Type
B, A: AbGroup
f, g: X -> AbSES B A
(f $=> g) <~> f == g
Proof.
H: Univalence
X: Type
B, A: AbGroup
f, g: X -> AbSES B A
(f $=> g) <~> f == g
  srapply equiv_functor_forall_id; intro x; cbn.
H: Univalence
X: Type
B, A: AbGroup
f, g: X -> AbSES B A
x: X
abses_path_data_iso (f x) (g x) <~> f x = g x
  srapply equiv_path_abses_iso.
Defined.

Definition pmap_abses_const {B' A' B A : AbGroup@{u}} : AbSES B A -->* AbSES B' A'
  := Build_BasepointPreservingFunctor (const pt) (Id pt).

Definition to_pointed `{Univalence} {B' A' B A : AbGroup@{u}}
  : (AbSES B A -->* AbSES B' A') -> (AbSES B A ->* AbSES B' A')
  := fun f => Build_pMap _ _ f (equiv_path_abses_iso (bp_pointed f)).

Lemma pmap_abses_const_to_pointed `{Univalence} {B' A' B A : AbGroup@{u}}
  : pconst ==* to_pointed (@pmap_abses_const B' A' B A).
H: Univalence
B', A', B, A: AbGroup
pconst ==* to_pointed pmap_abses_const
Proof.
H: Univalence
B', A', B, A: AbGroup
pconst ==* to_pointed pmap_abses_const
  srapply Build_pHomotopy.
H: Univalence
B', A', B, A: AbGroup
pconst == to_pointed pmap_abses_const
H: Univalence
B', A', B, A: AbGroup
?p pt =
dpoint_eq pconst @
(dpoint_eq (to_pointed pmap_abses_const))^
  1: reflexivity.
H: Univalence
B', A', B, A: AbGroup
(fun x0 : AbSES' B A => 1%path) pt =
dpoint_eq pconst @
(dpoint_eq (to_pointed pmap_abses_const))^
  apply moveL_pV.
H: Univalence
B', A', B, A: AbGroup
1 @ dpoint_eq (to_pointed pmap_abses_const) =
dpoint_eq pconst
  refine (concat_1p _ @ _).
H: Univalence
B', A', B, A: AbGroup
dpoint_eq (to_pointed pmap_abses_const) =
dpoint_eq pconst
  apply equiv_path_abses_1.
Defined.

Lemma abses_ap_fmap `{Univalence} {B0 B1 A0 A1 : AbGroup@{u}}
      (f : AbSES B0 A0 -> AbSES B1 A1) `{!Is0Functor f, !Is1Functor f}
      {E F : AbSES B0 A0} (p : E $== F)
  : ap f (equiv_path_abses_iso p) = equiv_path_abses_iso (fmap f p).
H: Univalence
B0, B1, A0, A1: AbGroup
f: AbSES B0 A0 -> AbSES B1 A1
Is0Functor0: Is0Functor f
Is1Functor0: Is1Functor f
E, F: AbSES B0 A0
p: E $== F
ap f (equiv_path_abses_iso p) =
equiv_path_abses_iso (fmap f p)
Proof.
H: Univalence
B0, B1, A0, A1: AbGroup
f: AbSES B0 A0 -> AbSES B1 A1
Is0Functor0: Is0Functor f
Is1Functor0: Is1Functor f
E, F: AbSES B0 A0
p: E $== F
ap f (equiv_path_abses_iso p) =
equiv_path_abses_iso (fmap f p)
  revert p.
H: Univalence
B0, B1, A0, A1: AbGroup
f: AbSES B0 A0 -> AbSES B1 A1
Is0Functor0: Is0Functor f
Is1Functor0: Is1Functor f
E, F: AbSES B0 A0
forall p : E $== F,
ap f (equiv_path_abses_iso p) =
equiv_path_abses_iso (fmap f p)
  apply (equiv_ind equiv_path_abses_iso^-1%equiv);
    intro p.
H: Univalence
B0, B1, A0, A1: AbGroup
f: AbSES B0 A0 -> AbSES B1 A1
Is0Functor0: Is0Functor f
Is1Functor0: Is1Functor f
E, F: AbSES B0 A0
p: E = F
ap f
  (equiv_path_abses_iso
     ((equiv_path_abses_iso^-1)%equiv p)) =
equiv_path_abses_iso
  (fmap f ((equiv_path_abses_iso^-1)%equiv p))
  induction p.
H: Univalence
B0, B1, A0, A1: AbGroup
f: AbSES B0 A0 -> AbSES B1 A1
Is0Functor0: Is0Functor f
Is1Functor0: Is1Functor f
E: AbSES B0 A0
ap f
  (equiv_path_abses_iso
     ((equiv_path_abses_iso^-1)%equiv 1%path)) =
equiv_path_abses_iso
  (fmap f ((equiv_path_abses_iso^-1)%equiv 1%path))
  refine (ap (ap f) (eisretr _ _) @ _).
H: Univalence
B0, B1, A0, A1: AbGroup
f: AbSES B0 A0 -> AbSES B1 A1
Is0Functor0: Is0Functor f
Is1Functor0: Is1Functor f
E: AbSES B0 A0
ap f 1 =
equiv_path_abses_iso
  (fmap f ((equiv_path_abses_iso^-1)%equiv 1%path))
  nrefine (_ @ ap equiv_path_abses_iso _).
H: Univalence
B0, B1, A0, A1: AbGroup
f: AbSES B0 A0 -> AbSES B1 A1
Is0Functor0: Is0Functor f
Is1Functor0: Is1Functor f
E: AbSES B0 A0
ap f 1 = equiv_path_abses_iso ?Goal0
H: Univalence
B0, B1, A0, A1: AbGroup
f: AbSES B0 A0 -> AbSES B1 A1
Is0Functor0: Is0Functor f
Is1Functor0: Is1Functor f
E: AbSES B0 A0
?Goal0 =
fmap f ((equiv_path_abses_iso^-1)%equiv 1%path)
  2: {
H: Univalence
B0, B1, A0, A1: AbGroup
f: AbSES B0 A0 -> AbSES B1 A1
Is0Functor0: Is0Functor f
Is1Functor0: Is1Functor f
E: AbSES B0 A0
?Goal0 =
fmap f ((equiv_path_abses_iso^-1)%equiv 1%path) rapply path_hom.
H: Univalence
B0, B1, A0, A1: AbGroup
f: AbSES B0 A0 -> AbSES B1 A1
Is0Functor0: Is0Functor f
Is1Functor0: Is1Functor f
E: AbSES B0 A0
?Goal0 $==
fmap f ((equiv_path_abses_iso^-1)%equiv 1%path)
       srefine (_ $@ fmap2 _ _).
H: Univalence
B0, B1, A0, A1: AbGroup
f: AbSES B0 A0 -> AbSES B1 A1
Is0Functor0: Is0Functor f
Is1Functor0: Is1Functor f
E: AbSES B0 A0
?Goal0 $== fmap f ?f
H: Univalence
B0, B1, A0, A1: AbGroup
f: AbSES B0 A0 -> AbSES B1 A1
Is0Functor0: Is0Functor f
Is1Functor0: Is1Functor f
E: AbSES B0 A0
E $-> E
H: Univalence
B0, B1, A0, A1: AbGroup
f: AbSES B0 A0 -> AbSES B1 A1
Is0Functor0: Is0Functor f
Is1Functor0: Is1Functor f
E: AbSES B0 A0
?f $== (equiv_path_abses_iso^-1)%equiv 1%path
       2: exact (Id E).
H: Univalence
B0, B1, A0, A1: AbGroup
f: AbSES B0 A0 -> AbSES B1 A1
Is0Functor0: Is0Functor f
Is1Functor0: Is1Functor f
E: AbSES B0 A0
?Goal0 $== fmap f (Id E)
H: Univalence
B0, B1, A0, A1: AbGroup
f: AbSES B0 A0 -> AbSES B1 A1
Is0Functor0: Is0Functor f
Is1Functor0: Is1Functor f
E: AbSES B0 A0
Id E $== (equiv_path_abses_iso^-1)%equiv 1%path
       2: intro x; reflexivity.
H: Univalence
B0, B1, A0, A1: AbGroup
f: AbSES B0 A0 -> AbSES B1 A1
Is0Functor0: Is0Functor f
Is1Functor0: Is1Functor f
E: AbSES B0 A0
?Goal0 $== fmap f (Id E)
       exact (fmap_id f _)^$. }
H: Univalence
B0, B1, A0, A1: AbGroup
f: AbSES B0 A0 -> AbSES B1 A1
Is0Functor0: Is0Functor f
Is1Functor0: Is1Functor f
E: AbSES B0 A0
ap f 1 = equiv_path_abses_iso (Id (f E))
  exact equiv_path_abses_1^.
Defined.

Definition to_pointed_compose `{Univalence} {B0 B1 B2 A0 A1 A2 : AbGroup@{u}}
           (f : AbSES B0 A0 -->* AbSES B1 A1) (g : AbSES B1 A1 -->* AbSES B2 A2)
           `{!Is1Functor f, !Is1Functor g}
  : to_pointed g o* to_pointed f ==* to_pointed (g $o* f).
H: Univalence
B0, B1, B2, A0, A1, A2: AbGroup
f: AbSES B0 A0 -->* AbSES B1 A1
g: AbSES B1 A1 -->* AbSES B2 A2
Is1Functor0: Is1Functor f
Is1Functor1: Is1Functor g
to_pointed g o* to_pointed f ==* to_pointed (g $o* f)
Proof.
H: Univalence
B0, B1, B2, A0, A1, A2: AbGroup
f: AbSES B0 A0 -->* AbSES B1 A1
g: AbSES B1 A1 -->* AbSES B2 A2
Is1Functor0: Is1Functor f
Is1Functor1: Is1Functor g
to_pointed g o* to_pointed f ==* to_pointed (g $o* f)
  srapply Build_pHomotopy.
H: Univalence
B0, B1, B2, A0, A1, A2: AbGroup
f: AbSES B0 A0 -->* AbSES B1 A1
g: AbSES B1 A1 -->* AbSES B2 A2
Is1Functor0: Is1Functor f
Is1Functor1: Is1Functor g
to_pointed g o* to_pointed f == to_pointed (g $o* f)
H: Univalence
B0, B1, B2, A0, A1, A2: AbGroup
f: AbSES B0 A0 -->* AbSES B1 A1
g: AbSES B1 A1 -->* AbSES B2 A2
Is1Functor0: Is1Functor f
Is1Functor1: Is1Functor g
?p pt =
dpoint_eq (to_pointed g o* to_pointed f) @
(dpoint_eq (to_pointed (g $o* f)))^
  1: reflexivity.
H: Univalence
B0, B1, B2, A0, A1, A2: AbGroup
f: AbSES B0 A0 -->* AbSES B1 A1
g: AbSES B1 A1 -->* AbSES B2 A2
Is1Functor0: Is1Functor f
Is1Functor1: Is1Functor g
(fun x0 : AbSES' B0 A0 => 1%path) pt =
dpoint_eq (to_pointed g o* to_pointed f) @
(dpoint_eq (to_pointed (g $o* f)))^
  lazy beta.
H: Univalence
B0, B1, B2, A0, A1, A2: AbGroup
f: AbSES B0 A0 -->* AbSES B1 A1
g: AbSES B1 A1 -->* AbSES B2 A2
Is1Functor0: Is1Functor f
Is1Functor1: Is1Functor g
1%path =
dpoint_eq (to_pointed g o* to_pointed f) @
(dpoint_eq (to_pointed (g $o* f)))^
  nrapply moveL_pV.
H: Univalence
B0, B1, B2, A0, A1, A2: AbGroup
f: AbSES B0 A0 -->* AbSES B1 A1
g: AbSES B1 A1 -->* AbSES B2 A2
Is1Functor0: Is1Functor f
Is1Functor1: Is1Functor g
1 @ dpoint_eq (to_pointed (g $o* f)) =
dpoint_eq (to_pointed g o* to_pointed f)
  nrefine (concat_1p _ @ _).
H: Univalence
B0, B1, B2, A0, A1, A2: AbGroup
f: AbSES B0 A0 -->* AbSES B1 A1
g: AbSES B1 A1 -->* AbSES B2 A2
Is1Functor0: Is1Functor f
Is1Functor1: Is1Functor g
dpoint_eq (to_pointed (g $o* f)) =
dpoint_eq (to_pointed g o* to_pointed f)
  unfold pmap_compose, Build_pMap, pointed_fun, point_eq, dpoint_eq.
H: Univalence
B0, B1, B2, A0, A1, A2: AbGroup
f: AbSES B0 A0 -->* AbSES B1 A1
g: AbSES B1 A1 -->* AbSES B2 A2
Is1Functor0: Is1Functor f
Is1Functor1: Is1Functor g
dpoint_eq (to_pointed (g $o* f)) =
ap (to_pointed g) (dpoint_eq (to_pointed f)) @
dpoint_eq (to_pointed g)
  refine (_ @ ap (fun x => x @ _) _^).
H: Univalence
B0, B1, B2, A0, A1, A2: AbGroup
f: AbSES B0 A0 -->* AbSES B1 A1
g: AbSES B1 A1 -->* AbSES B2 A2
Is1Functor0: Is1Functor f
Is1Functor1: Is1Functor g
equiv_path_abses_iso (bp_pointed (g $o* f)) =
?Goal0 @ equiv_path_abses_iso (bp_pointed g)
H: Univalence
B0, B1, B2, A0, A1, A2: AbGroup
f: AbSES B0 A0 -->* AbSES B1 A1
g: AbSES B1 A1 -->* AbSES B2 A2
Is1Functor0: Is1Functor f
Is1Functor1: Is1Functor g
ap (to_pointed g) (dpoint_eq (to_pointed f)) = ?Goal0
  2: apply (abses_ap_fmap g).
H: Univalence
B0, B1, B2, A0, A1, A2: AbGroup
f: AbSES B0 A0 -->* AbSES B1 A1
g: AbSES B1 A1 -->* AbSES B2 A2
Is1Functor0: Is1Functor f
Is1Functor1: Is1Functor g
equiv_path_abses_iso (bp_pointed (g $o* f)) =
equiv_path_abses_iso (fmap g (bp_pointed f)) @
equiv_path_abses_iso (bp_pointed g)
  nrefine (_ @ (abses_path_data_compose_beta _ _)^).
H: Univalence
B0, B1, B2, A0, A1, A2: AbGroup
f: AbSES B0 A0 -->* AbSES B1 A1
g: AbSES B1 A1 -->* AbSES B2 A2
Is1Functor0: Is1Functor f
Is1Functor1: Is1Functor g
equiv_path_abses_iso (bp_pointed (g $o* f)) =
equiv_path_abses_iso
  (abses_path_data_compose 
     (fmap g (bp_pointed f)) 
     (bp_pointed g))
  nrapply (ap equiv_path_abses_iso).
H: Univalence
B0, B1, B2, A0, A1, A2: AbGroup
f: AbSES B0 A0 -->* AbSES B1 A1
g: AbSES B1 A1 -->* AbSES B2 A2
Is1Functor0: Is1Functor f
Is1Functor1: Is1Functor g
bp_pointed (g $o* f) =
abses_path_data_compose 
  (fmap g (bp_pointed f)) 
  (bp_pointed g)
  rapply path_hom.
H: Univalence
B0, B1, B2, A0, A1, A2: AbGroup
f: AbSES B0 A0 -->* AbSES B1 A1
g: AbSES B1 A1 -->* AbSES B2 A2
Is1Functor0: Is1Functor f
Is1Functor1: Is1Functor g
bp_pointed (g $o* f) $==
abses_path_data_compose 
  (fmap g (bp_pointed f)) 
  (bp_pointed g)
  reflexivity.
Defined.

Definition equiv_ptransformation_phomotopy `{Univalence} {B' A' B A : AbGroup@{u}}
           {f g : AbSES B A -->* AbSES B' A'}
  : f $=>* g <~> to_pointed f ==* to_pointed g.
H: Univalence
B', A', B, A: AbGroup
f, g: AbSES B A -->* AbSES B' A'
f $=>* g <~> to_pointed f ==* to_pointed g
Proof.
H: Univalence
B', A', B, A: AbGroup
f, g: AbSES B A -->* AbSES B' A'
f $=>* g <~> to_pointed f ==* to_pointed g
  refine (issig_pforall _ _ oE _).
H: Univalence
B', A', B, A: AbGroup
f, g: AbSES B A -->* AbSES B' A'
f $=>* g <~>
{f0
: forall x : AbSES B A,
  pfam_phomotopy (to_pointed f) (to_pointed g) x &
f0 pt =
dpoint (pfam_phomotopy (to_pointed f) (to_pointed g))}
  apply (equiv_functor_sigma' (equiv_path_data_homotopy f g)); intro h.
H: Univalence
B', A', B, A: AbGroup
f, g: AbSES B A -->* AbSES B' A'
h: f $=> g
h pt $== bp_pointed f $@ (bp_pointed g)^$ <~>
equiv_path_data_homotopy f g h pt =
dpoint (pfam_phomotopy (to_pointed f) (to_pointed g))
  refine (equiv_concat_r _ _ oE _).
H: Univalence
B', A', B, A: AbGroup
f, g: AbSES B A -->* AbSES B' A'
h: f $=> g
?Goal =
dpoint (pfam_phomotopy (to_pointed f) (to_pointed g))
H: Univalence
B', A', B, A: AbGroup
f, g: AbSES B A -->* AbSES B' A'
h: f $=> g
h pt $== bp_pointed f $@ (bp_pointed g)^$ <~>
equiv_path_data_homotopy f g h pt = ?Goal
  1: exact ((abses_path_data_compose_beta _ _)^ @ ap (fun x => _ @ x) (abses_path_data_V _)^).
H: Univalence
B', A', B, A: AbGroup
f, g: AbSES B A -->* AbSES B' A'
h: f $=> g
h pt $== bp_pointed f $@ (bp_pointed g)^$ <~>
equiv_path_data_homotopy f g h pt =
equiv_path_abses_iso
  (abses_path_data_compose (bp_pointed f)
     (abses_path_data_inverse (bp_pointed g)))
  refine (equiv_ap' equiv_path_abses_iso _ _ oE _).
H: Univalence
B', A', B, A: AbGroup
f, g: AbSES B A -->* AbSES B' A'
h: f $=> g
h pt $== bp_pointed f $@ (bp_pointed g)^$ <~>
h (1%equiv pt) =
abses_path_data_compose (bp_pointed f)
  (abses_path_data_inverse (bp_pointed g))
  refine (equiv_path_sigma_hprop _ _ oE _).
H: Univalence
B', A', B, A: AbGroup
f, g: AbSES B A -->* AbSES B' A'
h: f $=> g
h pt $== bp_pointed f $@ (bp_pointed g)^$ <~>
(h (1%equiv pt)).1 =
(abses_path_data_compose (bp_pointed f)
   (abses_path_data_inverse (bp_pointed g))).1
  apply equiv_path_groupisomorphism.
Defined.

(** *** Characterisation of loops of short exact sequences *)

(** Endomorphisms of the trivial short exact sequence in [AbSES B A] correspond to homomorphisms [B -> A]. *)
Lemma abses_endomorphism_trivial `{Funext} {B A : AbGroup@{u}}
  : {phi : GroupHomomorphism (point (AbSES B A)) (point (AbSES B A)) &
             (phi o inclusion _ == inclusion _)
             * (projection _ == projection _ o phi)}
      <~> (B $-> A).
H: Funext
B, A: AbGroup
{phi : GroupHomomorphism pt pt &
(phi o inclusion pt == inclusion pt) *
(projection pt == projection pt o phi)} <~> (B $-> A)
Proof.
H: Funext
B, A: AbGroup
{phi : GroupHomomorphism pt pt &
(phi o inclusion pt == inclusion pt) *
(projection pt == projection pt o phi)} <~> (B $-> A)
  srapply equiv_adjointify.
H: Funext
B, A: AbGroup
{phi : GroupHomomorphism pt pt &
(phi o inclusion pt == inclusion pt) *
(projection pt == projection pt o phi)} -> B $-> A
H: Funext
B, A: AbGroup
(B $-> A) ->
{phi : GroupHomomorphism pt pt &
(phi o inclusion pt == inclusion pt) *
(projection pt == projection pt o phi)}
H: Funext
B, A: AbGroup
?f o ?g == idmap
H: Funext
B, A: AbGroup
?g o ?f == idmap
  -
H: Funext
B, A: AbGroup
{phi : GroupHomomorphism pt pt &
(phi o inclusion pt == inclusion pt) *
(projection pt == projection pt o phi)} -> B $-> A intros [phi _].
H: Funext
B, A: AbGroup
phi: GroupHomomorphism pt pt
B $-> A
    exact (ab_biprod_pr1 $o phi $o ab_biprod_inr).
  -
H: Funext
B, A: AbGroup
(B $-> A) ->
{phi : GroupHomomorphism pt pt &
(phi o inclusion pt == inclusion pt) *
(projection pt == projection pt o phi)} intro f.
H: Funext
B, A: AbGroup
f: B $-> A
{phi : GroupHomomorphism pt pt &
(phi o inclusion pt == inclusion pt) *
(projection pt == projection pt o phi)}
    snrefine (_;_).
H: Funext
B, A: AbGroup
f: B $-> A
GroupHomomorphism pt pt
H: Funext
B, A: AbGroup
f: B $-> A
(fun phi : GroupHomomorphism pt pt =>
 (phi o inclusion pt == inclusion pt) *
 (projection pt == projection pt o phi)) ?proj1
    +
H: Funext
B, A: AbGroup
f: B $-> A
GroupHomomorphism pt pt refine (ab_biprod_rec ab_biprod_inl _).
H: Funext
B, A: AbGroup
f: B $-> A
B $-> ab_biprod A B
      refine (ab_biprod_corec f grp_homo_id).
    +
H: Funext
B, A: AbGroup
f: B $-> A
(fun phi : GroupHomomorphism pt pt =>
 (phi o inclusion pt == inclusion pt) *
 (projection pt == projection pt o phi))
  (ab_biprod_rec ab_biprod_inl
     (ab_biprod_corec f grp_homo_id)) split; intro x; cbn.
H: Funext
B, A: AbGroup
f: B $-> A
x: A
(x + f group_unit, group_unit + group_unit) =
(x, group_unit)
H: Funext
B, A: AbGroup
f: B $-> A
x: pt
snd x = group_unit + snd x
      *
H: Funext
B, A: AbGroup
f: B $-> A
x: A
(x + f group_unit, group_unit + group_unit) =
(x, group_unit) apply path_prod; cbn.
H: Funext
B, A: AbGroup
f: B $-> A
x: A
x + f group_unit = x
H: Funext
B, A: AbGroup
f: B $-> A
x: A
group_unit + group_unit = group_unit
        --
H: Funext
B, A: AbGroup
f: B $-> A
x: A
x + f group_unit = x exact (ap _ (grp_homo_unit f) @ right_identity _).
        --
H: Funext
B, A: AbGroup
f: B $-> A
x: A
group_unit + group_unit = group_unit exact (right_identity _).
      *
H: Funext
B, A: AbGroup
f: B $-> A
x: pt
snd x = group_unit + snd x exact (left_identity _)^.
  -
H: Funext
B, A: AbGroup
(fun
   X : {phi : GroupHomomorphism pt pt &
       (phi o inclusion pt == inclusion pt) *
       (projection pt == projection pt o phi)} =>
 (fun (phi : GroupHomomorphism pt pt)
    (_ : ((fun x : A => phi (inclusion pt x)) ==
          inclusion pt) *
         (projection pt ==
          (fun x : pt => projection pt (phi x)))) =>
  ab_biprod_pr1 $o phi $o ab_biprod_inr) X.1 X.2)
o (fun f : B $-> A =>
   (ab_biprod_rec ab_biprod_inl
      (ab_biprod_corec f grp_homo_id);
   ((fun x : A =>
     path_prod
       (x + f group_unit, group_unit + group_unit)
       (x, group_unit)
       (ap (sg_op x) (grp_homo_unit f) @
        right_identity x
        :
        fst
          (x + f group_unit, group_unit + group_unit) =
        fst (x, group_unit))
       (right_identity group_unit
        :
        snd
          (x + f group_unit, group_unit + group_unit) =
        snd (x, group_unit))
     :
     ab_biprod_rec ab_biprod_inl
       (ab_biprod_corec f grp_homo_id)
       (inclusion pt x) = inclusion pt x)
    :
    (fun x : A =>
     ab_biprod_rec ab_biprod_inl
       (ab_biprod_corec f grp_homo_id)
       (inclusion pt x)) == inclusion pt,
   (fun x : pt =>
    (left_identity (snd x))^
    :
    projection pt x =
    projection pt
      (ab_biprod_rec ab_biprod_inl
         (ab_biprod_corec f grp_homo_id) x))
   :
   projection pt ==
   (fun x : pt =>
    projection pt
      (ab_biprod_rec ab_biprod_inl
         (ab_biprod_corec f grp_homo_id) x))))) ==
idmap intro f.
H: Funext
B, A: AbGroup
f: B $-> A
ab_biprod_pr1 $o
ab_biprod_rec ab_biprod_inl
  (ab_biprod_corec f grp_homo_id) $o ab_biprod_inr = f
    rapply equiv_path_grouphomomorphism; intro b; cbn.
H: Funext
B, A: AbGroup
f: B $-> A
b: B
group_unit + f b = f b
    exact (left_identity _).
  -
H: Funext
B, A: AbGroup
(fun f : B $-> A =>
 (ab_biprod_rec ab_biprod_inl
    (ab_biprod_corec f grp_homo_id);
 ((fun x : A =>
   path_prod
     (x + f group_unit, group_unit + group_unit)
     (x, group_unit)
     (ap (sg_op x) (grp_homo_unit f) @
      right_identity x
      :
      fst (x + f group_unit, group_unit + group_unit) =
      fst (x, group_unit))
     (right_identity group_unit
      :
      snd (x + f group_unit, group_unit + group_unit) =
      snd (x, group_unit))
   :
   ab_biprod_rec ab_biprod_inl
     (ab_biprod_corec f grp_homo_id) (inclusion pt x) =
   inclusion pt x)
  :
  (fun x : A =>
   ab_biprod_rec ab_biprod_inl
     (ab_biprod_corec f grp_homo_id) (inclusion pt x)) ==
  inclusion pt,
 (fun x : pt =>
  (left_identity (snd x))^
  :
  projection pt x =
  projection pt
    (ab_biprod_rec ab_biprod_inl
       (ab_biprod_corec f grp_homo_id) x))
 :
 projection pt ==
 (fun x : pt =>
  projection pt
    (ab_biprod_rec ab_biprod_inl
       (ab_biprod_corec f grp_homo_id) x)))))
o (fun
     X : {phi : GroupHomomorphism pt pt &
         (phi o inclusion pt == inclusion pt) *
         (projection pt == projection pt o phi)} =>
   (fun (phi : GroupHomomorphism pt pt)
      (_ : ((fun x : A => phi (inclusion pt x)) ==
            inclusion pt) *
           (projection pt ==
            (fun x : pt => projection pt (phi x)))) =>
    ab_biprod_pr1 $o phi $o ab_biprod_inr) X.1 X.2) ==
idmap intros [phi [p q]].
H: Funext
B, A: AbGroup
phi: GroupHomomorphism pt pt
p: (fun x : A => phi (inclusion pt x)) ==
inclusion pt
q: projection pt ==
(fun x : pt => projection pt (phi x))
(ab_biprod_rec ab_biprod_inl
   (ab_biprod_corec
      (ab_biprod_pr1 $o phi $o ab_biprod_inr)
      grp_homo_id);
(fun x : A =>
 path_prod
   (x +
    (ab_biprod_pr1 $o phi $o ab_biprod_inr) group_unit,
   group_unit + group_unit) (x, group_unit)
   (ap (sg_op x)
      (grp_homo_unit
         (ab_biprod_pr1 $o phi $o ab_biprod_inr)) @
    right_identity x) (right_identity group_unit),
fun x : pt => (left_identity (snd x))^)) =
(phi; (p, q))
    apply path_sigma_hprop; cbn.
H: Funext
B, A: AbGroup
phi: GroupHomomorphism pt pt
p: (fun x : A => phi (inclusion pt x)) ==
inclusion pt
q: projection pt ==
(fun x : pt => projection pt (phi x))
ab_biprod_rec ab_biprod_inl
  (ab_biprod_corec
     (grp_homo_compose
        (grp_homo_compose ab_biprod_pr1 phi)
        ab_biprod_inr) grp_homo_id) = phi
    rapply equiv_path_grouphomomorphism; intros [a b]; cbn.
H: Funext
B, A: AbGroup
phi: GroupHomomorphism pt pt
p: (fun x : A => phi (inclusion pt x)) ==
inclusion pt
q: projection pt ==
(fun x : pt => projection pt (phi x))
a: A
b: B
(a + fst (phi (group_unit, b)), group_unit + b) =
phi (a, b)
    apply path_prod; cbn.
H: Funext
B, A: AbGroup
phi: GroupHomomorphism pt pt
p: (fun x : A => phi (inclusion pt x)) ==
inclusion pt
q: projection pt ==
(fun x : pt => projection pt (phi x))
a: A
b: B
a + fst (phi (group_unit, b)) = fst (phi (a, b))
H: Funext
B, A: AbGroup
phi: GroupHomomorphism pt pt
p: (fun x : A => phi (inclusion pt x)) ==
inclusion pt
q: projection pt ==
(fun x : pt => projection pt (phi x))
a: A
b: B
group_unit + b = snd (phi (a, b))
    +
H: Funext
B, A: AbGroup
phi: GroupHomomorphism pt pt
p: (fun x : A => phi (inclusion pt x)) ==
inclusion pt
q: projection pt ==
(fun x : pt => projection pt (phi x))
a: A
b: B
a + fst (phi (group_unit, b)) = fst (phi (a, b)) rewrite (ab_biprod_decompose a b).
H: Funext
B, A: AbGroup
phi: GroupHomomorphism pt pt
p: (fun x : A => phi (inclusion pt x)) ==
inclusion pt
q: projection pt ==
(fun x : pt => projection pt (phi x))
a: A
b: B
a + fst (phi (group_unit, b)) =
fst (phi ((a, group_unit) + (group_unit, b)))
      refine (_ @ (grp_homo_op (ab_biprod_pr1 $o phi) _ _)^).
H: Funext
B, A: AbGroup
phi: GroupHomomorphism pt pt
p: (fun x : A => phi (inclusion pt x)) ==
inclusion pt
q: projection pt ==
(fun x : pt => projection pt (phi x))
a: A
b: B
a + fst (phi (group_unit, b)) =
(ab_biprod_pr1 $o phi) (a, group_unit) +
(ab_biprod_pr1 $o phi) (group_unit, b)
      apply grp_cancelR; symmetry.
H: Funext
B, A: AbGroup
phi: GroupHomomorphism pt pt
p: (fun x : A => phi (inclusion pt x)) ==
inclusion pt
q: projection pt ==
(fun x : pt => projection pt (phi x))
a: A
b: B
(ab_biprod_pr1 $o phi) (a, group_unit) = a
      exact (ap fst (p a)).
    +
H: Funext
B, A: AbGroup
phi: GroupHomomorphism pt pt
p: (fun x : A => phi (inclusion pt x)) ==
inclusion pt
q: projection pt ==
(fun x : pt => projection pt (phi x))
a: A
b: B
group_unit + b = snd (phi (a, b)) rewrite (ab_biprod_decompose a b).
H: Funext
B, A: AbGroup
phi: GroupHomomorphism pt pt
p: (fun x : A => phi (inclusion pt x)) ==
inclusion pt
q: projection pt ==
(fun x : pt => projection pt (phi x))
a: A
b: B
group_unit + b =
snd (phi ((a, group_unit) + (group_unit, b)))
      refine (_ @ (grp_homo_op (ab_biprod_pr2 $o phi) _ _)^); cbn; symmetry.
H: Funext
B, A: AbGroup
phi: GroupHomomorphism pt pt
p: (fun x : A => phi (inclusion pt x)) ==
inclusion pt
q: projection pt ==
(fun x : pt => projection pt (phi x))
a: A
b: B
snd (phi (a, group_unit)) + snd (phi (group_unit, b)) =
group_unit + b
      exact (ap011 _ (ap snd (p a)) (q (group_unit, b))^).
Defined.

(** Consequently, the loop space of [AbSES B A] is [GroupHomomorphism B A]. (In fact, [B $-> A] are the loops of any short exact sequence, but the trivial case is easiest to show.) *)
Definition loops_abses `{Univalence} {A B : AbGroup}
  : (B $-> A) <~> loops (AbSES B A)
  := equiv_path_abses oE abses_endomorphism_trivial^-1.

(** We can transfer a loop of the trivial short exact sequence to any other. *)
Definition hom_loops_data_abses {A B : AbGroup} (E : AbSES B A)
  : (B $-> A) -> abses_path_data E E.
A, B: AbGroup
E: AbSES B A
(B $-> A) -> abses_path_data E E
Proof.
A, B: AbGroup
E: AbSES B A
(B $-> A) -> abses_path_data E E
  intro phi.
A, B: AbGroup
E: AbSES B A
phi: B $-> A
abses_path_data E E
  srefine (_; (_, _)).
A, B: AbGroup
E: AbSES B A
phi: B $-> A
GroupHomomorphism E E
A, B: AbGroup
E: AbSES B A
phi: B $-> A
?proj1 $o inclusion E == inclusion E
A, B: AbGroup
E: AbSES B A
phi: B $-> A
projection E == projection E $o ?proj1
  -
A, B: AbGroup
E: AbSES B A
phi: B $-> A
GroupHomomorphism E E exact (ab_homo_add grp_homo_id (inclusion E $o phi $o projection E)).
  -
A, B: AbGroup
E: AbSES B A
phi: B $-> A
ab_homo_add grp_homo_id
  (inclusion E $o phi $o projection E) $o inclusion E ==
inclusion E intro a; cbn.
A, B: AbGroup
E: AbSES B A
phi: B $-> A
a: A
inclusion E a +
inclusion E (phi (projection E (inclusion E a))) =
inclusion E a
    refine (ap (fun x => _ + inclusion E (phi x)) _ @ _).
A, B: AbGroup
E: AbSES B A
phi: B $-> A
a: A
projection E (inclusion E a) = ?Goal
A, B: AbGroup
E: AbSES B A
phi: B $-> A
a: A
inclusion E a + inclusion E (phi ?Goal) =
inclusion E a
    1: apply iscomplex_abses.
A, B: AbGroup
E: AbSES B A
phi: B $-> A
a: A
inclusion E a + inclusion E (phi (pconst a)) =
inclusion E a
    refine (ap (fun x => _ + x) (grp_homo_unit (inclusion E $o phi)) @ _).
A, B: AbGroup
E: AbSES B A
phi: B $-> A
a: A
inclusion E a + mon_unit = inclusion E a
    apply grp_unit_r.
  -
A, B: AbGroup
E: AbSES B A
phi: B $-> A
projection E ==
projection E $o
ab_homo_add grp_homo_id
  (inclusion E $o phi $o projection E) intro e; symmetry.
A, B: AbGroup
E: AbSES B A
phi: B $-> A
e: E
(projection E $o
 ab_homo_add grp_homo_id
   (inclusion E $o phi $o projection E)) e =
projection E e
    refine (grp_homo_op (projection E) _ _ @ _); cbn.
A, B: AbGroup
E: AbSES B A
phi: B $-> A
e: E
projection E e +
projection E (inclusion E (phi (projection E e))) =
projection E e
    refine (ap (fun x => _ + x) _ @  _).
A, B: AbGroup
E: AbSES B A
phi: B $-> A
e: E
projection E (inclusion E (phi (projection E e))) =
?Goal
A, B: AbGroup
E: AbSES B A
phi: B $-> A
e: E
projection E e + ?Goal = projection E e
    1: apply iscomplex_abses.
A, B: AbGroup
E: AbSES B A
phi: B $-> A
e: E
projection E e + pconst (phi (projection E e)) =
projection E e
    apply grp_unit_r.
Defined.

(** ** Morphisms of short exact sequences *)

(** A morphism between short exact sequences is a natural transformation between the underlying diagrams. *)
Record AbSESMorphism {A X B Y : AbGroup@{u}}
  {E : AbSES B A} {F : AbSES Y X} := {
    component1 : A $-> X;
    component2 : middle E $-> middle F;
    component3 : B $-> Y;
    left_square : (inclusion _) $o component1 == component2 $o (inclusion _);
    right_square : (projection _) $o component2 == component3 $o (projection _);
  }.

Arguments AbSESMorphism {A X B Y} E F.
Arguments Build_AbSESMorphism {_ _ _ _ _ _} _ _ _ _ _.

Definition issig_AbSESMorphism {A X B Y : AbGroup@{u}}
           {E : AbSES B A} {F : AbSES Y X}
  : { f : (A $-> X) * (middle E $-> middle F) * (B $-> Y)
          & ((inclusion _) $o (fst (fst f)) == (snd (fst f)) $o (inclusion _))
            * ((projection F) $o (snd (fst f)) == (snd f) $o (projection _)) }
      <~> AbSESMorphism E F := ltac:(make_equiv).

(** The identity morphism from [E] to [E]. *)
Lemma abses_morphism_id {A B : AbGroup@{u}} (E : AbSES B A)
  : AbSESMorphism E E.
A, B: AbGroup
E: AbSES B A
AbSESMorphism E E
Proof.
A, B: AbGroup
E: AbSES B A
AbSESMorphism E E
  snrapply (Build_AbSESMorphism grp_homo_id grp_homo_id grp_homo_id).
A, B: AbGroup
E: AbSES B A
inclusion E $o grp_homo_id ==
grp_homo_id $o inclusion E
A, B: AbGroup
E: AbSES B A
projection E $o grp_homo_id ==
grp_homo_id $o projection E
  1,2: reflexivity.
Defined.

Definition absesmorphism_compose {A0 A1 A2 B0 B1 B2 : AbGroup@{u}}
           {E : AbSES B0 A0} {F : AbSES B1 A1} {G : AbSES B2 A2}
           (g : AbSESMorphism F G) (f : AbSESMorphism E F)
  : AbSESMorphism E G.
A0, A1, A2, B0, B1, B2: AbGroup
E: AbSES B0 A0
F: AbSES B1 A1
G: AbSES B2 A2
g: AbSESMorphism F G
f: AbSESMorphism E F
AbSESMorphism E G
Proof.
A0, A1, A2, B0, B1, B2: AbGroup
E: AbSES B0 A0
F: AbSES B1 A1
G: AbSES B2 A2
g: AbSESMorphism F G
f: AbSESMorphism E F
AbSESMorphism E G
  rapply (Build_AbSESMorphism (component1 g $o component1 f)
                              (component2 g $o component2 f)
                              (component3 g $o component3 f)).
A0, A1, A2, B0, B1, B2: AbGroup
E: AbSES B0 A0
F: AbSES B1 A1
G: AbSES B2 A2
g: AbSESMorphism F G
f: AbSESMorphism E F
inclusion G $o (component1 g $o component1 f) ==
component2 g $o component2 f $o inclusion E
A0, A1, A2, B0, B1, B2: AbGroup
E: AbSES B0 A0
F: AbSES B1 A1
G: AbSES B2 A2
g: AbSESMorphism F G
f: AbSESMorphism E F
projection G $o (component2 g $o component2 f) ==
component3 g $o component3 f $o projection E
  -
A0, A1, A2, B0, B1, B2: AbGroup
E: AbSES B0 A0
F: AbSES B1 A1
G: AbSES B2 A2
g: AbSESMorphism F G
f: AbSESMorphism E F
inclusion G $o (component1 g $o component1 f) ==
component2 g $o component2 f $o inclusion E intro x; cbn.
A0, A1, A2, B0, B1, B2: AbGroup
E: AbSES B0 A0
F: AbSES B1 A1
G: AbSES B2 A2
g: AbSESMorphism F G
f: AbSESMorphism E F
x: A0
inclusion G (component1 g (component1 f x)) =
component2 g (component2 f (inclusion E x))
    exact (left_square g _ @ ap _ (left_square f _)).
  -
A0, A1, A2, B0, B1, B2: AbGroup
E: AbSES B0 A0
F: AbSES B1 A1
G: AbSES B2 A2
g: AbSESMorphism F G
f: AbSESMorphism E F
projection G $o (component2 g $o component2 f) ==
component3 g $o component3 f $o projection E intro x; cbn.
A0, A1, A2, B0, B1, B2: AbGroup
E: AbSES B0 A0
F: AbSES B1 A1
G: AbSES B2 A2
g: AbSESMorphism F G
f: AbSESMorphism E F
x: E
projection G (component2 g (component2 f x)) =
component3 g (component3 f (projection E x))
    exact (right_square g _ @ ap _ (right_square f _)).
Defined.

(** ** Characterization of split short exact sequences *)

(* We characterize trivial short exact sequences in [AbSES] as those for which [projection] splits. *)

(** If [projection E] splits, we get an induced map [fun e => e - s (projection E e)] from [E] to [ab_kernel (projection E)]. *)
Definition projection_split_to_kernel {B A : AbGroup} (E : AbSES B A)
           {s : B $-> E} (h : projection _ $o s == idmap)
  : (middle E) $-> (@ab_kernel E B (projection _)).
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
E $-> ab_kernel (projection E)
Proof.
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
E $-> ab_kernel (projection E)
  snrapply (grp_kernel_corec (G:=E) (A:=E)).
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
E $-> E
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
projection E $o ?g == grp_homo_const
  -
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
E $-> E refine (ab_homo_add grp_homo_id
              (grp_homo_compose ab_homo_negation (s $o (projection _)))).
  -
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
projection E $o
ab_homo_add grp_homo_id
  (grp_homo_compose ab_homo_negation
     (s $o projection E)) == grp_homo_const intro x; simpl.
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
x: E
projection E (x + - s (projection E x)) = group_unit
    refine (grp_homo_op (projection _) x _ @ _).
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
x: E
projection E x + projection E (- s (projection E x)) =
group_unit
    refine (ap (fun y => (projection _) x + y) _ @ right_inverse ((projection _) x)).
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
x: E
projection E (- s (projection E x)) = - projection E x
    refine (grp_homo_inv _ _ @ ap negate _ ).
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
x: E
projection E (s (projection E x)) = projection E x
    apply h.
Defined.

(** The composite [A -> E -> ab_kernel (projection E)] is [grp_cxfib]. *)
Lemma projection_split_to_kernel_beta {B A : AbGroup} (E : AbSES B A)
      {s : B $-> E} (h : (projection _) $o s == idmap)
  : (projection_split_to_kernel E h) $o (inclusion _) == grp_cxfib cx_isexact.
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
projection_split_to_kernel E h $o inclusion E ==
grp_cxfib cx_isexact
Proof.
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
projection_split_to_kernel E h $o inclusion E ==
grp_cxfib cx_isexact
  intro a.
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
a: A
(projection_split_to_kernel E h $o inclusion E) a =
grp_cxfib cx_isexact a
  apply path_sigma_hprop; cbn.
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
a: A
inclusion E a + - s (projection E (inclusion E a)) =
inclusion E a
  apply grp_cancelL1.
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
a: A
- s (projection E (inclusion E a)) = mon_unit
  refine (ap (fun x => - s x) _ @ _).
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
a: A
projection E (inclusion E a) = ?Goal
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
a: A
- s ?Goal = mon_unit
  1: rapply cx_isexact.
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
a: A
- s (pconst a) = mon_unit
  exact (ap _ (grp_homo_unit _) @ negate_mon_unit).
Defined.

(** The induced map [E -> ab_kernel (projection E) + B] is an isomorphism. We suffix it with 1 since it is the first composite in the desired isomorphism [E -> A + B]. *)
Definition projection_split_iso1 {B A : AbGroup} (E : AbSES B A)
           {s : GroupHomomorphism B E} (h : (projection _) $o s == idmap)
  : GroupIsomorphism E (ab_biprod (@ab_kernel E B (projection _)) B).
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
GroupIsomorphism E
  (ab_biprod (ab_kernel (projection E)) B)
Proof.
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
GroupIsomorphism E
  (ab_biprod (ab_kernel (projection E)) B)
  srapply Build_GroupIsomorphism.
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
GroupHomomorphism E
  (ab_biprod (ab_kernel (projection E)) B)
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
IsEquiv ?grp_iso_homo
  -
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
GroupHomomorphism E
  (ab_biprod (ab_kernel (projection E)) B) refine (ab_biprod_corec _ (projection _)).
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
E $-> ab_kernel (projection E)
    exact (projection_split_to_kernel E h).
  -
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
IsEquiv
  (ab_biprod_corec (projection_split_to_kernel E h)
     (projection E)) srapply isequiv_adjointify.
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
ab_biprod (ab_kernel (projection E)) B -> E
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
ab_biprod_corec (projection_split_to_kernel E h)
  (projection E) o ?g == idmap
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
?g
o ab_biprod_corec (projection_split_to_kernel E h)
    (projection E) == idmap
    +
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
ab_biprod (ab_kernel (projection E)) B -> E refine (ab_biprod_rec _ s).
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
ab_kernel (projection E) $-> E
      rapply subgroup_incl.
    +
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
ab_biprod_corec (projection_split_to_kernel E h)
  (projection E)
o ab_biprod_rec
    (subgroup_incl (grp_kernel (projection E))) s ==
idmap intros [a b]; simpl.
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
a: ab_kernel (projection E)
b: B
((a.1 + s b + - s (projection E (a.1 + s b));
 grp_homo_op (projection E) (a.1 + s b)
   (- s (projection E (a.1 + s b))) @
 (ap (fun y : B => projection E (a.1 + s b) + y)
    (grp_homo_inv (projection E)
       (s (projection E (a.1 + s b))) @
     ap negate (h (projection E (a.1 + s b)))) @
  right_inverse (projection E (a.1 + s b)))),
projection E (a.1 + s b)) = (a, b)
      apply path_prod'.
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
a: ab_kernel (projection E)
b: B
(a.1 + s b + - s (projection E (a.1 + s b));
grp_homo_op (projection E) (a.1 + s b)
  (- s (projection E (a.1 + s b))) @
(ap (fun y : B => projection E (a.1 + s b) + y)
   (grp_homo_inv (projection E)
      (s (projection E (a.1 + s b))) @
    ap negate (h (projection E (a.1 + s b)))) @
 right_inverse (projection E (a.1 + s b)))) = a
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
a: ab_kernel (projection E)
b: B
projection E (a.1 + s b) = b
      *
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
a: ab_kernel (projection E)
b: B
(a.1 + s b + - s (projection E (a.1 + s b));
grp_homo_op (projection E) (a.1 + s b)
  (- s (projection E (a.1 + s b))) @
(ap (fun y : B => projection E (a.1 + s b) + y)
   (grp_homo_inv (projection E)
      (s (projection E (a.1 + s b))) @
    ap negate (h (projection E (a.1 + s b)))) @
 right_inverse (projection E (a.1 + s b)))) = a srapply path_sigma_hprop; cbn.
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
a: ab_kernel (projection E)
b: B
a.1 + s b + - s (projection E (a.1 + s b)) = a.1
        refine ((associativity _ _ _)^ @ _).
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
a: ab_kernel (projection E)
b: B
a.1 + (s b + - s (projection E (a.1 + s b))) = a.1
        apply grp_cancelL1.
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
a: ab_kernel (projection E)
b: B
s b + - s (projection E (a.1 + s b)) = mon_unit
        refine (ap _ _ @ right_inverse _).
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
a: ab_kernel (projection E)
b: B
- s (projection E (a.1 + s b)) = - s b
        apply (ap negate).
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
a: ab_kernel (projection E)
b: B
s (projection E (a.1 + s b)) = s b
        apply (ap s).
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
a: ab_kernel (projection E)
b: B
projection E (a.1 + s b) = b
        refine (grp_homo_op (projection _) a.1 (s b) @ _).
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
a: ab_kernel (projection E)
b: B
projection E a.1 + projection E (s b) = b
        exact (ap (fun y => y + _) a.2 @ left_identity _ @ h b).
      *
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
a: ab_kernel (projection E)
b: B
projection E (a.1 + s b) = b refine (grp_homo_op (projection _) a.1 (s b) @ _).
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
a: ab_kernel (projection E)
b: B
projection E a.1 + projection E (s b) = b
        exact (ap (fun y => y + _) a.2 @ left_identity _ @ h b).
    +
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
ab_biprod_rec
  (subgroup_incl (grp_kernel (projection E))) s
o ab_biprod_corec (projection_split_to_kernel E h)
    (projection E) == idmap intro e; simpl.
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
e: E
e + - s (projection E e) + s (projection E e) = e
      by apply grp_moveR_gM.
Defined.

(** The full isomorphism [E -> A + B]. *)
Definition projection_split_iso {B A : AbGroup@{u}}
  (E : AbSES B A) {s : GroupHomomorphism B E}
  (h : (projection _) $o s == idmap)
  : GroupIsomorphism E (ab_biprod A B).
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
GroupIsomorphism E (ab_biprod A B)
Proof.
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
GroupIsomorphism E (ab_biprod A B)
  etransitivity (ab_biprod (ab_kernel _) B).
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
GroupIsomorphism E (ab_biprod (ab_kernel ?f) B)
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
GroupIsomorphism (ab_biprod (ab_kernel ?f) B)
  (ab_biprod A B)
  -
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
GroupIsomorphism E (ab_biprod (ab_kernel ?f) B) exact (projection_split_iso1 E h).
  -
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
GroupIsomorphism
  (ab_biprod (ab_kernel (projection E)) B)
  (ab_biprod A B) srapply (equiv_functor_ab_biprod
               (grp_iso_inverse _) grp_iso_id).
B, A: AbGroup
E: AbSES B A
s: GroupHomomorphism B E
h: projection E $o s == idmap
GroupIsomorphism A (ab_kernel (projection E))
    rapply grp_iso_cxfib.
Defined.

Proposition projection_split_beta {B A : AbGroup} (E : AbSES B A)
            {s : B $-> E} (h : (projection _) $o s == idmap)
  : projection_split_iso E h o (inclusion _) == ab_biprod_inl.
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
projection_split_iso E h o inclusion E ==
ab_biprod_inl
Proof.
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
projection_split_iso E h o inclusion E ==
ab_biprod_inl
  intro a.
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
a: A
projection_split_iso E h (inclusion E a) =
ab_biprod_inl a
  refine (ap _ (ab_corec_eta _ _ _ _) @ _).
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
a: A
equiv_functor_ab_biprod
  (grp_iso_inverse
     (grp_iso_cxfib (isexact_inclusion_projection E)))
  grp_iso_id
  (ab_biprod_corec
     (projection_split_to_kernel E h $o inclusion E)
     (projection E $o inclusion E) a) =
ab_biprod_inl a
  refine (ab_biprod_functor_beta _ _ _ _ _ @ _).
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
a: A
ab_biprod_corec
  (grp_iso_inverse
     (grp_iso_cxfib (isexact_inclusion_projection E)) $o
   (projection_split_to_kernel E h $o inclusion E))
  (grp_iso_id $o (projection E $o inclusion E)) a =
ab_biprod_inl a
  nrapply path_prod'.
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
a: A
(grp_iso_inverse
   (grp_iso_cxfib (isexact_inclusion_projection E)) $o
 (projection_split_to_kernel E h $o inclusion E)) a =
grp_homo_id a
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
a: A
(grp_iso_id $o (projection E $o inclusion E)) a =
grp_homo_const a
  2: rapply cx_isexact.
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
a: A
(grp_iso_inverse
   (grp_iso_cxfib (isexact_inclusion_projection E)) $o
 (projection_split_to_kernel E h $o inclusion E)) a =
grp_homo_id a
  refine (ap _ (projection_split_to_kernel_beta E h a) @ _).
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
a: A
grp_iso_inverse
  (grp_iso_cxfib (isexact_inclusion_projection E))
  (grp_cxfib cx_isexact a) = grp_homo_id a
  apply eissect.
Defined.

(** A short exact sequence [E] in [AbSES B A] is trivial if and only if [projection E] splits. *)
Proposition iff_abses_trivial_split `{Univalence}
  {B A : AbGroup@{u}} (E : AbSES B A)
  : {s : B $-> E & (projection _) $o s == idmap}
    <-> (E = point (AbSES B A)).
H: Univalence
B, A: AbGroup
E: AbSES B A
{s : B $-> E & projection E $o s == idmap} <-> E = pt
Proof.
H: Univalence
B, A: AbGroup
E: AbSES B A
{s : B $-> E & projection E $o s == idmap} <-> E = pt
  refine (iff_compose _ (iff_equiv equiv_path_abses_iso)); split.
H: Univalence
B, A: AbGroup
E: AbSES B A
{s : B $-> E & projection E $o s == idmap} ->
abses_path_data_iso E pt
H: Univalence
B, A: AbGroup
E: AbSES B A
abses_path_data_iso E pt ->
{s : B $-> E & projection E $o s == idmap}
  -
H: Univalence
B, A: AbGroup
E: AbSES B A
{s : B $-> E & projection E $o s == idmap} ->
abses_path_data_iso E pt intros [s h].
H: Univalence
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
abses_path_data_iso E pt
    exists (projection_split_iso E h).
H: Univalence
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
(projection_split_iso E h $o inclusion E ==
 inclusion pt) *
(projection E ==
 projection pt $o projection_split_iso E h)
    split.
H: Univalence
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
projection_split_iso E h $o inclusion E ==
inclusion pt
H: Univalence
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
projection E ==
projection pt $o projection_split_iso E h
    +
H: Univalence
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
projection_split_iso E h $o inclusion E ==
inclusion pt nrapply projection_split_beta.
    +
H: Univalence
B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
projection E ==
projection pt $o projection_split_iso E h reflexivity.
  -
H: Univalence
B, A: AbGroup
E: AbSES B A
abses_path_data_iso E pt ->
{s : B $-> E & projection E $o s == idmap} intros [phi [g h]].
H: Univalence
B, A: AbGroup
E: AbSES B A
phi: GroupIsomorphism E pt
g: phi $o inclusion E == inclusion pt
h: projection E == projection pt $o phi
{s : B $-> E & projection E $o s == idmap}
    exists (grp_homo_compose (grp_iso_inverse phi) ab_biprod_inr).
H: Univalence
B, A: AbGroup
E: AbSES B A
phi: GroupIsomorphism E pt
g: phi $o inclusion E == inclusion pt
h: projection E == projection pt $o phi
projection E $o
grp_homo_compose (grp_iso_inverse phi) ab_biprod_inr ==
idmap
    intro x; cbn.
H: Univalence
B, A: AbGroup
E: AbSES B A
phi: GroupIsomorphism E pt
g: phi $o inclusion E == inclusion pt
h: projection E == projection pt $o phi
x: B
projection E (phi^-1 (group_unit, x)) = x
    exact (h _ @ ap snd (eisretr _ _)).
Defined.

(** ** Constructions of short exact sequences *)

(** Any inclusion [i : A $-> E] determines a short exact sequence by quotienting. *)
Definition abses_from_inclusion `{Univalence}
  {A E : AbGroup@{u}} (i : A $-> E) `{IsEmbedding i}
  : AbSES (QuotientAbGroup E (grp_image_embedding i)) A.
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
AbSES (QuotientAbGroup E (grp_image_embedding i)) A
Proof.
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
AbSES (QuotientAbGroup E (grp_image_embedding i)) A
  srapply (Build_AbSES E i).
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
E $-> QuotientAbGroup E (grp_image_embedding i)
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
IsConnMap (Tr (-1)) ?projection
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
IsExact (Tr (-1)) i ?projection
  1: exact grp_quotient_map.
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
IsConnMap (Tr (-1)) grp_quotient_map
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
IsExact (Tr (-1)) i grp_quotient_map
  1: exact _.
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
IsExact (Tr (-1)) i grp_quotient_map
  srapply Build_IsExact.
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
IsComplex i grp_quotient_map
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
IsConnMap (Tr (-1)) (cxfib ?cx_isexact)
  -
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
IsComplex i grp_quotient_map srapply phomotopy_homotopy_hset.
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
grp_quotient_map o* i == pconst
    intro x.
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
x: A
(grp_quotient_map o* i) x = pconst x
    apply qglue; cbn.
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
x: A
hfiber i (- i x + mon_unit)
    exists (-x).
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
x: A
i (- x) = - i x + mon_unit
    exact (grp_homo_inv _ _ @ (grp_unit_r _)^).
  -
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
IsConnMap (Tr (-1))
  (cxfib
     (phomotopy_homotopy_hset
        ((fun x : A =>
          qglue
            ((- x;
             grp_homo_inv i x @ (grp_unit_r (- i x))^)
             :
             in_cosetL
               {|
                 normalsubgroup_subgroup :=
                   grp_image_embedding i;
                 normalsubgroup_isnormal :=
                   isnormal_ab_subgroup E
                    (grp_image_embedding i)
               |} (i x) mon_unit))
         :
         grp_quotient_map o* i == pconst))) snrapply (conn_map_homotopic (Tr (-1)) (B:=grp_kernel (@grp_quotient_map E _))).
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
A -> grp_kernel grp_quotient_map
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
?f ==
cxfib
  (phomotopy_homotopy_hset
     ((fun x : A =>
       qglue
         ((- x;
          grp_homo_inv i x @ (grp_unit_r (- i x))^)
          :
          in_cosetL
            {|
              normalsubgroup_subgroup :=
                grp_image_embedding i;
              normalsubgroup_isnormal :=
                isnormal_ab_subgroup E
                  (grp_image_embedding i)
            |} (i x) mon_unit))
      :
      grp_quotient_map o* i == pconst))
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
IsConnMap (Tr (-1)) ?f
    +
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
A -> grp_kernel grp_quotient_map exact (grp_kernel_quotient_iso _ o ab_image_in_embedding i).
    +
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
grp_kernel_quotient_iso (ab_image_embedding i)
o ab_image_in_embedding i ==
cxfib
  (phomotopy_homotopy_hset
     ((fun x : A =>
       qglue
         ((- x;
          grp_homo_inv i x @ (grp_unit_r (- i x))^)
          :
          in_cosetL
            {|
              normalsubgroup_subgroup :=
                grp_image_embedding i;
              normalsubgroup_isnormal :=
                isnormal_ab_subgroup E
                  (grp_image_embedding i)
            |} (i x) mon_unit))
      :
      grp_quotient_map o* i == pconst)) intro a.
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
a: A
grp_kernel_quotient_iso 
  (ab_image_embedding i) 
  (ab_image_in_embedding i a) =
cxfib
  (phomotopy_homotopy_hset
     (fun x : A =>
      qglue
        (- x;
        grp_homo_inv i x @ (grp_unit_r (- i x))^))) a
      by rapply (isinj_embedding (subgroup_incl _)).
    +
H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
IsConnMap (Tr (-1))
  (grp_kernel_quotient_iso (ab_image_embedding i)
   o ab_image_in_embedding i) rapply conn_map_isequiv.
Defined.

(** Conversely, given a short exact sequence [A -> E -> B], [A] is the kernel of [E -> B]. (We don't need exactness at [B], so we drop this assumption.) *)
Lemma abses_kernel_iso `{Funext} {A E B : AbGroup} (i : A $-> E) (p : E $-> B)
  `{IsEmbedding i, IsExact (Tr (-1)) _ _ _ i p}
  : GroupIsomorphism A (ab_kernel p).
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
GroupIsomorphism A (ab_kernel p)
Proof.
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
GroupIsomorphism A (ab_kernel p)
  snrapply Build_GroupIsomorphism.
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
GroupHomomorphism A (ab_kernel p)
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
IsEquiv ?grp_iso_homo
  -
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
GroupHomomorphism A (ab_kernel p) apply (grp_kernel_corec i).
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
p $o i == grp_homo_const
    rapply cx_isexact.
  -
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
IsEquiv (grp_kernel_corec i cx_isexact) apply isequiv_surj_emb.
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
IsConnMap (Tr (-1)) (grp_kernel_corec i cx_isexact)
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
IsEmbedding (grp_kernel_corec i cx_isexact)
    2: rapply (cancelL_mapinO _ (grp_kernel_corec _ _) _).
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
IsConnMap (Tr (-1)) (grp_kernel_corec i cx_isexact)
    intros [y q].
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
y: E
q: grp_kernel p y
IsConnected (Tr (-1))
  (hfiber (grp_kernel_corec i cx_isexact) (y; q))
    assert (a : Tr (-1) (hfiber i y)).
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
y: E
q: grp_kernel p y
Tr (-1) (hfiber i y)
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
y: E
q: grp_kernel p y
a: Tr (-1) (hfiber i y)
IsConnected (Tr (-1))
  (hfiber (grp_kernel_corec i cx_isexact) (y; q))
    1: by rapply isexact_preimage.
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
y: E
q: grp_kernel p y
a: Tr (-1) (hfiber i y)
IsConnected (Tr (-1))
  (hfiber (grp_kernel_corec i cx_isexact) (y; q))
    strip_truncations; destruct a as [a r].
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
y: E
q: grp_kernel p y
a: A
r: i a = y
IsConnected (Tr (-1))
  (hfiber (grp_kernel_corec i cx_isexact) (y; q))
    rapply contr_inhabited_hprop.
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
y: E
q: grp_kernel p y
a: A
r: i a = y
Tr (-1)
  (hfiber (grp_kernel_corec i cx_isexact) (y; q))
    refine (tr (a; _)); cbn.
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
y: E
q: grp_kernel p y
a: A
r: i a = y
(i a; cx_isexact a) = (y; q)
    apply path_sigma_hprop; cbn.
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
y: E
q: grp_kernel p y
a: A
r: i a = y
i a = y
    exact r.
Defined.

(** A computation rule for the inverse of [abses_kernel_iso i p]. *)
Lemma abses_kernel_iso_inv_beta `{Funext} {A E B : AbGroup} (i : A $-> E) (p : E $-> B)
  `{IsEmbedding i, IsExact (Tr (-1)) _ _ _ i p}
  : i o (abses_kernel_iso i p)^-1 == subgroup_incl _.
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
i o (abses_kernel_iso i p)^-1 ==
subgroup_incl (grp_kernel p)
Proof.
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
i o (abses_kernel_iso i p)^-1 ==
subgroup_incl (grp_kernel p)
  rapply (equiv_ind (abses_kernel_iso i p)); intro a.
H: Funext
A, E, B: AbGroup
i: A $-> E
p: E $-> B
IsEmbedding0: IsEmbedding i
H0: IsExact (Tr (-1)) i p
a: A
i ((abses_kernel_iso i p)^-1 (abses_kernel_iso i p a)) =
subgroup_incl (grp_kernel p) (abses_kernel_iso i p a)
  exact (ap i (eissect (abses_kernel_iso i p) _)).
Defined.

(* Any surjection [p : E $-> B] induces a short exact sequence by taking the kernel. *)
Lemma abses_from_surjection {E B : AbGroup@{u}} (p : E $-> B) `{IsSurjection p}
  : AbSES B (ab_kernel p).
E, B: AbGroup
p: E $-> B
IsSurjection0: IsConnMap (Tr (-1)) p
AbSES B (ab_kernel p)
Proof.
E, B: AbGroup
p: E $-> B
IsSurjection0: IsConnMap (Tr (-1)) p
AbSES B (ab_kernel p)
  srapply (Build_AbSES E _ p).
E, B: AbGroup
p: E $-> B
IsSurjection0: IsConnMap (Tr (-1)) p
ab_kernel p $-> E
E, B: AbGroup
p: E $-> B
IsSurjection0: IsConnMap (Tr (-1)) p
IsEmbedding ?inclusion
E, B: AbGroup
p: E $-> B
IsSurjection0: IsConnMap (Tr (-1)) p
IsExact (Tr (-1)) ?inclusion p
  1: exact (subgroup_incl _).
E, B: AbGroup
p: E $-> B
IsSurjection0: IsConnMap (Tr (-1)) p
IsEmbedding (subgroup_incl (grp_kernel p))
E, B: AbGroup
p: E $-> B
IsSurjection0: IsConnMap (Tr (-1)) p
IsExact (Tr (-1)) (subgroup_incl (grp_kernel p)) p
  1: exact _.
E, B: AbGroup
p: E $-> B
IsSurjection0: IsConnMap (Tr (-1)) p
IsExact (Tr (-1)) (subgroup_incl (grp_kernel p)) p
  snrapply Build_IsExact.
E, B: AbGroup
p: E $-> B
IsSurjection0: IsConnMap (Tr (-1)) p
IsComplex (subgroup_incl (grp_kernel p)) p
E, B: AbGroup
p: E $-> B
IsSurjection0: IsConnMap (Tr (-1)) p
IsConnMap (Tr (-1)) (cxfib ?cx_isexact)
  -
E, B: AbGroup
p: E $-> B
IsSurjection0: IsConnMap (Tr (-1)) p
IsComplex (subgroup_incl (grp_kernel p)) p apply phomotopy_homotopy_hset.
E, B: AbGroup
p: E $-> B
IsSurjection0: IsConnMap (Tr (-1)) p
p o* subgroup_incl (grp_kernel p) == pconst
    intros [e q]; cbn.
E, B: AbGroup
p: E $-> B
IsSurjection0: IsConnMap (Tr (-1)) p
e: E
q: grp_kernel p e
p e = ispointed_group B
    exact q.
  -
E, B: AbGroup
p: E $-> B
IsSurjection0: IsConnMap (Tr (-1)) p
IsConnMap (Tr (-1))
  (cxfib
     (phomotopy_homotopy_hset
        ((fun x : ab_kernel p =>
          (fun (e : E) (q : grp_kernel p e) =>
           q
           :
           (p o* subgroup_incl (grp_kernel p)) (e; q) =
           pconst (e; q)) x.1 x.2)
         :
         p o* subgroup_incl (grp_kernel p) == pconst))) rapply conn_map_isequiv.
Defined.

(** Conversely, given a short exact sequence [A -> E -> B], [B] is the cokernel of [A -> E]. In fact, we don't need exactness at [A], so we drop this from the statement. *)
Lemma abses_cokernel_iso `{Funext}
  {A E B : AbGroup@{u}} (f : A $-> E) (g : GroupHomomorphism E B)
  `{IsSurjection g, IsExact (Tr (-1)) _ _ _ f g}
  : GroupIsomorphism (ab_cokernel f) B.
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
GroupIsomorphism (ab_cokernel f) B
Proof.
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
GroupIsomorphism (ab_cokernel f) B
  snrapply Build_GroupIsomorphism.
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
GroupHomomorphism (ab_cokernel f) B
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
IsEquiv ?grp_iso_homo
  -
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
GroupHomomorphism (ab_cokernel f) B snrapply (quotient_abgroup_rec _ _ g).
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
forall n : E, grp_image f n -> g n = mon_unit
    intros e; rapply Trunc_rec; intros [a p].
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
e: E
a: A
p: f a = e
g e = mon_unit
    refine (ap _ p^ @ _).
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
e: E
a: A
p: f a = e
g (f a) = mon_unit
    rapply cx_isexact.
  -
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
IsEquiv
  (quotient_abgroup_rec 
     (grp_image f) B g
     (fun e : E =>
      Trunc_rec
        (fun X : {a : A & f a = e} =>
         (fun (a : A) (p : f a = e) =>
          ap g p^ @ cx_isexact a) X.1 X.2))) apply isequiv_surj_emb.
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
IsConnMap (Tr (-1))
  (quotient_abgroup_rec 
     (grp_image f) B g
     (fun e : E =>
      Trunc_rec
        (fun X : {a : A & f a = e} =>
         ap g (X.2)^ @ cx_isexact X.1)))
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
IsEmbedding
  (quotient_abgroup_rec 
     (grp_image f) B g
     (fun e : E =>
      Trunc_rec
        (fun X : {a : A & f a = e} =>
         ap g (X.2)^ @ cx_isexact X.1)))
    1: rapply cancelR_conn_map.
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
IsEmbedding
  (quotient_abgroup_rec 
     (grp_image f) B g
     (fun e : E =>
      Trunc_rec
        (fun X : {a : A & f a = e} =>
         ap g (X.2)^ @ cx_isexact X.1)))
    apply isembedding_isinj_hset.
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
isinj
  (quotient_abgroup_rec 
     (grp_image f) B g
     (fun e : E =>
      Trunc_rec
        (fun X : {a : A & f a = e} =>
         ap g (X.2)^ @ cx_isexact X.1)))
    srapply Quotient_ind_hprop; intro x.
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
x: E
(fun
   q : E /
       in_cosetL
         {|
           normalsubgroup_subgroup := grp_image f;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup E (grp_image f)
         |} =>
 forall x1 : ab_cokernel f,
 quotient_abgroup_rec 
   (grp_image f) B g
   (fun e : E =>
    Trunc_rec
      (fun X : {a : A & f a = e} =>
       ap g (X.2)^ @ cx_isexact X.1)) q =
 quotient_abgroup_rec 
   (grp_image f) B g
   (fun e : E =>
    Trunc_rec
      (fun X : {a : A & f a = e} =>
       ap g (X.2)^ @ cx_isexact X.1)) x1 -> 
 q = x1)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := grp_image f;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup E (grp_image f)
        |}) x)
    srapply Quotient_ind_hprop; intro y.
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
x, y: E
(fun
   q : E /
       in_cosetL
         {|
           normalsubgroup_subgroup := grp_image f;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup E (grp_image f)
         |} =>
 quotient_abgroup_rec 
   (grp_image f) B g
   (fun e : E =>
    Trunc_rec
      (fun X : {a : A & f a = e} =>
       ap g (X.2)^ @ cx_isexact X.1))
   (class_of
      (in_cosetL
         {|
           normalsubgroup_subgroup := grp_image f;
           normalsubgroup_isnormal :=
             isnormal_ab_subgroup E (grp_image f)
         |}) x) =
 quotient_abgroup_rec 
   (grp_image f) B g
   (fun e : E =>
    Trunc_rec
      (fun X : {a : A & f a = e} =>
       ap g (X.2)^ @ cx_isexact X.1)) q ->
 class_of
   (in_cosetL
      {|
        normalsubgroup_subgroup := grp_image f;
        normalsubgroup_isnormal :=
          isnormal_ab_subgroup E (grp_image f)
      |}) x = q)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := grp_image f;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup E (grp_image f)
        |}) y)
    intro p.
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
x, y: E
p: quotient_abgroup_rec 
  (grp_image f) B g
  (fun e : E =>
   Trunc_rec
     (fun X : {a : A & f a = e} =>
      ap g (X.2)^ @ cx_isexact X.1))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := grp_image f;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup E (grp_image f)
        |}) x) =
quotient_abgroup_rec 
  (grp_image f) B g
  (fun e : E =>
   Trunc_rec
     (fun X : {a : A & f a = e} =>
      ap g (X.2)^ @ cx_isexact X.1))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := grp_image f;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup E (grp_image f)
        |}) y)
class_of
  (in_cosetL
     {|
       normalsubgroup_subgroup := grp_image f;
       normalsubgroup_isnormal :=
         isnormal_ab_subgroup E (grp_image f)
     |}) x =
class_of
  (in_cosetL
     {|
       normalsubgroup_subgroup := grp_image f;
       normalsubgroup_isnormal :=
         isnormal_ab_subgroup E (grp_image f)
     |}) y
    apply qglue; cbn.
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
x, y: E
p: quotient_abgroup_rec 
  (grp_image f) B g
  (fun e : E =>
   Trunc_rec
     (fun X : {a : A & f a = e} =>
      ap g (X.2)^ @ cx_isexact X.1))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := grp_image f;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup E (grp_image f)
        |}) x) =
quotient_abgroup_rec 
  (grp_image f) B g
  (fun e : E =>
   Trunc_rec
     (fun X : {a : A & f a = e} =>
      ap g (X.2)^ @ cx_isexact X.1))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := grp_image f;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup E (grp_image f)
        |}) y)
Trunc (-1) {a : A & f a = - x + y}
    refine (isexact_preimage (Tr (-1)) _ _ (-x + y) _).
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
x, y: E
p: quotient_abgroup_rec 
  (grp_image f) B g
  (fun e : E =>
   Trunc_rec
     (fun X : {a : A & f a = e} =>
      ap g (X.2)^ @ cx_isexact X.1))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := grp_image f;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup E (grp_image f)
        |}) x) =
quotient_abgroup_rec 
  (grp_image f) B g
  (fun e : E =>
   Trunc_rec
     (fun X : {a : A & f a = e} =>
      ap g (X.2)^ @ cx_isexact X.1))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := grp_image f;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup E (grp_image f)
        |}) y)
g (- x + y) = pt
    refine (grp_homo_op _ _ _ @ _).
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
x, y: E
p: quotient_abgroup_rec 
  (grp_image f) B g
  (fun e : E =>
   Trunc_rec
     (fun X : {a : A & f a = e} =>
      ap g (X.2)^ @ cx_isexact X.1))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := grp_image f;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup E (grp_image f)
        |}) x) =
quotient_abgroup_rec 
  (grp_image f) B g
  (fun e : E =>
   Trunc_rec
     (fun X : {a : A & f a = e} =>
      ap g (X.2)^ @ cx_isexact X.1))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := grp_image f;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup E (grp_image f)
        |}) y)
g (- x) + g y = pt
    rewrite grp_homo_inv.
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
x, y: E
p: quotient_abgroup_rec 
  (grp_image f) B g
  (fun e : E =>
   Trunc_rec
     (fun X : {a : A & f a = e} =>
      ap g (X.2)^ @ cx_isexact X.1))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := grp_image f;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup E (grp_image f)
        |}) x) =
quotient_abgroup_rec 
  (grp_image f) B g
  (fun e : E =>
   Trunc_rec
     (fun X : {a : A & f a = e} =>
      ap g (X.2)^ @ cx_isexact X.1))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := grp_image f;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup E (grp_image f)
        |}) y)
- g x + g y = pt
    apply grp_moveL_M1^-1.
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
x, y: E
p: quotient_abgroup_rec 
  (grp_image f) B g
  (fun e : E =>
   Trunc_rec
     (fun X : {a : A & f a = e} =>
      ap g (X.2)^ @ cx_isexact X.1))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := grp_image f;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup E (grp_image f)
        |}) x) =
quotient_abgroup_rec 
  (grp_image f) B g
  (fun e : E =>
   Trunc_rec
     (fun X : {a : A & f a = e} =>
      ap g (X.2)^ @ cx_isexact X.1))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := grp_image f;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup E (grp_image f)
        |}) y)
g y = g x
    exact p^.
Defined.

Definition abses_cokernel_iso_inv_beta `{Funext}
  {A E B : AbGroup} (f : A $-> E) (g : GroupHomomorphism E B)
  `{IsSurjection g, IsExact (Tr (-1)) _ _ _ f g}
  : (abses_cokernel_iso f g)^-1 o g == grp_quotient_map.
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
(abses_cokernel_iso f g)^-1 o g == grp_quotient_map
Proof.
H: Funext
A, E, B: AbGroup
f: A $-> E
g: GroupHomomorphism E B
IsSurjection0: IsConnMap (Tr (-1)) g
H0: IsExact (Tr (-1)) f g
(abses_cokernel_iso f g)^-1 o g == grp_quotient_map
  intro x; by apply moveR_equiv_V.
Defined.