fact: Definition pequiv_cxfib {F X Y : pType} {i : F ->* X} {f : X ->* Y} `{IsExact purely F X Y i f} : F <~>* pfiber f := Build_pEquiv _ _ (cxfib cx_isexact) _.
imports: Basics Types SuccessorStructure WildCat Pointed Modalities.Identity Modalities.Descent Truncations HFiber ObjectClassifier