80-514/814
Spring 2024
(14 weeks)
Introduction
- Logic and CT
- Curry-Howard and categorification
- Duality: Lawvere and Stone
Review of Category Theory (week 1)
- categories, functors, natural transformations
- representables, presheaves, Yoneda's lemma
- limits and colimits
- adjoints and monads
Algebraic Theories (weeks 2-3)
- Equational theories and varieties of algebras
- Classifying category and universal model
- The representation theorem
- Lawvere duality
- Summary of functorial semantics for algebraic theories
- Completeness
- Topics:
- Proof of duality in Lawvere, Adamek, Rosicky
- Examples: commutative rings, distributive lattices, semilattices
- Gabriel-Ulmer duality
Propositional Logic (weeks 4-5)
- Sketch of classical propositional logic:
syntax, deduction, valuations, soundness and completeness
- Boolean algebra, completeness of alegbraic logic
- Stone's representation theorem
- Stone duality
- Summary of functorial semantics for propositional logic
- Kripke semantics is presheaves on a poset
- Sub(1) in presheaves is a Heyting algebra
- Yoneda preserves products and exponentials
- Completeness theorem for propositional logics
- Topics:
- Duality for dLat and Pos
- Frames, locales, spaces
- S4 modal logic and topological models
- Bi-Heyting logic and presheaf models
First-Order Logic (week 6-7)
- Hyperdoctrines
- Adding the quantifiers: syntax, deduction
- Lex/Regular/Heyting categories
- Summary of functorial semantics for first-order logic
- Topics:
- Kripke semantics
- Completeness for intuitionistic first-order logic
The Lambda-Calculus (weeks 8-9)
- Curry-Howard: proof theory of IPC gives the lambda-calculus
- Lambda theories and their models in CCCs
- Classifying category, functorial semantics
- Kripke models: on a poset, on a CCC
- Completeness: Yoneda preserves exponentials, completeness in presheaves
- Topics:
- Topological models, spaces and local homeomorphisms.
- H-Sets, Sheaves, ...
- Domain-theoretic model of the untyped lambda-calculus
- Monoidal closed categories and a type theory for linear logic
Type Theory (weeks 10-12)
- Dependent types, Sigma, Pi, and Equality types, examples
- Locally cartesian closed categories
- Presheaves
- Local homeomorphisms
- H-sets
- Topics:
- Equilogical spaces
- Completeness in LCCCs, Kripke, Topological
- Coherence, Natural models
- W-types: Endofunctors, initial algebras, final coalgebras
- Coinduction
- Identity types
- Universes: Prop, Set, Type, ...
- Impredicativity, realizability models
- Homotopy type theory
Student Presentations (weeks 13-14)
- 2/class meeting = 8 presentations