`{Funext} {A B : Type} (f : A -> B) (e : forall (Z:Type), In O Z -> IsEquiv (fun g:B->Z => g o f)) : O_inverts f. Proof. apply O_inverts_from_extendable. intros Z ?. rapply ((equiv_extendable_isequiv 0 _ _)^-1%equiv). 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.