Outline for Type Theory

80-518/818

Spring 2025

(14 weeks)

Introduction (week 1)

• Logic, Type Theory, and Category Theory
• Curry-Howard, proof relevance, categorification
• Soundness, completeness, and representation theorems

1. Simply Typed Lambda-Calculus (weeks 2-5)

• Lambda theories and their models in CCCs
• Classifying category, functorial semantics
• Completeness in CCCs
• Poset and Kripke semantics
• Topics:
  • Topological models, spaces and local homeomorphisms.
  • H-Sets, Sheaves, Realizability
  • Domain-theoretic models
  • The untyped lambda-calculus
  • Monoidal closed categories and linear type theory

2. Dependent Type Theory (weeks 6-9)

• Dependent types, Sigma, Pi, and Equality types
  • The slice lemma
• Locally cartesian closed categories
  • H-sets
  • Presheaves
  • Local homeomorphisms
• Completeness in LCCCs
  • Kripke semantics
  • Topological semantics
  • Kripke-Joyal forcing
• W-types
  • Polynomial endofunctors
  • Initial algebras
• Coherence:
  • CwFs, natural models
  • Universes and the Beck-Chevalley
• Topics:
  • Equilogical spaces
  • Final coalgebras and coinduction
  • Impredicativity, realizability models
  • CwA's, comprehension categories
  • Setoids and quotient types

3. Homotopy Type Theory (weeks 10-13)

• Identity types
• Fibrations
• H-S universes
• Univalence
• The H-levels: Prop, Set, Gpd, ...
• Topics:
  • The groupoid model
  • Algebraic weak factorization systems
  • Homotopy-initial algebras
  • Synthetic homotopy theory: pi_1(S^1)

Student Presentations (week 14)

• 2 talks / class meeting = 4 presentations