It is my understanding that HITs are just as easy to integrate into non-homotopy type theories as they are to HoTTs.