一句话：用模态类型论分解 Löb 归纳，提出捕获 topos of trees 模态结构且不排除 canonicity/normalization 的 guarded 类型论 Gatsby。
本文重新分析 guarded recursion 中的基本 Löb 归纳原理。既有方法通常将 Löb 归纳作为核心原语，本文则借助模态类型论与 univalent foundations 的近期进展，从一组更简单、概念上更清晰的原语推导出它。基于这一洞察，作者提出 Gatsby：首个在捕获 topos of trees 丰富模态结构的同时支持 Löb 归纳，且不直接排除 canonicity 或 normalization 的 guarded 类型论。作者表明 Gatsby 能恢复许多既有 guarded recursion 方法，并利用其额外表达力改进先前例子。该工作关键依赖同伦论洞察，也是 univalent foundations 在程序语言理论中的新应用。
We present a novel analysis of the fundamental Löb induction principle from guarded recursion. Taking advantage of recent work in modal type theory and univalent foundations, we derive Löb induction from a simpler and more conceptual set of primitives. We then capitalize on these insights to present Gatsby, the first guarded type theory capturing the rich modal structure of the topos of trees alongside Löb induction without immediately precluding canonicity or normalization. We show that Gatsby can recover many prior approaches to guarded recursion and use its additional power to improve on prior examples. We crucially rely on homotopical insights and Gatsby constitutes a new application of univalent foundations to the theory of programming languages.