Core.v

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

Local Open Scope pointed_scope.
Local Open Scope path_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.

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]. *)
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
  snapply 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))) 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))
     ((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))
     ((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)) ((a, b); p)
    exists a.B, A: AbGroup
a: A
b: B
p: b = ispointed_group B
((a, group_unit); 1) = ((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. *)
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)
  exact 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 : Hom (A:=AbGroup) 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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 + 0 = f
    apply grp_unit_r.
  -B, A: AbGroup
E, F: AbSES B A
phi: E $-> F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
IsEmbedding phi apply isembedding_istrivial_kernel.B, A: AbGroup
E, F: AbSES B A
phi: E $-> F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
IsTrivialGroup (grp_kernel phi)
    intros e p.B, A: AbGroup
E, F: AbSES B A
phi: E $-> F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
e: E
p: grp_kernel phi e
trivial_subgroup E e
    assert (a : Tr (-1) (hfiber (inclusion E) e)).B, A: AbGroup
E, F: AbSES B A
phi: E $-> F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
e: E
p: grp_kernel phi e
Tr (-1) (hfiber (inclusion E) e)
B, A: AbGroup
E, F: AbSES B A
phi: E $-> F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
e: E
p: grp_kernel phi e
a: Tr (-1) (hfiber (inclusion E) e)
trivial_subgroup E e
    1: {B, A: AbGroup
E, F: AbSES B A
phi: E $-> F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
e: E
p: grp_kernel phi e
Tr (-1) (hfiber (inclusion E) e) refine (isexact_preimage _ (inclusion E) (projection E) _ _).B, A: AbGroup
E, F: AbSES B A
phi: E $-> F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
e: E
p: grp_kernel phi e
projection E e = pt
         exact (p1 e @ ap (projection F) p @ grp_homo_unit _). }B, A: AbGroup
E, F: AbSES B A
phi: E $-> F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
e: E
p: grp_kernel phi e
a: Tr (-1) (hfiber (inclusion E) e)
trivial_subgroup E e
    strip_truncations.B, A: AbGroup
E, F: AbSES B A
phi: E $-> F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
e: E
p: grp_kernel phi e
a: hfiber (inclusion E) e
trivial_subgroup E e
    refine (a.2^ @ ap (inclusion E ) _ @ grp_homo_unit (inclusion E)).B, A: AbGroup
E, F: AbSES B A
phi: E $-> F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
e: E
p: grp_kernel phi e
a: hfiber (inclusion E) e
a.1 = 0
    rapply (isinj_embedding (inclusion F) _ _).B, A: AbGroup
E, F: AbSES B A
phi: E $-> F
p0: phi $o inclusion E == inclusion F
p1: projection E == projection F $o phi
e: E
p: grp_kernel phi e
a: hfiber (inclusion E) e
inclusion F a.1 = inclusion F 0
    exact ((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 : Hom (A:=AbGroup) 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: 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 : 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 *)

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).

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).

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).

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)))).

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.

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

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 *)
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)
  snapply 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.

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.

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)
  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
Proof.H: Univalence
B, A: AbGroup
E: AbSES B A
equiv_path_abses_iso (abses_path_data_1 E) = 1
  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
  refine (eissect _ _ @ _).H: Univalence
B, A: AbGroup
E: AbSES B A
abses_path_data_1 E = equiv_path_abses_iso^-1 1
  srapply path_sigma_hprop; simpl.H: Univalence
B, A: AbGroup
E: AbSES B A
grp_iso_id =
{|
  grp_iso_homo :=
    {|
      grp_homo_map := idmap;
      issemigrouppreserving_grp_homo :=
        abstract_algebra.id_sg_morphism
    |};
  isequiv_group_iso :=
    {|
      equiv_inv := idmap;
      eisretr := fun x : E => 1;
      eissect := fun x : E => 1;
      eisadj := fun x : E => 1
    |}
|}
  srapply equiv_path_groupisomorphism.H: Univalence
B, A: AbGroup
E: AbSES B A
grp_iso_id ==
{|
  grp_iso_homo :=
    {|
      grp_homo_map := idmap;
      issemigrouppreserving_grp_homo :=
        abstract_algebra.id_sg_morphism
    |};
  isequiv_group_iso :=
    {|
      equiv_inv := idmap;
      eisretr := fun x : E => 1;
      eissect := fun x : E => 1;
      eisadj := fun x : E => 1
    |}
|}
  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 = Id E
Proof.H: Univalence
B, A: AbGroup
E: AbSES B A
equiv_path_abses_iso^-1 1 = 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
  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))
  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)) =
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)
     (equiv_path_abses_iso^-1 1))
  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)
     (equiv_path_abses_iso^-1 1))
  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)
  (equiv_path_abses_iso^-1 1)
  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)
   (equiv_path_abses_iso^-1 1)).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
  exact 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) 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
  exact 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)) =
equiv_path_abses_iso
  (fmap f (equiv_path_abses_iso^-1%equiv 1))
  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))
  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)
  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) tapply 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)
       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
       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
       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) 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 =
dpoint_eq (to_pointed g o* to_pointed f) @
(dpoint_eq (to_pointed (g $o* f)))^
  napply 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))
  napply (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)
  tapply 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
      exact (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 (grp_prod_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, 0) + (0, 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, 0) +
(ab_biprod_pr1 $o phi) (0, 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, 0) = 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 (grp_prod_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, 0) + (0, 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, 0)) + snd (phi (0, 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
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
E $-> E exact (grp_homo_id + (inclusion E $o phi $o projection E)).
  -A, B: AbGroup
E: AbSES B A
phi: B $-> A
(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 + 0 = inclusion E a
    apply grp_unit_r.
  -A, B: AbGroup
E: AbSES B A
phi: B $-> A
projection E ==
projection E $o
(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
 (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
  snapply (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)
  snapply (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 (grp_homo_id - (s $o projection _)).
  -B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
projection E $o (grp_homo_id - 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 (-) _).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)) = 0
  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 = 0
  1: tapply cx_isexact.B, A: AbGroup
E: AbSES B A
s: B $-> E
h: projection E $o s == idmap
a: A
- s (pconst a) = 0
  exact (ap _ (grp_homo_unit _) @ grp_inv_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 inv (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 inv (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 inv (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)) = 0
        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
  (* The next two lines might help the reader, but both are definitional equalities:
  lhs napply (ap _ (grp_prod_corec_natural _ _ _ _)).
  lhs napply ab_biprod_functor_beta.
  *)
  napply 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
 ab_biprod_pr1)
  (projection_split_iso1 E h (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 ab_biprod_pr2)
  (projection_split_iso1 E h (inclusion E a)) =
grp_homo_const a
  2: tapply 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
 ab_biprod_pr1)
  (projection_split_iso1 E h (inclusion E a)) =
grp_homo_id a
  (* The LHS of the remaining goal is definitionally equal to
       (grp_iso_inverse (grp_iso_cxfib (isexact_inclusion_projection E)) $o
         (projection_split_to_kernel E h $o inclusion E)) a
     allowing us to do: *)
  lhs napply (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 napply 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 + 0)
    exists (-x).H: Univalence
A, E: AbGroup
i: A $-> E
IsEmbedding0: IsEmbedding i
x: A
i (- x) = - i x + 0
    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) 0))
         :
         grp_quotient_map o* i == pconst))) snapply (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) 0))
      :
      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) 0))
      :
      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)
  snapply 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
    exact 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: tapply (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 tapply 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
  snapply 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
  snapply 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 snapply (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 = 0
    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 = 0
    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) = 0
    tapply 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 : {x : A & f x = 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 : {x : A & f x = 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 : {x : A & f x = 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 : {x : A & f x = 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
IsInjective
  (quotient_abgroup_rec 
     (grp_image f) B g
     (fun e : E =>
      Trunc_rec
        (fun X : {x : A & f x = e} =>
         ap g (X.2)^ @ cx_isexact X.1)))
    srapply Quotient_ind2_hprop; intros 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
(fun
   x
    y : 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 : {x0 : A & f x0 = e} =>
       ap g (X.2)^ @ cx_isexact X.1)) x =
 quotient_abgroup_rec 
   (grp_image f) B g
   (fun e : E =>
    Trunc_rec
      (fun X : {x0 : A & f x0 = e} =>
       ap g (X.2)^ @ cx_isexact X.1)) y -> 
 x = 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)
    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 : {x : A & f x = 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 : {x : A & f x = 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 : {x : A & f x = 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 : {x : A & f x = 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) {x0 : A & f x0 = - 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 : {x : A & f x = 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 : {x : A & f x = 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 : {x : A & f x = 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 : {x : A & f x = 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 : {x : A & f x = 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 : {x : A & f x = 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 : {x : A & f x = 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 : {x : A & f x = 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.