This is a follow-up question from my previous question titled Constructing coproduct types and boolean types from universes, where I showed how every basic operation in set theory/topos theory could be constructed from dependent product types, dependent sum types, identity types, an empty type, and a universe $U$ which is closed under the above types, although the types constructed are usually $U$-large.

Now, the HoTT book describes set-truncations in a number of ways. In section 6.9, set-truncations of a type $A$ are first defined as the higher inductive type generated by a function $\vert - \vert_0:A \to \vert A \vert_0$, and for every element $x:A$ and $y:A$ and every path $p:x = y$ and $q:x = y$, a path $\mathrm{trunc}(x, y, p, q):p = q$. Later in the section, set-truncations are defined as a higher inductive type generated by a dependent function

$$\prod_{f:S^1 \to A} \mathrm{ap}_f(p) = \mathrm{ap}_f(q)$$

where $(S^1, 0, 1, p, q)$ is the higher inductive circle type generated by the points $0:S^1$ and $1:S^1$ and the paths $p:0 = 1$ and $q:0 = 1$. Either way, the set-truncation is constructed as a higher inductive type.

Now, is there a way to directly construct the set-truncation of a type from universes, without the use of higher inductive types? No requirements are made of the size of the resulting set-truncation, they could be $U$-large if necessary.