[mafribe]

It depends on what you mean by "embedding". If one does a deep embedding then powerful calculi can be embedded in much weaker calculi. E.g. Isabelle uses a variant to LF as meta-language to embed all manner of more powerful logics. That doesn't mean LF has a lot of expressive power.

Coq's logic isn't quite the CoC anymore: impredictivity is switched off by default, Coq has universes etc.

With this in mind, I'm not sure what Voevodsky means when he says HoTT and CoC are the same thing.