{B A : AbGroup@{u}} (E F : AbSES B A) := {phi : GroupIsomorphism E F & (phi $o inclusion _ == inclusion _) * (projection _ == projection _ $o phi)}. Local Lemma shuffle_abses_path_data_iso `{Funext} {B A : AbGroup@{u}} (E F : AbSES B A) : ( E F) <~> {phi : GroupIsomorphism E F & (phi $o inclusion _ == inclusion _) * (projection _ $o grp_iso_inverse phi == projection _)}. Proof. srapply equiv_functor_sigma_id; intro phi. srapply equiv_functor_prod'. 1: exact equiv_idmap. srapply (equiv_functor_forall' phi^-1); intro e; cbn. apply equiv_concat_r. exact (ap _ (eisretr _ _)). Defined.
Require Import Basics Types Truncations.Core. Require Import HSet WildCat. Require Import Groups.QuotientGroup Groups.ShortExactSequence. Require Import AbelianGroup AbGroups.Biproduct AbHom. Require Import Homotopy.ExactSequence Pointed. Require Import Modalities.ReflectiveSubuniverse.