This concerns Richard Wood's remarks on regular categories: Maybe this is a superficial observation, but the terminal object in a topos and the 1 in a ccd lattice are the unit elements with respect to cartesian product x and binary meet, respectively. I seem to remember that such unit objects are responsible for difficulties when proving nice coherence theorems (maybe Richard Blute could comment on that). Also, from computer scientists I got the impression that a unit object with respect to pairing causes complications in the lambda calculus. In particular the isomorphism A \cong [I,A] causes lots of trouble with the "continuation passing style transformation" some computer scientists like to use. I wonder whether it is this aspect of the terminal objects that is responsible for the complications Richard Wood describes. -- J"urgen -- J"urgen Koslowski | If I don't see you no more in this world Department of Mathematics | I meet you in the next world Kansas State University | and don't be late! koslowj@math.ksu.edu | Jimi Hendrix (Voodoo Chile) ==============================================================================