fact: Definition classify_fiberseq `{Univalence} {Y F : pType@{u}} : (Y ->* [Type@{u}, F]) <~> { X : pType@{u} & FiberSeq F X Y }.
imports: Basics Types SuccessorStructure WildCat Pointed Modalities.Identity Modalities.Descent Truncations HFiber ObjectClassifier