I'm not only learning things from Wikipedia. I use other sources, many of which are easier to understand than Wikipedia, but I link to Wikipedia because it seems to be the most "canonical" source out of everything I find.
Rubber duck debugging style, I think that writing things here made me understand the Lambek part of the correspondence.
Okay, according to Curry–Howard correspondence - Wikipedia, the morphisms in the category are the identity function, the composition operator, the product constructor, a currying function, and a function application (evaluation) function, and the unit type is the terminal object.
I think I was already aware of this relationship before. Haskellers talk about a pseudo-category "Hask" (which does not satisfy the laws in the presence of _|_). The objects are the Haskell types and the morphisms are the Haskell functions. In this case, how types and terms are like the objects and morphisms is obvious.
However, I'm not completely sure if I got this right. After all, Hask has sums and an initial object (AKA identity of the sum operation), and the Cartesian closed category definition does not mention sums.
I also still think that I'm mixing up two different things by relating A ^ B in the Cartesian closed category and B -> A as in the "type" of a morphism, as the "types" of morphisms of functions are written in the latter manner for all categories (even ones that aren't Cartesian closed), so they are probably different?
I found relation between type theory and category theory in nLab, which seems to confirm that the relationship between types and functions and objects and morphisms that I describe is the Lambek part of the correspondence. However, I also see something about an "internal language," which I don't understand. (Maybe I need real CT background knowledge for this. After all, I understand the relationship between programs and proofs because I've learned implication, conjunction, disjunction, etc.)