@Gro-Tsen Interesting. I guess that should work. I wasn't aware of that impredicative formula.

@JamesEHanson Yes you are correct: The locale I'm refering too is not a sublocale of R but a locale X with a monomorphism X→R (I corrected this). I thought this was this X that Simpson considered, but I should go, I think he might be looking at its image in R.

@Gro-Tsen I've added an "unbounded" description - this is the best I think is doable in term of "logical simplicity" but maybe there are some simplification (for e.g. by wirrting more explicitely what happen when we iterate $j_0$).

If you are happy with formula that include an ** unbounded ** join or meet, that is indexed by either proper class or at least sets whose size depends on the size of the frames (for e.g. running over all ordinals, or all elements of one of the two frames) then I think I can write down a formula. Back when I was thinking at related problems, I was in a setting where the frame where large sets (due to the lack of power sets) and I needed to find expression that only involved "small" operations - and this turned out to be impossible.

I'm relatively sure no such simple expression exist, I'm not entirely sure what would qualify as a negative result though.

It can be any class that satisfies the assumption of the theorem. But it is meant to be the class of trivial cofibrations between cofibrant $\kappa$-presentable objects. Typically in the situation I was talking about above where you have a Brown category J is the class of cofibrations that are weak equivalences.

... Note that condition (iii') of the theorem is obtained from a relative cylinder by taking B=B' and C to be the relative cylinder $B \coprod_A B \hookrightarrow C \overset{\sim}{\to} B$

I'm not sure I understood the question correctly but: Theorem 2.4 in the linked paper implies that if you start with a finitely presentable category and $I$ generating cofibrations between finitely presentable objects. Then if the category of finite $I$-cell complex is a Brown category where the cofibration are the relative $I$-cell complexes (which is closely related to having a factorization as in the question) then this extend into a left semi-structure on the whole category which is cofibrantly generated by $I$ and by the set of "trivial cofibrations" of the Brown category.

@JamesEHanson Well if you define $\mathbb{C}$ this way, then you can argue it is an algebraic definition (one can still debate over whether the cardinality requirement is is an algebraic notion of not), but then the fundamental theorem of algebra has a pretty obvious "algebraic" proof...

To be precise. $KH$ is the ex/reg completion of the category of profinite sets. So it is the pretopos completion only whem the category of profinite set is considered as a regular and extensive category. (i.e. a functor fron profinite set to a pretopos extent to a pretopos morphism on $KH$ if it is a regular and coproduct preserving functor...)

In fact the Dedekind real are exactly the one sided Dedekind cut $x$ such that there is another one sided cut $y$ satisfying $x+y = 0$.

@StevenStadnicki you can define anything you want however you want, but you won't be able to prove any of the expected properties. For example defining $-x$ this way, you don't have $x - x =0$, unless your topos is boolean. While using two sidded cut you get an honest rings. The condition I put in my answer correspodns to the fact that if two real $x$ and $y$ are such that $x <y$, then there exists a real (even a rational) $z$ such that $x <z<y$. So you won't get that either with your definition.