Jensen's covering lemma states that either every uncountable set of ordinals is covered by a constructible set of ordinals of the same size or else there is an elementary embedding from the constructible universe to itself. This talk takes up the question of whether there could be an analog of this theorem with constructibility replaced by ordinal definability. For example, we answer a question posed by Woodin: assuming the HOD conjecture and a strongly compact cardinal, there is no nontrivial elementary embedding from HOD to HOD.