Given a $C^\ast$-algebra $A$, its "Bohr topos" (see there for a survey) is the presheaf topos on its commutative subalgebras. The idea here is that if we think of $A$ as the algebra of quantum operators of a quantum mechanical system (for instance all the bounded operators on the Hilbert space of states of a system), then the commutative subalgebras correspond to classically simultaneous observables, and a presheaf on these is anything that can be "probed" by all such "classical contexts". Since Niels Bohr in his informal writings propagated the idea that whatever quantum mechanics is, it should be communicatable by classical observations, this has been argued to formalize Bohr's view on quantum physics.
In any case the types in the internal logic of the Bohr topos, hence the objects of the Bohr topos, are all "observations testable on classical contexts".
The main result of this construction can be summarized as follows: a classical observable internal to the Bohr topos is equivalently a quantum observable on $A$, in the sense of QM formulated in terms of operator algebra. See at kinematics of a Bohr topos for details. This may feel like a satisfactory state of affairs. It is however as yet not quite clear what else this is going to lead to.
One should be careful with overstating what Bohr toposes achieve. Whether they serve as a "foundation of physics" would yet have to be shown. So far they serve to formalize only state spaces of quantum mechanical systems. Effectively they are a way to look at Hilbert spaces such that the notion of quantum observables fits more naturally with that of classical observables.
Already dynamics (e.g. Hamiltonians) is not captured by Bohr toposes as such. My student Joost Nuiten showed how one can formulate the local nets of observables of algebraic QFT in terms of sheaves of Bohr toposes on spacetime. See Nuiten's bachelor thesis. His main result is that the causal locality of quantum field theory is equivalent to a natural descent property of the collection of Bohr toposes assigned to each open subset of spacetime.
This does incorporate quantum field theoretical dynamics into the theory of Bohr toposes. But here, too, it is not quite clear currently what this is going to lead to. While I find this interesting, it is far from being a foundation for all of physics. It may be thought of as a topos-theoretic formulation of AQFT, though. Nice as it is, whether AQFT is even a foundation of all of Lorentzian quantum field theory is debatable.
If one really wants to see foundations of physics, one needs to dig a bit deeper, I would say. A fairly detailed proposal for how to go about this I have been describing at Synthetic Quantum Field Theory and in the articles linked to from there.
Incidentally, Joost Nuiten is just today defending his master thesis on this more comprehensive topic. See at master thesis Nuiten his work "Cohomological quantization of local prequantum boundary field theory". I gave a talk about this two days ago at the "Geometry and Physics XI"-workshop in Pittsburgh, see Motivic quantization of local prequantum field theory.
This describes a story where one starts in infinity-topos theory and discovers in there all of local prequantum field theory and eventually its motivic quantization to local quantum field theory. The examples-section of Nuiten's thesis shows how ordinary quantum mechanics is reproduced this way, the quantization of Poisson manifolds, of Poisson-model topological strings, of type II strings and of heterotic strings, reproducing in partcicular the Witten genus partition function of the heterotic 2d sigma-model field theory. If nothing else, this shows at least that there is non-trivial genuine physics captured by this formalization.