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

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

---

develop | en | SemBr