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,