Internal equivalence implies weak equivalence for Frechet Lie groupoids? 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?
 A: I don't know whether this is really an answer, but since the question is open for a while now I'll give it a try. If I am not mistaken, then the Lie groupoids are weakly equivalent if and only if the associated 2-functors $\operatorname{Man}^{op}\to \operatorname{Grp}$ are equivalent and the argument should go through also in the infinite-dimensional case as well (btw, why do you take Fréchet-Lie groupoids, I would expect that -unlike in the Banach case- the neither the metrisability nor the completeness does any job for you). That the functors are equivalent if the Lie groupoids are even strongly equivalent is obvious. Or am I missing something?
A: This is partly an answer (or maybe more of an extended comment) and partly a response to Christoph's answer, but too long for a comment. One needs to be careful what you mean by "associated 2-functors". The most naturally associated such $2$-functor to a (say Frechet) Lie groupoid $G$, is the functor $\tilde y \left(G\right)$ assigning a manifold $M$ the groupoid of internal functors from $M$ (viewed as a Lie groupoid) to G. The stackification of this functor is the stack of principle $G$-bundles. A morphism $\varphi:G \to H$ is a strong equivalence if and only if the induced map $$\tilde y\left(G\right) \to \tilde y\left(H\right)$$ is an equivalence. A good definition of a "weak equivalence" is if the induced morphism between their associated stacks is an equivalence. Perhaps this implies that the map defining "essential surjectivity" is a submersion of sorts, but if this is not the case, perhaps one could get away with demanding this, and end up with an equivalent saturated class of morphisms to invert. At any rate, it's still an interesting question.
A: There is a characterisation of weak equivalences which works in internal categories in a) finitely complete categories and b) finite-dimensional Lie groupoids (and in fact Lie categories). In the case of Lie groupoids, an internal functor $f\colon X\to Y$ is a weak equivalence in the sense of being fully faithful and essentially surjective (as mentioned in the question) if and only if there is a fully faithful functor $j\colon Y'\to Y$ with object component a surjective submersion, a functor $s\colon Y' \to X$ and a natural isomorphism $j\simeq f\circ s$. This latter property one might call locally weakly split.
An internal equivalence gives an example of a locally weakly split functor, with $j=id$, for groupoids or categories internal to any sort of category (with a notion of covers, to make sense of essential surjectivity and the analogue of the functor $j$). One only really needs the property of being locally weakly split in order to talk about localisations of 2-categories of internal groupoids to 2-categories of presentable stacks. I don't mention it, but that is the motivation in my recent paper.
