Topological completeness of the provability logic GLP

Provability logic $\mathbf{GLP}$ is well-known to be incomplete w.r.t. Kripke semantics. A natural topological semantics of $\mathbf{GLP}$ interprets modalities as derivative operators of a polytopological space. Such spaces are called GLP-spaces whenever they satisfy all the axioms of $\mathbf{GLP}$. We develop some constructions to build nontrivial GLP-spaces and show that $\mathbf{GLP}$ is complete w.r.t. the class of all GLP-spaces.