# Strong density of definable types and closed ordered differential fields

## TL;DR

This paper introduces a strong form of density for definable types in certain theories, including o-minimal theories and closed ordered differential fields, leading to a new proof of elimination of imaginaries for CODF.

## Contribution

It establishes a new density property for definable types in theories with fibered dimension functions, applicable to CODF and o-minimal theories, and uses it to prove elimination of imaginaries.

## Key findings

- Both o-minimal theories and CODF have the strong density property.
- A new proof of elimination of imaginaries for CODF is provided.
- The property links definable types with the dimension function d.

## Abstract

The following strong form of density of definable types is introduced for theories T admitting a fibered dimension function d: given a model M of T and a definable subset X of M^n, there is a definable type p in X, definable over a code for X and of the same d-dimension as X. Both o-minimal theories and the theory of closed ordered differential fields (CODF) are shown to have this property. As an application, we derive a new proof of elimination of imaginaries for CODF.