Re: categories: Re: is Set LFP?

[Paul Taylor <pt@dcs.qmw.ac.uk>]

(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