{A B} (f : A -> B) (b : B) : O (hfiber f b) -> hfiber (O_functor f) (to O B b). Proof. apply O_rec. intros [a p]. exists (to O A a). refine (to_O_natural f a @ _). apply ap, p. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.