n m X : Tr n (Tr m X) <~> Tr m (Tr n X). Proof. refine (Trunc_min m n _ oE equiv_transport (fun k => Tr k _) _ oE (Trunc_min n m _)^-1). apply trunc_index_min_swap. Defined.
Require Import Basics Types WildCat.Core WildCat.Universe HFiber. Require Import Modalities.Modality.