(Z:Type) (Yo : forall (A : Type) (B : Type) (f : A -> B) (Oif : O_inverts f), IsEquiv (fun g:B->Z => g o f)) : In O Z. Proof. pose (EZ := extension_isequiv_precompose (to O Z) _ (Yo Z (O Z) (to O Z) _) 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.