# Constructing set-truncations of types from universes

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.

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.