`{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). Proof. srapply Build_pHomotopy. 1: reflexivity. lazy beta. nrapply moveL_pV. nrefine (concat_1p _ @ _). unfold pmap_compose, Build_pMap, pointed_fun, point_eq, dpoint_eq. refine (_ @ ap (fun x => x @ _) _^). 2: apply (abses_ap_fmap g). nrefine (_ @ (abses_path_data_compose_beta _ _)^). nrapply (ap equiv_path_abses_iso). rapply path_hom. reflexivity. 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.