Forcing over a partial order $$P$$ can be viewed in a category theoretic sense as constructing the presheaf topos $${\bf Set}^{P^{op}}$$ over the partial order (viewed as a category) then passing through the double negation transformation to recover a Boolean topos instead of an intuitionistic one, as explained by Sridhar Ramesh in the comments here.

It is not entirely clear to me whether this process is (pseudo-)functorial, i.e. if there is a (pseudo-) functor $$\mathsf{Force}:{\bf Pos}\to\mathfrak{Top}$$ which takes a poset to the double negation of its presheaf topos. In particular I believe all we would need is for $$\neg\neg$$ to be functorial. This leads me to two questions:

1. Is $$\neg\neg$$ functorial?
2. If the answer to 1 is yes, does $$\mathsf{Force}:{\bf Pos}\to\mathfrak{Top}$$ have a left or right adjoint?

Below is a suggestion of how $$\mathsf{Force}$$ might be constructed, apologies if any glaring errors are made. The Yoneda embedding $$y_P$$ takes a poset $$P$$ to the subcategory $$y_P(P)\hookrightarrow{\bf Set}^{P^{op}}$$ of representable presheaves, so we can take a functor $$F:P\to P'$$ between poset categories to a functor $$y_F:y_P(P)\to y_{P'}(P')$$ between these subcategories by defining $$y_F\big({\bf Hom}_P(-,X)\big)={\bf Hom}_{P'}(-,F(X)),$$ $$y_F\big({\bf Hom}_P(-,f)\big)={\bf Hom}_{P'}(-,F(f)).$$ $${\bf Set}^{P^{op}}$$ is presentable as colimits over $$y_P(P)$$, so I believe this functor extends to a functor (up to iso) $$\overline y_F:{\bf Set}^{P^{op}}\to{\bf Set}^{P'^{op}}$$ given by representing each presheaf $$G\in{\bf Ob}_{{\bf Set}^{P^{op}}}$$ as a colimit of some functor $$G^\star:\mathcal{G}\to y_P(P)$$ over representable presheaves $$G=\varinjlim_{X\in{\bf Ob}_\mathcal{G}}G^\star(X)$$ and then sending $$G$$ to the colimit of the image of these representable presheaves under $$y_F$$, $$\overline y_F(G)=\varinjlim_{X\in{\bf Ob}_\mathcal{G}}y_F(G^\star(X)),$$ and sending a natural transformation $$\alpha:G\Rightarrow G'\in{\bf Hom}_{{\bf Set}^{P^{op}}}$$ to the natural transformation $$\overline y_F(\alpha):\overline y_F(G)\Rightarrow \overline y_F(G')$$ given by $$\overline y_F (\alpha)=[\{\alpha_Z\circ\nu^X_Z\}_{Z\in{\bf Ob}_P}]_{X\in{\bf Ob}_P}:\varinjlim_{X\in{\bf Ob}_\mathcal{G}}y_F(G^\star(X))\Longrightarrow\varinjlim_{Y\in{\bf Ob}_{\mathcal{G}'}}y_F(G'^\star(Y)),$$ where $$\nu^X_Z:y_F(G^\star(X))(Z)\to\varinjlim_{X\in{\bf Ob}_P}y_F(G^\star(X))(Z)$$ is the coprojection for $$y_F(G^\star(X))(Z)$$.

I believe we thusly have a functor $$y:{\bf Pos}\to\mathfrak{Top}$$ given by $$y(P)={\bf Set}^{P^{op}},$$ $$y(F:P\to P')=\overline y_F,$$ so if $$\neg_\mathcal{E}\neg_\mathcal{E}:\Omega\to\Omega$$ in a topos $$\mathcal{E}$$ extends to an endofunctor $$(\neg\neg)_\mathcal{E}:\mathcal{E}\to\mathcal{E}$$ we may be able to extend to an endofunctor $$\neg\neg:\mathfrak{Top}\to\mathfrak{Top}$$ and define $$\mathsf{Force}=\neg\neg\circ y$$. Does this work out?

• Have you had a look at MacLane and Moerdijk's "Sheaves in geometry and logic"? They have a whole sectin about this. – Andrej Bauer Jan 19 '19 at 8:45
• Page 277, section VI.2 on the Cohen topos. You should also look up (somewhere) the fact that the construction $C \mapsto \mathbf{Set}^{C^\mathrm{op}}$ is functorial in the site $C$ (so you don't have to do that part with your bare hands). After that it's "obvious" that the construction is functorial. – Andrej Bauer Jan 19 '19 at 9:19
• @AndrejBauer huh, so $P \mapsto (P,\neg\neg)$ is a functor from posets to sites? Nice. I do wonder if it's more generally true for non-posetal categories. However, Alec was probably wanting something like a functor $\neg\neg\colon Topos \to Topos$. I can see how this is likely true for logical functors of toposes, but for geometric morphisms? – David Roberts Jan 19 '19 at 10:43
• But it is common knowledge that it is functorial, which is precisely why you shouldn't trust the rumours. – Andrej Bauer Jan 19 '19 at 11:11
• Well, anyway, the lack of a functorial Borel map selecting generic filters for the countable models of set theory is interesting. It shows that the quotient step you mention is inherently difficult to achieve in a uniform way. – Joel David Hamkins Jan 19 '19 at 17:29