> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/350-type-theory/itt.md).

# Intuitionistic type theory

* Intuitionistic type theory (ITT)
* Constructive type theory (CTT)
* Martin-Löf type theory (MLTT)
  * MLTT71
  * MLTT72
  * MLTT73
  * MLTT79
* intuitionistic intensional type theory
* intuitionistic extensional type theory
* intuitionistic predicative type theory
* intuitionistic impredicative type theory
* constructive logic
* Girard's paradox
* dependent types
* inductive types
* unbounded data structures
* judgement, entailment (turnstile), antecedents (context), conclusion

ITT types

* Base types
  * 0 type, `⟘`, bottom, the empty type
  * 1 type, `()`, the unit type
  * 2 type
* Type ctors
  * `Σ`-types: dependent ordered pairs, existential quantification
  * `Π`-types: dependent functions, universal quantification
  * `=`-types: reflection
  * inductive types
  * universe types
    * predicative hierarchy of universes:
      * `𝒰₀, 𝒰₁, 𝒰₂, …`
      * `𝒰₀ : 𝒰₁`, `𝒰₁ : 𝒰₂`, …
    * predicative universes
    * impredicative universes
    * super universes
    * Mahlo universes