fact: Record LongExactSequence (k : Modality) (N : SuccStr) : Type := { les_carrier : N -> pType; les_fn : forall n, les_carrier n.+1 ->* les_carrier n; les_isexact : forall n, IsExact k (les_fn n.+1) (les_fn n) }.
imports: Basics Types SuccessorStructure WildCat Pointed Modalities.Identity Modalities.Descent Truncations HFiber ObjectClassifier