proposition: Lemma fmap_hfiber_abses_lemma `{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: 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.
imports: Basics Types HSet HFiber Limits.Pullback WildCat Pointed.Core Homotopy.ExactSequence Groups.QuotientGroup AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct AbSES.Core AbSES.Pullback Modalities.Identity Modalities.Modality Truncations.Core