{A B : Type} (f g : A -> B) (pi : f == g) : O_functor f == O_functor g. Proof. refine (O_indpaths _ _ _); intros x. refine (to_O_natural f x @ _). refine (_ @ (to_O_natural g x)^). apply ap, pi. 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.