fact: Definition i_fiberseq {F X Y} (fs : FiberSeq F X Y) : F ->* X := pfib fs.1 o* fs.2.
imports: Basics Types SuccessorStructure WildCat Pointed Modalities.Identity Modalities.Descent Truncations HFiber ObjectClassifier