Showing changes from revision #1 to #2:
Added | Removed | Changed
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.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.