Some time around 1977, André Joyal constructed a topos (actually a locale, i.e., a localic topos, necessarily non-spatial) in which the closed unit interval $[0,1]$ fails to be compact. There are only two places that I know of in which the topos in question is described or discussed:
very briefly, in a postscript at the end (p.301) of Fourman & Hyland's paper “Sheaf Models for Analysis” (p.280–301 in Fourman, Mulvey & Scott, Applications of Sheaves (Durham 1977) (1979 Springer LNM 753));
and in a somewhat more detailed way as example D.4.7.13 (p.1026–1028 in vol.2) in Johnstone's Sketches of an Elephant: A Topos Theory Compendium (Cambridge 2002).
(Johnstone describes the topos in question as the classifying topos of the theory of an open cover of $[0,1]$ such that each finite subcover has Lebesgue measure $<\frac{1}{2}$. The crucial point is that the object representing the interval $[0,1]$ is this topos comes from $\textbf{Set}$, i.e., is the constant sheaf with value $[0,1]$. Even if Johnstone's description is much more lengthy than Fourman & Hyland's 15-line postscript, it is still more an extended exercise than a full description.)
Since Johnstone does not give any other reference than Fourman & Hyland (and in particular, nothing by Joyal himself), I guess Joyal himself never published anything on the subject. Still, since this example is rather surprising and highly instructive, one might hope that it has been studied, or at least described, in greater detail, in the 20 years since Johnstone's account. So:
Question: Are there other descriptions, hopefully with even more details than Johnstone gives, of the topos in question? Has it been further studied somewhere (e.g., along the lines of what real analysis looks like in this topos)?
