To my knowledge, intuitionistic type theory (ITT) considers type of higher order (called higher-kinded types), so homotopy type theory (HoTT) isn't exactly relevant here - especially since it has, to my knowledge, not cross-pollinated with ML or ANN research. Models of recursion can be found in systems as simple as lambda calculi or cellular spaces, and this was the big idea behind Jeff Hawkins's HTM and other classical models (please correct me if I am wrong).
What HoTT brings to the table is the notion that a path between two types can be used to transport a proof from one type to another - currently immensely handy for theorem proving, but applications in ML and beyond remain to be made.
