> the definition of a Cartesian closed category in most textbooks expands to something like 20 equations, but you can simplify it down to the usual few equations which specify a model of simply typed lambda calculus

Has that been written down somewhere convenient? I'd like to have a look.

By the way, I found lots of your comments on your post history also very interesting!