A modal deconstruction of Löb induction
summary
Derives Löb induction from a small set of modal primitives and univalent foundations, building Gatsby — a guarded dependent type theory that adds one rule forcing the top modality to be unit and thereby makes many types accessible. Proves accessible types close under Pi, Sigma, equality and the universe and that later preserves accessibility, so standard guarded theories compile into Gatsby. Demonstrates by pen‑and‑paper case studies (step‑index logical relations, coinductive types) but no full implementation yet; normalization/canonicity for the full system remains future work.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 1:03Guarded recursion and later
- 2:30Intended model
- 3:54Limitations of later
- 4:36Gatsby and modalities
- 6:43Modal type theory background
- 7:24More modalities don't solve Löb
- 8:27Bomb proposition
- 9:50Proving Löb from bomb
- 11:12Accessible types
- 12:35Top modality role
- 13:41Top modality rule
- 14:45Compiling guarded type theory
- 15:26Usability and case studies
- 15:47Summary
- 16:49Gatsby meta-theory
related talks
12mA Unified View of Modalities in Type Systems
53mIntroduction to Intuitionistic Type Theory
18mThe Essence of Generalized Algebraic Data Types
20mModal Mu-Calculus for Free in Agda
52mType Theory and its Meaning Explanations
14mModal Effect Types
22mA Calculus of Inductive Linear Constructions
15mTowards a Coq Specification for Generalized Algebraic Datatypes in OCaml