{F X Y : pType} (i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f} : pequiv_pmap_idmap o* i ==* pfib f o* pequiv_cxfib. Proof. unfold Square. refine (pmap_postcompose_idmap _ @* _). symmetry; apply pfib_cxfib. 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.