Type theory MOC

ITT

Per Martin-Löf's Intensional Type Theory or ITT can be presented as the cartesian calculus of substitutions extended by the following: #m/def/type

  1. -type
  2. -type
  3. Coproduct type
  4. Empty type
  5. Unit type
  6. Intensional identity type
  7. Universes à la Tarski

#state/develop | #lang/en | #SemBr