lift_accmodality@{a i j} (O : Subuniverse@{i}) `{IsAccModality@{a i} O} : Modality@{j} := Nul@{a j} (acc_ngen O). Global Instance O_eq_lift_accmodality (O : Subuniverse@{i}) `{IsAccModality@{a i} O} : O <=> lift_accmodality O. Proof. split; intros A; apply inO_iff_isnull. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import Modality Accessible.