(I meant to send this to "categories" last week - by mistake it only went to Mamuka. Sorry if it's now out of context.) Mamuka Jibladze added to my comments on finite presentability,
one might also ask - which filteredness do we mean? In other words, in the condition `all finite diagrams can be coned', there might be several inequivalent finiteness notions to consider.
Indeed so. That's why I cited Section 6.6 ("Finiteness") of my book - I should have been more explcit about that. Not, of course, that I mean that to be an exhaustive account of the various notions of finiteness. There was a stress on "intuitionistic" in Michael Abbott's original email, which has perhaps got lost in the ensuing discussion. I remember getting very worried about being careful about this, and for example my unpublished paper "The Synthetic Plotkin Powerdomain" with Wesley Phoa was more complicated than it needed to be because I didn't at the time have his confidence in discussing finiteness intuitionistically (= in an elementary topos). However, what I found in writing "Practical Foundations" (with regard to many things but especially) about finiteness is that the traditional ("classical") idioms of mathematical argument are perfectly valid, once one understands the way in which they are idioms for using the rules of natural deduction. The rules for the existential quantifier apparently look very different from the vernacular use of the phrase "there exists" (in which one goes on to make use of the witness), but the correspondence is very clear and natural when you think about it - see Section 1.6. Paul