Is it possible to define general schemes internally, not necessarily finitely presented? What's difficult?

[space3time1]

A motivation for considering general schemes is to put algebraic geometries over different base rings into a single type theory, where different base rings can be simply interpreted as different contexts! For the reason why beyond finitely presented, an example is $\mathbb{Q}$ over $\mathbb{Z}$, which is not finitely presented, and we need to include $\mathbb{Q}$ in the "universal" $\mathbb{Z}$-algebraic geometry if we want to describe $\mathbb{Q}$-schemes in it.

In Foundations, the definition of schemes is restricted to those which are quasi-compact, quasi separated schemes, locally of finite presentation. However, as mentioned in Blechschmidt 21, pp 144, 153, if we choose to build the zariski topos based on f.p. algebras, we cannot even include $\mathbb{Q}$ in the $\mathbb{Z}$-algebraic geometry!

And furthermore, what are the difficulties to go beyond finite presentation in SAG?

[felixwellen]

So far, nobody has tried to use more than finitely presented algebras and covers of more than finitely many affine schemes! Also, our notion of open proposition has a finiteness assumption - it really just covers quasi-compact opens.
We just picked these restrictions because they are convenient, I know of no fundamental reason why you couldn't go beyond that. It will be more difficult though and less convenient. For example, to really work with more than finite presentations and covers, you need to fix some types you want to admit as index sets. You could take decidable subsets of the naturals, like we use in Synthetic Stone Duality, but then you need countable or even dependent choice internally - which needs to be checked, if it is available internally. And you probably would want to switch to a more complicated notion of open proposition then.