proposition: Proposition equiv_cxfib_beta {F X Y : pType} {i : F ->* X} {f : X ->* Y} `{forall y y' : Y, In O (y = y')} `{MapIn O _ _ i} (ex : IsExact O i f) : i o pequiv_inverse (equiv_cxfib ex) == pfib _.
proof: Proof. rapply equiv_ind. 1: exact (isequiv_cxfib ex). intro x. exact (ap (fun g => i g) (eissect _ x)). Defined.
imports: Basics Types SuccessorStructure WildCat Pointed Modalities.Identity Modalities.Descent Truncations HFiber ObjectClassifier