Let $A$ be a set and let $P(x)$ be a dependent type over $A$, which is a mere proposition. The latter means that for a fixed $a:A$, the type $P(a)$ is either empty or has a unique term. Viewed as fibration, the fibre $P(a)$ over $a$ has a “thickness” of zero or one. Like a characteristic function, this specifies a subset of $A$.

Note that per definition, if $\star_a$ denotes the unique term of the fibre $P(a)$, then $\langle a,\star_a\rangle:\Sigma_{x:A}P(x)$, and all terms of the sum type are of this form. To bridge to standard set theoretical notion, we can make the following identifications

• $\{x\,|\,P(x)\}\equiv \Sigma_{x:A}P(x)$

• $a\in\{x\,|\,P(x)\}\equiv P(a)$

• $\{x\,|\,Q(x)\}\subseteq\{x\,|\,P(x)\}\equiv {\large\Pi}_{x:A}\left(Q(x)\to P(x)\right)$

The first identification corresponds to the axiom schema of replacement (or similar axioms like collection and specification). The second notion is different from most set theories written down in a predicate logic in that the subset doesn't contain $a$ itself but a tagged version $\langle a,\star_a\rangle$ of it. With regard to the third notion it must be emphasizes that here sets don't contain sets that conain sets, etc., as e.g. in ZFC.

One can go further and work out a notion of power set $\mathcal{P}(A)$ with type constructor along the lines of “${\large\frac{x\,:\,A\,\vdash\,P(x)\,:\,\mathrm{Prop}}{\{x\,|\,P(x)\}\,:\,\mathcal{P}(A)}}$”.

Set . HoTT, Mere proposition