In any case, this suggests that we do have at least a forgetful functor from Pyknotic sets to the category of sheaves I described.

(Edit: the next sentence is wrong. see Peter Scholze's answer and my comment below it.) In any case, this suggests that we do have at least a forgetful functor from Pyknotic sets to the category of sheaves I described.

So, I wanted to say something, I don't think this answer the questions, but that was definitely too long for a comment. This is just the result of me trying to make sense of this idea:

Coming from topos theory, a "forcing extension" is for me a category of sheaves on a boolean locale, that is complete boolean algebras $\mathcal{B}$. These are functorial on morphisms of boolean locales:

If I ignore size issue for now (because they are present and can be handled in the same way for what I'm going to talk about and for Pyknotic sets), I can take a kind of (co)lax (co)limits (the "co" depending on how you fix the variance of the functoriality) of all these forcing extentions:

To be precise, I'm asking to have for collection of sheaves $X_{\mathcal{B}} \in Sh(\mathcal{B})$ for each Boolean locale $\mathcal{B}$ with comparison maps $f^* X_\mathcal{B} \to X_\mathcal{B'}$ for each morphism of boolean algebra (asking for isomorphism would collaps the notion)

Now, this is exactly the same as a sheaf on the categoy of all boolean locales, with the topology of open covering.

Small remark: Note that as a morphism of boolean locale is automatically an open maps one can also consider the topology where epimorphism (hence open surjection) and coproducts give the covering which is a bit stronger and also makes a lot of sense in this picture, but isn't going to change what I want to say.

So, this looks a lot like Pyknotic/condensed sets, but there is one big problem:

Here I look at morphisms of boolean locales, so up to the variance, map of boolean algebras that preserve supremums.

In Condensed/Pyknotic mathematics one considers the category of complete boolean algebra with arbitrary maps of boolean algebra. So this category has more maps.

Now, that is probably not be the end of the story: these additional maps actually also make sense from the point of view of forcing models: They corresponds to the ultraproduct (or filter-quotient?) construction. If $\mathcal{B}$ is a complete boolean algebra, a map of boolean algebra $\mathcal{B} \to \{0,1\}$ is justs an ultrafilter on $\mathcal{B}$ and I have a functoriality $Sh(\mathcal{B}) \to Set$ given by taking germs along this ultrafilter.

In any case, I think we do have at least a forgetful functor from Pyknotic sets to the category of sheaves I described.

So, I wanted to say something, I don't think this answer the questions, but that was definitely too long for a comment. In short, this is just the result of me trying to make sense of this idea:

Coming from topos theory, a "forcing extension" is for me a category of sheaves on a boolean locale, (that is a complete boolean algebras) $\mathcal{B}$. These are functorial on morphisms of boolean locales:

If I ignore size issue for now (because they are present and can be handled in the same way for what I'm going to talk about and for Pyknotic sets), I can take a kind of (co)lax (co)limits (the "co" depending on how you fix the variance of the functoriality) of all these forcing extensions:

To be precise, I'm looking at the category of collections of sheaves $X_{\mathcal{B}} \in Sh(\mathcal{B})$ for each Boolean locale $\mathcal{B}$ with comparison maps $f^* X_\mathcal{B} \to X_\mathcal{B'}$ for each morphism of boolean algebra (asking for isomorphism would collaps the notion)

An example of such an object is if you look at the "set" of functions from $X$ to $Y$. Indeed, in each new forcing model you get potentially more functions from $X$ to $Y$, so you have comparison map $f^*[X,Y]_\mathcal{B} \to [X,Y]_{\mathcal{B}'}$ which in general are not isomorphismes).

Now, this category of collection is equivalent to the category of sheaves on the categoy of all boolean locales, with the topology of open covering.

Small side remark: Note that as a morphism of boolean locales is automatically an open maps one can also consider the topology where epimorphism (hence open surjection) and coproducts give the covering. This topology is a bit stronger, but also makes a lot of sense in this picture, in fact I tend to find it more natural. For example the object [X,Y] described above is a sheaf for this stronger topology. This however doesn't really affect the next point.

So, this looks a lot like Pyknotic/condensed sets, but there is one big difference:

Indeed, here I look at the category of boolean locales, so up to the variance, the morphisms are map of boolean algebras that preserve supremums.

In Condensed/Pyknotic mathematics one considers the category of complete boolean algebra with arbitrary maps of boolean algebras. So this category has more maps. (The variance seems to match though)

Now, that is probably not be the end of the story: these additional maps actually also make sense from the point of view of forcing models: They corresponds to a generalized ultraproduct (or should I say filter-quotient?) construction. For example, if $\mathcal{B}$ is a complete boolean algebra, a map of boolean algebra $\mathcal{B} \to \{0,1\}$ is justs an ultrafilter on $\mathcal{B}$ and I have a functoriality $Sh(\mathcal{B}) \to Set$ given by taking germs along this ultrafilter.

In any case, this suggests that we do have at least a forgetful functor from Pyknotic sets to the category of sheaves I described.