functor_Trm@{i j i' j' | i' <= j, j' < j} `{Funext} {A : Type@{i}} {A' : Type@{i'}} (f : A -> A') : Trm@{i j} A -> Trm@{i' j'} A' := Trm_rec (trm o f).
Require Import HoTT.Basics. Require Import Universes.Smallness.