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
• Σ type
• Coproduct type
• 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
• let declaration

Concepts

• Dependent types as fibrations

Bibliography

• @angiuliPrinciplesDependentType2025

---

develop | en | SemBr