Modality. Proof. srapply (Build_Modality (fun _ => Unit) _ _ idmap). 1-2,6:intros; exact tt. - intros; assumption. - intros ? ? ? f z; exact (f z). - intros; reflexivity. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Modality Accessible.