Is it possible that the universe of types could be closed?
I'm uncertain what you're referring to exactly, but I can remark on a few things.

The first is that the usual problem with W-types is that encoding inductive types with them does not necessarily give you the right induction principles. For instance, we can try to define the natural numbers like so:

F : 2 → Type
F 0 = ⊥
F 1 = ⊤

ℕ : Type
ℕ = W 2 F

zero : ℕ
zero = sup 0 absurd

suc : ℕ → ℕ
suc n = sup 1 (const n)

induction : (P : ℕ → Type) → P zero → (∀ n. P n → P (suc n)) → ∀ n. P n
induction pz ps n = ???


The problem we'll run into is that induction on $W$ and $2$ allows us to observe the case $n = {\tt sup}\ 0\ f$, but we only have a proof of $P\ ({\tt sup}\ 0\ {\tt absurd})$. So we'll need a way to prove that $f = {\tt absurd}$, but there is no such principle in normal intensional type theory.

The answer to your question in this regard is that homotopy type theory does help in this regard, because e.g. univalence implies extensional equality of functions (and cubical type theory also includes this, for instance). So we should not have as many problems recovering the 'right' induction principles for $W$ based encodings.

However, another answer is that we didn't actually need this to begin with. This problem is somewhat particular to the specifics of $W$. Instead, we could use a more complex type of 'descriptions' of inductive definitions together with a decoding to a more 'first-order' representation of the container functor used in the $W$ definition. This approach is used in The Gentle Art of Levitation, which says it does not require extensional equality of functions (I believe).

This technique is also detailed in Ambrus Kaposi's thesis, which shows what sort of codes you need for inductive-recursive and inductive-inductive definitions.

The (I think) counter-intuitive bit about these systems is that they seem to actually be capable of describing themselves, and that this is not (it seems) contradictory.

So, it seems like we are relatively close to knowing how to to include most (commonly desired) definitions in type theory as a universe of descriptions with a 'decoding' function, instead of taking some universes to be open with respect to special definition forms. And this fact is somewhat independent of any features that homotopy type theory would have. I don't know of any system like Agda or Idris has this methodology on their roadmap, though.

I should say, there are potential traps, still. For instance, each universe Set i in Agda is called "Mahlo," because it admits inductive-recursive definitions. There are stronger universes known than Mahlo universes, too, which will in turn have (many) Mahlo universes within them. But the sort of 'universe' you define with induction-recursion cannot be Mahlo, because it is inconsistent for a Mahlo universe to have an induction principle. So any theory incorporating strong-than-Mahlo universes would at least need a different sort of 'description' system for those.