`{Univalence} {A B C : AbGroup} {E : AbSES C B} (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt) (U V : hfiber_cxfib' E F p) (q : U.1 = V.1) : (transport (fun Y : AbSES C A => hfiber_abses_path (cxfib' E Y) (F; p)) q U.2).1 = fmap (abses_pullback (projection E)) (equiv_path_abses_iso^-1 q^) $@ U.2.1. Proof. induction q. refine (ap pr1 (transport_1 _ _) @ _). refine (_ @ ap (fun x => fmap (abses_pullback (projection E)) x $@ _) equiv_path_absesV_1^). refine (_ @ ap (fun x => x $@ _) (fmap_id_strong _ _)^). exact (cat_idr_strong _)^. Defined.
Require Import Basics Types HSet HFiber Limits.Pullback. Require Import WildCat Pointed.Core Homotopy.ExactSequence. Require Import Groups.QuotientGroup. Require Import AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct. Require Import AbSES.Core AbSES.Pullback. Require Import Modalities.Identity Modalities.Modality Truncations.Core.