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.