{A : Type@{i}} {B : Type@{j}} (f : A -> B) (e : forall (Z:Type@{k}), In O Z -> ExtendableAlong@{i j k l} 2 f (fun _ => Z)) : O_inverts f. Proof. srapply isequiv_adjointify. - exact (O_rec (fst (e (O A) _) (to O A)).1). - srapply O_indpaths. intros b. rewrite O_rec_beta. assert (e1 := fun h k => fst (snd (e (O B) _) h k)). cbn in e1. refine ((e1 (fun y => O_functor f ((fst (e (O A) _) (to O A)).1 y)) (to O B) _).1 b). intros a. rewrite ((fst (e (O A) (O_inO A)) (to O A)).2 a). apply to_O_natural. - srapply O_indpaths. intros a. rewrite to_O_natural, O_rec_beta. exact ((fst (e (O A) (O_inO A)) (to O A)).2 a). 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.