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: type

1. Π-type
2. Σ type
3. Coproduct type
4. Empty type
5. Unit type
6. Intensional identity type

---

develop | en | SemBr