proposition: Lemma isexact_preimage_hfiber (O : Modality) {F X Y : pType} (i : F ->* X) (f : X ->* Y) `{IsExact O _ _ _ i f} (x : hfiber f pt) : O (hfiber i x.1).
proof: Proof. srapply isexact_preimage; exact x.2. Defined.
imports: Basics Types SuccessorStructure WildCat Pointed Modalities.Identity Modalities.Descent Truncations HFiber ObjectClassifier