hfiber_cxfib' {A B C : AbGroup} (E : AbSES C B) (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt) := {Y : AbSES C A & hfiber_abses_path (cxfib' E Y) (F; p)}. Local pr2_cxfib' `{Univalence} {A B C : AbGroup} {E : AbSES C B} (U : AbSES C A) : equiv_ptransformation_phomotopy (iscomplex_abses_pullback' _ _ (iscomplex_abses E)) U = equiv_path_abses_iso (cxfib' E U).2. Proof. change (equiv_ptransformation_phomotopy (iscomplex_abses_pullback' _ _ (iscomplex_abses E)) U) with (equiv_path_abses_iso ((iscomplex_abses_pullback' _ _ (iscomplex_abses E)).1 U)). apply (ap equiv_path_abses_iso). rapply path_hom. refine (_ $@R abses_pullback_compose' (inclusion E) (projection E) U); unfold trans_comp. refine (_ $@R abses_pullback_homotopic' (projection E $o inclusion E) grp_homo_const (iscomplex_abses E) U). reflexivity. 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.