`{Univalence} {A B B' : AbGroup} (f : B' $-> B) (X Y : graph_hfiber (abses_pullback (A:=A) f) pt) (Q : hfiber_abses_path X Y) : fmap (abses_pullback f) Q.1^$ $o Y.2^$ $== X.2^$. Proof. generalize Q. equiv_intro (equiv_hfiber_abses_pullback _ X Y)^-1%equiv p; induction p. refine ((_ $@R _) $@ _). { Unshelve. 2: exact (Id _). refine (fmap2 _ _ $@ fmap_id _ _). intro x; reflexivity. } exact (cat_idl _). 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.