The two foundations, ZFC and HoTT, paint different pictures of how mathematics can be organized, and they also serve different purposes (see Penelope Maddy's What Do We Want a Foundation to Do?). With this in mind, let me 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? This is not true. For example, the HoTT circle $S^1$ is a certain higher inductive type which is not a set but a groupoid. If we construct the circle in the usual set-theoretic way (construct $\mathbb{N}$, $\mathbb{Z}$, $\mathbb{Q}$, $\mathbb{R}$, define the Euclidean metric on $\mathbb{R}^2$, define the circle as a subspace of the plane of all points at unit distance from the origin), the result will be a different manifestation of "circle" that is not equivalent to $S^1$.

The second question asks about structures that exist in HoTT but not in ZFC. Here is one: there is a type $C$ with an element $b \in C$ such that the monoid of maps $C \to C$ which fix $b$ is isomorphic to the group $\mathbb{Z}$. In ZFC there is no such set for cardinality reasons (if $C$ is finite then it is too small, and if it is infinite then it is too large). The type in question is, you guessed it, the circle $S^1$.

I anticipate an objection:

But we can build a model of HoTT in ZFC with enough inaccessible cardinals!

My reply would be that doing things in a model built in ZFC is not the same thing as doing things in ZFC. At all.

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:

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

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

3. 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.

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:

1. 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.

2. 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.

The two foundations, ZFC and HoTT, paint different pictures of how mathematics can be organized, and they also serve different purposes (see Penelope Maddy's What Do We Want a Foundation to Do?). With this in mind, let me 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? This is not true. For example, the HoTT circle $S^1$ is a certain higher inductive type which is not a set but a groupoid. If we construct the circle in the usual set-theoretic way (construct $\mathbb{N}$, $\mathbb{Z}$, $\mathbb{Q}$, $\mathbb{R}$, define the Euclidean metric on $\mathbb{R}^2$, define the circle as a subspace of the plane of all points at unit distance from the origin), the result will be a different manifestation of "circle" that is not equivalent to $S^1$.

The second question asks about structures that exist in HoTT but not in ZFC. Here is one: there is a type $C$ with an element $b \in C$ such that the monoid of maps $C \to C$ which fix $b$ is isomorphic to the group $\mathbb{Z}$. In ZFC there is no such set for cardinality reasons (if $C$ is finite then it is too small, and if it is infinite then it is too large). The type in question is, you guessed it, the circle $S^1$.

I anticipate an objection:

But we can build a model of HoTT in ZFC with enough inaccessible cardinals!

To my mind, this objection is just as valid as the the following objection to the theorem that the angles of a triangle sum up to $180^\circ$:

But the upper half-plane is a model of non-Euclidean geometry in which angles do not sum up to $180^\circ$!

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:

1. 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.

2. 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.

The two foundations, ZFC and HoTT, paint different pictures of how mathematics can be organized, and they also serve different purposes (see Penelope Maddy's What Do We Want a Foundation to Do?). With this in mind, let me 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? This is not true. For example, the HoTT circle $S^1$ is a certain higher inductive type which is not a set but a groupoid. If we construct the circle in the usual set-theoretic way (construct $\mathbb{N}$, $\mathbb{Z}$, $\mathbb{Q}$, $\mathbb{R}$, define the Euclidean metric on $\mathbb{R}^2$, define the circle as a subspace of the plane of all points at unit distance from the origin), the result will be a different manifestation of "circle" that is not equivalent to $S^1$.

The second question asks about structures that exist in HoTT but not in ZFC. Here is one: there is a type $C$ with an element $b \in C$ such that the monoid of maps $C \to C$ which fix $b$ is isomorphic to the group $\mathbb{Z}$. In ZFC there is no such set for cardinality reasons (if $C$ is finite then it is too small, and if it is infinite then it is too large). The type in question is, you guessed it, the circle $S^1$.

I anticipate an objection:

But we can build a model of HoTT in ZFC with enough inaccessible cardinals!

My reply would be that doing things in a model built in ZFC is not the same thing as doing things in ZFC. At all.