fact: Definition fiberseq_loops {F X Y} (fs : FiberSeq F X Y) : FiberSeq (loops F) (loops X) (loops Y).
imports: Basics Types SuccessorStructure WildCat Pointed Modalities.Identity Modalities.Descent Truncations HFiber ObjectClassifier