Homotopy type theory is a type theory (of the Martin-Löf variety) that combines higher inductive types and has deep connections with the univalence axiom. That

Homotopy type theory is a type theory (of the Martin-Löf variety) that combines higher inductive types and has deep connections with the univalence axiom. That's probably the main reason. Then there's also cubical type theory, which some would claim gives computational meaning to HTT.