(Z:Type@{k}) (E : forall (A : Type@{i}) (B : Type@{j}) (f : A -> B) (Oif : O_inverts f), ooExtendableAlong f (fun _ => Z)) : In O Z. Proof. pose (EZ := fst (E Z (O Z) (to O Z) _ 1%nat) idmap). exact (inO_to_O_retract _ EZ.1 EZ.2). 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.