{B A : AbGroup@{u}} {E F : AbSES B A} : (E $-> F) -> (F $-> E). Proof. intros [phi [p q]]. srefine (_; (_,_)). - exact (grp_iso_inverse phi). - intro a. exact (ap _ (p a)^ @ eissect _ (inclusion E a)). - intro a; simpl. exact (ap (projection F) (eisretr _ _)^ @ (q _)^). 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.