n m X : Tr (trunc_index_min n m) X <~> Tr n (Tr m X). Proof. destruct (trunc_index_min_path n m) as [p|q]. + assert (l := trunc_index_min_leq_right n m). destruct p^; clear p. snrapply (Build_Equiv _ _ (Trunc_functor _ tr)). nrapply O_inverts_conn_map. rapply (conn_map_O_leq _ (Tr m)). rapply O_leq_Tr_leq. + assert (l := trunc_index_min_leq_left n m). destruct q^; clear q. srapply equiv_tr. srapply istrunc_leq. Defined.
Require Import Basics Types WildCat.Core WildCat.Universe HFiber. Require Import Modalities.Modality.