resized_Trm_rec@{i j k u | i <= k, Set < k} {A : Type@{i}} {P : Type@{j}} `{IsHProp P} (f : A -> P) : resized_Trm@{i k u} A -> P. Proof. refine (_ o (equiv_smalltype@{u k} _)). exact (fun ma => (equiv_smalltype@{Set j} P) (ma (smalltype@{Set j} P) _ ((equiv_smalltype@{Set j} P)^-1 o f))). Defined.
Require Import HoTT.Basics. Require Import Universes.Smallness.