added example of a coherent category satisfying the axiom of finiteness

Anonymous

]]>added a separate definition of well-pointedness in terms of the axiom schemata of bounded separation (in addition to the terminal object being a strong generator), as defined in

- Michael Shulman (2018). Comparing material and structural set theories. arXiv:1808.05204.

Anonymous

]]>Added citations for the recently added theorem, thanks to an anonymous contributor by email.

]]>Added section “References”, at this time containing only some references to Mac Lane and Moerdijk’s SGL. Also added some remarks.

]]>Added a proof that in classical logic, well-pointedness is equivalent to the conjunction nondegenerate + Boolean + two-valued + split supports. This seems to be hard to find in the literature.

]]>Fixed the last equivalent version of well-pointedness, and added a proof that 1 is also a strong generator.

]]>Clarified last paragraph of the section “In a pretopos”

]]>I think the “it” means this bit:

we have to strengthen the condition that 1 is a generator to the condition that 1 is a strong generator,

And I think the “whenever” means that it’s not just in thinking about a predicative category of sets, but an arbitrary pretopos.

]]>The pretopos section ends in a sentence I don’t know how to interpret:

But of course it applies whenever one is studying a pretopos.

Does this really mean topos here at the end? If not, what is “it”?

]]>started a section well-pointed (oo,1)-topos as parts of the blog discussion here

In the course of that I added to the plain definition the statement that the global section functor is faithful

]]>Added an "Examples"-section to well-pointed topos and to Boolean topos mentioning Set and models for ETCS.

]]>