Showing changes from revision #0 to #1:
Added | ~~Removed~~ | ~~Chan~~ged

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.