path_hfiber_cxfib' {A B C : AbGroup} {E : AbSES C B} {F : AbSES (middle E) A} {p : abses_pullback (inclusion E) F $== pt} (X Y : hfiber_cxfib' (B:=B) E F p) : Type. Proof. refine (sig (fun q0 : X.1 $== Y.1 => _)). exact ((fmap (abses_pullback (projection E)) q0)^$ $@ X.2.1 $== Y.2.1). 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.