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:
- Is $\neg\neg$ functorial?
- 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?
