(n : trunc_index) : Modality. Proof. srapply (Build_Modality (fun A => IsTrunc n A)); cbn. - intros A B ? f ?; rapply (istrunc_isequiv_istrunc A f). - exact (Trunc n). - intros; apply istrunc_truncation. - intros A; apply tr. - intros A B ? f oa; cbn in *. exact (Trunc_ind B f oa). - intros; reflexivity. - exact (@istrunc_paths' n). Defined.
Require Import Basics Types WildCat.Core WildCat.Universe HFiber. Require Import Modalities.Modality.