issmall_inhabited_issmall@{i j k | i < k, j <= k} `{PropResizing} `{Univalence} (X : Type@{j}) (isX : X -> IsSmall@{i j} X) : IsSmall@{i j} X. Proof. rapply (issmall_issmall_codomain_fibers@{i k} isX). intro sX. rapply sigma_closed_issmall. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.Trunc Basics.Tactics