ooextendable_O_inverts@{a b z i} {A : Type@{a}} {B : Type@{b}} (f : A -> B) `{O_inverts f} (Z : Type@{z}) `{In@{i} O Z} : ooExtendableAlong@{a b z i} f (fun _ => Z). Proof. refine (cancelL_ooextendable@{a b i z i i i i i} _ _ (to O B) _ _). 1:exact (extendable_to_O'@{i b z} O B). refine (ooextendable_homotopic _ (O_functor f o to O A) _ _). 1:apply to_O_natural. refine (ooextendable_compose _ (to O A) (O_functor f) _ _). - srapply ooextendable_equiv. - exact (extendable_to_O'@{i a z} O 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.