There are of course all sorts of different notions of finiteness in constructive mathematics, but the unadorned word “finite” is usually used to mean the strongest one.

]]>Ah, so the word finite in the result really does mean the strongest sort of finite in the absence of Choice. That’s what is was worried about. I’ve been thinking about toposes internal to toposes - specifically models of ZF - and the requirement for finite limits got me mildly worried. Because really I suppose we would ask for the existence of tbe limits.

]]>Since finite sets are, by definition, the sets you can obtain by starting with nothing and repeatedly taking a binary coproduct with a singleton, you aren’t going to be able to get to any non-finite set that way, regardless of whether it is D-finite. (-:

]]>That’s pretty much it. If I have a diagram $S\to C$ where $S$ is non-finite D-finite, I suppose we need to take a non-finite D-finite product in constructing its limit, and I have a hard time imagining that in terms of binary products, as I tend to think of an iterated product described thus as a rooted binary tree.

]]>I don’t see anything that goes wrong with the usual proof that any finite limit is constructible from nullary and binary products and equalizers. Are you asking whether you can also construct non-finite D-finite limits? That seems doubtful to me.

]]>I am wondering, if we are working in Choice-free foundations, about the bifurcation of the sorts of finite (co)limits we can have. To save typing, I will only consider limits, and also because they seem to be what I need to think about for what I’m working on.

We have the standard result in usual foundations that terminal object, binary products and equalisers implies all finite limits, but in the case where we have the existence of non-finite D-finite sets, do we still get this? In particular, might it be the case that really we would like the existence of the smaller class $tbe$ of limits generated by terminal object, binary products and equalisers? For the sort of simple reasoning I’m envisaging, these are certainly all I’d want. It seems to be only theorems do we usually get given an arbitrary finite diagram of which we need to take the limit. But could these really be referring to $tbe$-limits? (Hammering the point, I know, but I’m genuinely curious.) Of course, I’ve probably just hidden the non-finite, D-finite sets in the definition of ’generated’, but can we adjust that definition so it is something along the lines of ’generated by a finite sequence involving $t$, $b$ and $e$, which is in bijection with a standard numeral’?

]]>