Type theory MOC

ETT

Per Martin-Löf's Extensional Type Theory or ETT 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. Extensional identity type
  7. Universes à la Tarski

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