fact: Definition connecting_map_family {Y : pType} (P : pFam Y) : loops Y ->* [P pt, dpoint P].
imports: Basics Types SuccessorStructure WildCat Pointed Modalities.Identity Modalities.Descent Truncations HFiber ObjectClassifier