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 vari

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.