The game semantics of free cartesian closed categories: a syntactic derivation

It is well known that cartesian closed categories (CCCs) model typed lambda calculus with products. We explore how the game semantics of free CCCs can be derived from the syntax of a typed lambda calculus with products and invertible constants. The categorical model for this is a free CCC, 𝓕_G, generated by an object equipped with a free group, G, of automorphisms. This appears to be a novel approach that has the benefit of simplicity while also being generalisable. Along the way we give an algorithm for computing long βη-normal forms together with a proof of correctness. All of this is facilitated by a natural automorphism Φ on the inclusion functor 𝓕 → 𝓕_G, where 𝓕 is the free CCC generated by an object. A solution to the problem of totality of composition of strategies [1] is hinted at using our machinery. We also claim conjecturally that it is possible to generalise long βη-normal forms to free almost bi-cartesian closed categories [16] using these ideas.