Trunc_functor@{i j k | i <= k, j <= k} {X : Type@{i}} {Y : Type@{j}} (f : X -> Y) : Tr@{i} n X -> Tr@{j} n Y := O_functor@{k k k} (Tr n) f.
Require Import Basics Types WildCat.Core WildCat.Universe HFiber. Require Import Modalities.Modality.