fact: Definition iscomplex_trivial {X Y : pType} (f : X ->* Y) : IsComplex (@pconst pUnit X) f.
imports: Basics Types SuccessorStructure WildCat Pointed Modalities.Identity Modalities.Descent Truncations HFiber ObjectClassifier