{n : trunc_index} {A B : Type} (f : A -> B) `{MapIn (Tr n) _ _ f} : IsTruncMap n f. Proof. assumption. Defined.
Require Import Basics Types WildCat.Core WildCat.Universe HFiber. Require Import Modalities.Modality.