Core.v

From HoTT Require Import Basics Types Truncations.Core.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
From HoTT.WildCat Require Import Core Equiv Induced NatTrans.
Require Import HSet Pointed.Core Pointed.Loops.
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.