Pierce's Basic Category Theory for Computer Scientists writes:
1.10.2 Definition A Cartesian Closed Category (CCC) is a category with a terminal object, binary products and exponentiation.
I recall that a Cartesian Closed Category has something to do with higher order logic. What is the terminal object there?