Andree C. Ehresmann wrote:
Already in the fifties, Charles Ehresmann has introduced and extensively studied categories internal to Diff (which he called "categories differentiables") in his development of Differential Geometry.
I'm sorry to have not yet gotten ahold of the references you provided - I got distracted by other matters - but if you will forgive my laziness, I'll ask another question:
Could someone please explain how Charles Ehresmann dealt with the fact that Diff does not have all pullbacks? In the definition of internal category we need a pullback to exist: the "object of composable pairs of morphisms", C_1 x_{C_0} C_1. These days, people working on Lie groupoids usually impose some requirements on the source and target maps s,t: C_1 -> C_0 that ensure that this pullback exists. Personally I lean towards a simpler approach, which is simply to demand that the pullback exists. This makes it harder to prove certain theorems, but has a certain charm. I'm wondering what Charles Ehresmann thought about this issue.
Best,
The category Diff has pull-backs of transversal maps, and furthermore these are the only "correct" pull-backs. A natural (and "necessary") requirement for the existence of a given pull-back is transversality, which has a lot of charm. In the well adapted models of SDG all pull-backs of differential manifolds exists, but they will be objects in the topos (actually C-infinity Schemes) which are not differential manifolds unless the pull-back is transversal. The work of Charles Ehresmann and Andre Weil is very much related to this fact. Best, edubuc.