functor_O_cover@{u v} `{O : ReflectiveSubuniverse} {X Y : Type@{u}} (f : X -> Y) (x : O X) : O_cover@{u} X x -> O_cover@{u} Y (O_functor O f x) := functor_hfiber (f:=to O _) (g:=to O _) (h:=f) (k:=O_functor O f) (to_O_natural O f) x.
Require Import Basics Types HFiber Truncations.Core Truncations.SeparatedTrunc Pointed