`{O : ReflectiveSubuniverse} {X Y : pType} (f : X ->* Y) `{IsEquiv _ _ f} : O_pcover O X pt <~>* O_pcover O Y pt := Build_pEquiv _ _ (pfunctor_O_pcover f) _.
Require Import Basics Types HFiber Truncations.Core Truncations.SeparatedTrunc Pointed