isconnected_O_leq'@{a i1 i2} (O1 : ReflectiveSubuniverse@{i1}) (O2 : ReflectiveSubuniverse@{i2}) `{IsAccRSU@{a i1} O1} `{O_leq@{i1 i2 i2} O1 O2} (A : Type@{i2}) `{IsConnected O2 A} : IsConnected O1 A. Proof. srefine (isconnected_O_leq O1 (lift_accrsu@{a i1 i1} O1) A). 1-2:exact _. change (Contr@{i1} (Localize@{a i2} (acc_lgen@{a i1} O1) A)). refine (contr_equiv'@{i2 i1} _ 1%equiv). change (IsConnected@{i2} (lift_accrsu@{a i1 i2} O1) A). srapply (isconnected_O_leq _ O2). rapply O_leq_lift_accrsu. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.