This is a stub collecting information on the question in the title. Setzer computes the strength of MLTT+W. Voevodsky reduces Coq’s inductive types to W-types. Coquand et al reduces univalence and some HITs to an unspecified constructive framework.

There is an MO-question on the proof theoretic strength of pCIC. Avigad provide a general overview of the proof theory of predicative constructive systems.

The strength of type theories

This section collects some references that establish the strength various type theories, roughly in increasing order of strength.

Let $\mathrm{ML}_n$ denote MLTT without inductive types and $n$ universes closed under $\Pi$ and $\Sigma$. This has the strength of the first-order system of $n$ iterated fixed points (whether with intuitionistic or classical logic), and thus by Feferman 1982 has proof-theoretic ordinal $\xi_n$, where $\xi_0=\varepsilon_0$ and $\xi_{n+1} = \varphi(\xi_n,0)$.