{F X Y : pType} {i : F ->* X} {f : X ->* Y} (cx : IsComplex i f) : F ->* pfiber f. Proof. srapply Build_pMap. - exact (fun x => (i x; cx x)). - cbn. refine (path_sigma' _ (point_eq i) _); cbn. refine (transport_paths_Fl _ _ @ _). apply moveR_Vp. exact ((concat_p1 _)^ @ point_htpy cx). Defined.
Require Import Basics Types. Require Import SuccessorStructure. Require Import WildCat. Require Import Pointed. Require Import Modalities.Identity Modalities.Descent. Require Import Truncations. Require Import HFiber. Require Import ObjectClassifier.