The blog post was written in the context of HoTT having just come out and some people were assuming it was a form of hard constructivism (see the mailing list discussions linked to in the blog post), so I tried to explain that:

HoTT is agnostic with respect to excluded middle and the axiom of choice. One can assume these principles if so desired, and thereby incorporate set-level classical mathematics.

In HoTT the usual conception of set appears naturally as one level of a richer hierarchy of types. In this sense HoTT is a generalization of set theory. Moreover, the hierarchy is quite relevant to mathematical practice and has significant explanatory power.

Regarding the second point, note that it is not at all unusual to have sets appear in a larger universe. For example, every Grothendieck topos contains sets as a full subcategory, as well as any realizability topos.

The two foundations, ZFC and HoTT, paint different pictures of how mathematics *can* be organized, they serve different purposes, and they are used diffrently (see Penelope Maddy's What Do We Want a Foundation to Do?).

To demonstrate the difference, let us consider the circle. There are several mathematical manifestations of the idea:

The circle as a raw set $C$ of all points in a plane at unit distance from the origin.

The circle as a topological space $(C, \tau)$, with the standard topology $\tau$.

The circle $(\{z \in \mathbb{C} \mid |z| = 1\}, 1, {}^{-1}, {\times})$ as the multiplicative subgroup of non-zero complex numbers.

The above manifestations are constructed in ZFC from sets as *structure*, as indicated above.

In HoTT we can *also* define all the manifestations in the exact way, as structures. But *in addition*, there is a fourth manifestation of the circle: the *homotopical* circle $S^1$ that is built as a higher-inductive type. This type is *not* the result of any set-theoretic construction *carried out in HoTT*.

One can of course build a *model* of HoTT in ZFC and observe that the homotopical circle $S^1$ is an object in this model, namely a certain Kan simplicial set, therefore it is the result of a set-theoretic construction *carried out in ZFC*.

I would hope that the above remarks are completely obvious. And let me be explicit: I do *not* think that one foundation is "better" than the other.

Now, let me finally address OP's questions.

The way I understand the first questions is this: what are the higher types appearing in HoTT good for if they already can be constructed from sets? I hope the above discussion clears this up. So long as we work inside HoTT, there are going to be types that are not sets, not can they be constructed from sets. The homotopical circle is an example.

The second question asks about structures that exist in HoTT but not in ZFC. Again, we can use the homotopical circle $S^1$ as an example. This is a pointed type, with a base point $b : S^1$, such that the monoid of *all* maps $S^1 \to S^1$ that fix $b$ is isomorphic to the additive group $\mathbb{Z}$ (in HoTT paralance we would say that the loop space of $S^1$ is equivalent to $\mathbb{Z}$). No set has this property, for cardinality reasons.

And let me reiterate: *of course* one can build groupoids in ZFC and observe that there is a pointed groupoid whose loop space is equivalent to $\mathbb{Z}$. However, this does not falsify the claim that in HoTT $S^1$ exhibits a phenomenon that no set can.