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 lambda calculus

à la Martin-Löf

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

Types

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

Type constructors

• -type (Function type)
• -type (Product type)
• Coproduct type
• Identity type
  • Extensional identity 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

• Dependent types as fibrations

Bibliography

• @angiuliPrinciplesDependentType2025

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