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.