I have heard the simply typed lambda calculus is the internal language of closed Cartesian categories.
I have a written a compiler from the STLC to CCCs but this involves a lot of ugly tuple shuffling.
Is it possible to get the STLC for free from the definition of a closed Cartesian category?