O_inverts_O_leq'@{a i1 i2} (O1 : ReflectiveSubuniverse@{i1}) (O2 : ReflectiveSubuniverse@{i2}) `{IsAccRSU@{a i1} O1} `{O_leq@{i1 i2 i2} O1 O2} {A B : Type@{i2}} (f : A -> B) `{O_inverts O2 f} : O_inverts O1 f. Proof. assert (oleq := O_leq_lift_accrsu O1 O2). assert (e := O_inverts_O_leq (lift_accrsu@{a i1 i2} O1) O2 f); clear oleq. nrapply (O_inverts_O_leq O1 (lift_accrsu@{a i1 i1} O1) f). 1:exact _. refine (@isequiv_homotopic _ _ _ _ e _). apply O_indpaths; intros x; reflexivity. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.