It is a known theorem that an internal equivalence of Lie groupoids (finite dimensional manifolds!) - that is an equivalence in the 2-category of Lie groupoids, smooth functors and transformations - is a weak equivalence: a fully faithful essentially surjective functor. Here we say a functor is essentially surjective is the map expressing this fact is not only surjective but a surjective submersion.
I'm interesting an analogues of this fact for Frechet Lie groupoids - groupoids internal to the category of Frechet manifolds, where the source and target are submersions of Frechet manifolds (this is stronger than surjective on tangent spaces - need local charts where the map looks like projection out of a direct sum).
The proof for Lie groupoids relies on the fact that Lie groupoids admit local bisections through every arrow $g$. These are maps $X_0 \supset U \stackrel{f}{\to} X_1$ where $s(g) \in U$, an open subset of $X_0$ such that $f(s(g)) = g$, and $t\circ f:U \to X_0$ is an open embedding. So far so good, the existence of local bisections depends on the characterisation of a submersion as locally a projection out of a direct sum, but with a small twist, which I haven't thought about, but don't expect to cause trouble.
The problem is showing that the 'surjective implies submersion' part of the proof, which uses a different characterisation of submersions of finite-dimensional manifolds, namely that admit local sections through every point in their codomain. This is false in the general Frechet case, but it doesn't mean the proof couldn't be rewritten to use the other characterisation of submersions (locally a projection).
My question is: has this been done?