I recall reading somewhere that there is a topos in which the Dedekind reals are exactly the measurable functions.
Now vector spaces are prominently characterised by dimensionality. This prompted the thought as to whether there is a topos in which the natural numbers object are the finite-dimensional vector spaces (upto isomorphism); and if there is such a topos, what would the Dedekind reals be there?