functor_imp_Trm@{i i' | Set < i, Set < i'} `{Funext} {A : Type@{i}} {A' : Type@{i'}} (f : A -> A') : imp_Trm@{i} A -> imp_Trm@{i'} A' := imp_Trm_rec (trm o f).
Require Import HoTT.Basics. Require Import Universes.Smallness.