fact: Definition issig_isexact (n : Modality) {F X Y : pType} (i : F ->* X) (f : X ->* Y) : _ <~> IsExact n i f := ltac:(issig).
imports: Basics Types SuccessorStructure WildCat Pointed Modalities.Identity Modalities.Descent Truncations HFiber ObjectClassifier