fact: Definition abses_pullback_compose `{Univalence} {A B0 B1 B2 : AbGroup@{u}} (f : B0 $-> B1) (g : B1 $-> B2) : abses_pullback (A:=A) f o abses_pullback g == abses_pullback (g $o f) := fun x => equiv_path_abses_iso (abses_pullback_compose' f g x).
imports: Basics Types HSet Limits.Pullback WildCat Pointed.Core Homotopy.ExactSequence Modalities.ReflectiveSubuniverse AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct AbSES.Core AbSES.DirectSum