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