A type theory is a formal system in which every term has a ‘type’, and operations in the system are restricted to acting on specific types.
A number of type theories have been used or proposed for doing homotopy type theory.
‘Type theory’ on the nLab wiki.