Add to ORKGAbstract. We describe a sequent calculus µLJ with primitives for inductive and co-inductive datatypes and equip it with reduction rules allowing a sound translation of Gödel’s system T. We introduce the notion of a µ-closed category, relying on a uniform interpretation of open µLJ formulas as strong functors. We show that any µ-closed cat-egory is a sound model for µLJ. We then turn to the construction of a concrete µ-closed category based on Hyland-Ong game semantics. The model relies on three main ingredients: the construction of a general class of strong functors called open functors acting on the category of games and strategies, the solution of recursive arena equations by ex-ploiting cycles in arenas, and the adaptation of the winnin...