Constructing set-truncations of types from universes

Question

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.

Answer 1

Given a universe $U$, the type of $U$-small propositions is given by $$\mathrm{Prop} \equiv \sum_{P:U} \prod_{x:P} \prod_{y:P} x = y$$ Given a type $A:U$, for $x:A$ and $y:A$, the type $$[x = y] \equiv \prod_{P:\mathrm{Prop}} ((x = y) \to P) \to P$$ is the propositional truncation of the identity type $x = y$, and is always an equivalence relation on $A$. The set-truncation of $A$ is the quotient set $$[A]_0 \equiv \sum_{P:A \to \mathrm{Prop}} \exists x:A.\forall y:A.[x = y] \iff P(x)$$

In general, this type is $U$-large unless one has an axiom like propositional resizing or replacement.