I recently learnt from David Roberts' answer that, there is a way, due to Colin McLarty, to set up the foundations on finite order arithmetic for EGA & SGA. In particular, all usages of Grothendieck universes or inaccessible cardinals in EGA & SGA are supposed to be realizable in a (conservative extension of) finite order arithmetic (or ETCS).

I am no logician, but after a glimpse at McLarty's paper, it seems that this is very different from the usual approach of choosing cut-off cardinals in, say, Stacks Project. If I understand correctly, due to lack of axiom of replacement, the usual cardinal arithmetic does not seem to work well, at least a class "being small" cannot be simply tested by its cardinality. In other words, we cannot simply understand this as a "size issue" as in ZFC.

Now I wonder whether/how much condensed mathematics can be founded on such a weaker system? If I understand correctly, there are some issues about constructing "large rings" there, so to avoid extra complications, let me restrict to the content of chapters 1-6 of Lectures on Condensed Mathematics, i.e. up to solid abelian groups. And also, to avoid complications from higher categories, I would first look at the 1-categorical structures instead of derived $\infty$-categories.

**Update:** For example, I wonder whether the proof of Prop 2.9 can be founded, or interpreted in ETCS, with some modifications of the proposition itself?

Here is a motivation for seeking such weaker systems. When we use condensed mathematics to reproduce some classical theorems (such as coherent duality and basic theorems in complex analysis), or some slight generalizations, it seems probable that their classical proofs only rely on something much weaker than ZFC, and I hope that the proof using condensed mathematics can be interpreted in at least a not-much-stronger system.

allfinite orders, and it is closely related to Lawvere's ETCS? $\endgroup$extremally disconnected sets, and every extremally disconnected set is a retract of such. Extremally connected sets are preciselycompact projectiveobjects (aka.strongly of finite presentation) of the category of condensed sets. Consequently, say, in the category of condensed abelian groups, you have enough projective objects. $\endgroup$9more comments