have a four-dimensional formal manifold with a given pseudo-Riemannian structure.

There exist the models of pseudo-Riemannian structure on a formal manifold in different well adapted models.

So we have the method of construction of models of intuitionistic General Theory of Relativity in cartesian closed categories, and, in particullary, in toposes.

In model ${\bf Set^{L^{op}}}$ the Einstein’s equations at stage $\ell A =\ell C^\infty(\R^n)/I$ in vacuum have the following form: $$R_{ij}(u) - \frac{1}{2} g_{ij}(u) R(u) = 0 mod I,  \eqno(*)$$ where the argument $u\in\R^n$ is some “hidden” parameter corresponding to the stage $\ell A$, i.e. we got the non-denumerably infinite collection of equations. The solution of these equations is serious problem. At stage ${\bf 1}=\ell  C^\infty(\R^0) = \ell C^\infty(\R)/(x)$ the equations (\*) coinside with the usual Einstein’s equations.

Space-time as Grothendieck topos
================================

There is still another possibility of applying topos theory to a mathematical description of space-time. One can attempt to achieve the desired simplicity when axiomatizing relativity theory at the cost of giving up the classical view that space-time is the world of events “placed” in a single “space”.

To this end, consider a partially ordered set $<{\bf P}, \preceq >$ and contravariant functors from the pre-category ${\bf P}$ 