The following strong form of density of definable types is introduced for theoriesTadmitting a fibered dimension functiond: given a modelMofTand a definable setX⊆Mn, there is a definable typepinX, definable over a code forXand of the samed-dimension asX. Both o-minimal theories and the theory of closed ordered differential fields are shown to have this property. As an application, we derive a new proof of elimination of imaginaries for CODF.

We revisit Kolchin's results on definability of differential Galois groups of strongly normal extensions, in the case where the field of constants is not necessarily algebraically closed. In certain classes of differential topological fields, which encompasses ordered or p‐valued differential fields, we find a partial Galois correspondence and we show one cannot expect more in general. In the class of ordered differential fields, using elimination of imaginaries in, we establish a relative Galois correspondence for relatively definable subgroups of the group (...) of differential order automorphisms. (shrink)