O_inverts_O_leq@{i1 i2} (O1 : ReflectiveSubuniverse@{i1}) (O2 : ReflectiveSubuniverse@{i2}) `{O_leq@{i1 i2 i1} O1 O2} {A B : Type@{i1}} (f : A -> B) `{O_inverts O2 f} : O_inverts O1 f. Proof. apply O_inverts_from_extendable@{i1 i1 i1 i1 i1}; intros Z Z_inO. pose (inO_leq O1 O2 Z _). apply (lift_extendablealong@{i1 i1 i1 i1 i1 i1 i2 i1 i1 i2 i1}). apply (ooextendable_O_inverts O2); exact _. 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.