Let me expand a bit my comment as this is a rather subtle property.

As I said any locally compact Hausdorff topological space is a strongly hausdroff locally compact locales. (and under the axiom of choice the two notion are completely equivalent) So this does not exaclty answer the precise question you ask, but as it applies to all topological manifold, it should be sufficient for your purpose.

The result you need for this is lemma C4.1.8 of sketches of an elephant which says that:

**Lemma :** (C4.1.8 in Sketches) The product of a locally compact spatial locale with a spatial locale is spatial.

The reason that it gives you what you want is because the only reason why Hausdroff and strongly Hausdorff are differents is because in general the product $X \times X$ in the category of locales can be non-spatial even if $X$ is spatial, hence asking that the diagonal map $X \rightarrow X \times^{top} X$ in the category of topological space is closed only say that the map from $X$ to the largest spatial sublocale of $X \times X$ is closed. But this largest spatial sublocale can be itself not closed and so it does not implies that the locale is strongly Hausdorff. But because of the lemma above, if $X$ is locally compact then $X \times X$ is spatial and so the product in the category of topological space and the product in the category of locales are the same.

This is enough for the treatment of manifolds.

I wouldn't be surprise if results of this kind also holds under only paracompactness assumption. But having only studied the constructive theory of locales I know very little of paracompactness in this framework so I leave to someone else to comment or answer about this.

**Side note :** I would like to add a last remark regarding your project: classically (i.e. assuming the axiom of choice and the law of excluded middle) there is a complete equivalence between locally compact strongly Hausdorff locales and locally compact Hausdorff topological spaces, so you will have no problem formulating differential geometry in this framework and it will not say anything new.

In constructive settings this is no longer true. In fact if you look at section D4.7 of Sketches of an elephant you will see a very interesting feature:

In constructive mathematics one can define a ``locale of real numbers'' which is always locally compact and Hausdorff but which is in general not spatial, i.e. not the same as the topological spaces of real numbers. And constructively The topological space of real numbers can even fail to be locally compact ! In fact it will be isomorphic to the locale of real number if and only if it is locally compact.

So clearly, if one wants to do differential geometry in constructive mathematics one HAS to use locales instead of topological space (or we need to say goodbye to local compactness... which would basically the end of everything in differential geometry) and I have never seen anyone develop that point of view.

(Also note that this is not related to AC, but really to LEM: the law of excluded middle alone is already enough to prove that the topological space of real number is locally compact/the locale of real number is spatial)

1more comment