fact: Definition connecting_map {F X Y} (i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f} : loops Y ->* F := i_fiberseq (connect_fiberseq i f).
imports: Basics Types SuccessorStructure WildCat Pointed Modalities.Identity Modalities.Descent Truncations HFiber ObjectClassifier