(A : Type) : O_functor (to O A) == to O (O A). Proof. refine (O_indpaths _ _ _); intros x. apply to_O_natural. 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.