`{n : trunc_index} {X Y : pType} (f : X ->* Y) : O_pcover (Tr n) X pt ->* O_pcover (Tr n) Y pt := functor_pfiber (ptr_natural n f).
Require Import Basics Types HFiber Truncations.Core Truncations.SeparatedTrunc Pointed