Type checking (decidability)

Layer 0 — Mathematicsin the Type Theory subtree

STLC + System F + MLTT + CoC all admit decidable type-checking (modulo definitional-equality); Lean's elaborator uses bidirectional algorithm; fundamental to proof-assistant practice.