No. Homotopy Type Theory is a total language, so even type-level programming simply has to terminate, or the proof-checker won't accept it.

Proving that nontrivially recursive programs terminate can be a bugger.