For completeness I'm adding the specific example that the OP is asking for, turning my comment above and Jason Rute's into an answer.
One thing that make type theories occurring in most PAs strictly logically (consistency-wise) stronger is the availability of universes. I would think that one universe is enough to build a model of HOL (and thus showing that is stronger by Gödels 2nd incompleteness theorem). By the same token, “There exists a model of HOL” can't be proved in HOL. On the other hand, Isabelle/HOL includes a theory (
ZFC_in_HOL) that builds a set theoretic universe, so you recover some strength.
That said, the great majority of results in math do not need logical strength greater than few orders on top arithmetic: For instance, McLarty showed that Fermat's Last Theorem can be formalized in something like third order arithmetic (while every HOL system provides you with all the finite orders).
Nevertheless, these comments are independent of the fact that implementing some stuff in DTT might be more direct than in HOL. This is the point usually made by K. Buzzard.
EDIT: Some references that were kindly provided by user9716869: the document The HOL System Logic provides HOL semantics (effectively in $V(\omega+\omega)$ without the empty set). Sets in Types, Types in Sets shows that ZFC with n inaccessibles can be encoded in CiC with a variant of the Axiom of Choice and $n+1$ universes.
ZFC_in_HOL) that builds a set theoretic universe, so you recover some strength. Nevertheless, these comments are independent of the fact that implementing some stuff in DTT might be more direct than in HOL. $\endgroup$