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. ### See also ### '[[nlab:type theory|Type theory]]' on the nLab wiki.