`(O : ReflectiveSubuniverse) {X Y : pType} (f : X ->* Y) `{IsEquiv _ _ f} : [O X, _] <~>* [O Y, _] := Build_pEquiv _ _ (O_pfunctor O f) _.
Require Import Basics Types ReflectiveSubuniverse Pointed.Core.