I just came across a very interesting result in *Sheaves in Geometry and Logic*, and it seemed like the sort of thing which ought to be recorded in nLab somewhere, yet isn’t.

**Theorem.** The object of Dedekind reals in the topos of sheaves on a topological space $X$ is isomorphic to the sheaf of continuous functions on $X$.

*Proof.* See Mac Lane and Moerdijk [1994, Ch. VI, §8].

At the moment, there’s an article about real numbers and an article about Dedekind cuts, but very little is said about them in the context of the internal logic of a topos. I was thinking about starting an article on the topic, but I’m not very sure what should be discussed.

]]>The page internal ∞-groupoid claimed that the case of “internal ∞-groupoids in an (∞,1)-category” was discussed in detail at groupoid object in an (∞,1)-category. That doesn’t seem right to me—I think the groupoid objects on the latter page are really only internal 1-groupoids, not internal ∞-groupoids. They’re “∞” in that their composition is associative and unital only up to higher homotopies, but those are homotopies in the *ambient* (∞,1)-category; they themselves contain no “higher cells” as additional data. In particular, if the ambient (∞,1)-category is a 1-category, then an internal groupoid in the sense of groupoid object in an (∞,1)-category is just an ordinary internal groupoid, no ∞-ness about it. Does that seem right?