proposition: Lemma isexact_preimage (O : Modality) {F X Y : pType} (i : F ->* X) (f : X ->* Y) `{IsExact O _ _ _ i f} (x : X) (p : f x = point Y) : O (hfiber i x).
proof: Proof. rapply (O_functor O (A:=hfiber (cxfib cx_isexact) (x; p))). - intros [z q]. exact (z; ap pr1 q). - apply center, conn_map_isexact. Defined.
imports: Basics Types SuccessorStructure WildCat Pointed Modalities.Identity Modalities.Descent Truncations HFiber ObjectClassifier