lift_accrsu@{a i j} (O : Subuniverse@{i}) `{IsAccRSU@{a i} O} : ReflectiveSubuniverse@{j} := Loc@{a j} (acc_lgen O). Global Instance O_eq_lift_accrsu@{a i j k} (O : Subuniverse@{i}) `{IsAccRSU@{a i} O} : O_eq@{i j k} O (lift_accrsu@{a i j} O). Proof. split; intros A A_inO. - intros i. assert (e := fst (inO_iff_islocal O A) A_inO i). apply (lift_ooextendablealong@{a a a a a a i j k i j} (acc_lgen O i) (fun _ => A)). exact e. - apply (inO_iff_islocal O). intros i. pose (e := A_inO i). apply (lift_ooextendablealong@{a a a a a a j i k j i} (acc_lgen O i) (fun _ => A)). exact e. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.