Mathematics MOC

Type theory MOC

Type theory is the study of type theories and their semantics. The differences between type theory and set theory are subtle; see Type theory vs set theory.

Axiomatic type theories

Calculus of substitutions

à la Church

• Lambda cube
  • Simply typed λ-calculus

à la Martin-Löf

• ETT
• ITT
• Homotopy type theory
  • Axiomatic HoTT
  • Cubical TT

Connectives

• Empty type
• Unit type
• Natural numbers type
• Type of booleans

Type constructors

graph TD;
    sigma["Σ[a : A] B(a)"]
    pi["Π[a : A] B(a)"]
    dorp["A ∐ B"]
    prod["A × B"]
    fun["A → B"]
    sigma-->|"A = 𝟚"|dorp
    sigma-->|"B(x) = B"|prod
    pi-->|"A = 𝟚"|prod
    pi-->|"B(x) = B"|fun

• 𝚷-type (Function type)
• Σ-type (Product type)
• Coproduct type
• Identity type
  • Extensional equality type

Special kinds of types

• Inductive type
  • W-type
• Coïnductive type
• Higher inductive type

Elements of syntax

• Context in a proof system
• Judgemental equality

Concepts

• Internalizing judgemental structure

Computation

• 𝛽-computation
• 𝜂-unicity

Bibliography

• PoDTT

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