We present a novel analysis of the fundamental L{"o}b induction principle from guarded recursion. Taking advantage of recent work in modal type theory and univalent foundations, we derive L{"o}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{"o}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.

I am interested in type theory as it relates to mathematics and computer science.