`{O : ReflectiveSubuniverse} {X Y : pType} (f : X ->* Y) : O_pcover O X pt ->* O_pcover O Y pt := functor_pfiber (pto_O_natural O f).
Require Import Basics Types HFiber Truncations.Core Truncations.SeparatedTrunc Pointed