Change definition of Cartesian to include a terminal object.

[TOTBWF]

Currently, our definition of cartesian only requires binary products, which is somewhat non-standard. We should probably create a new module Cat.Cartesian that exposes this new definition, along with some helpers (agda-categories would be good to look at here).

This will also require some careful proofreading to ensure that we update any prose in other modules.