{n m : trunc_index} (Hmn : m <= n) : O_leq (Tr m) (Tr n). Proof. intros A; rapply istrunc_leq. Defined.
Require Import Basics Types WildCat.Core WildCat.Universe HFiber. Require Import Modalities.Modality.