最近，一种称为 DHOL 的高阶逻辑扩展被引入，它用依赖类型丰富了语言，并创造了一种强大的外延类型理论。本文提出了两种将选择添加到 DHOL 的方法。我们通过希尔伯特的非确定选择算子 $\epsilon$ 扩展 DHOL 项结构，定义了选择项到 HOL 选择的翻译，该翻译扩展了现有的从 DHOL 到 HOL 的翻译，并证明了翻译扩展的完备性，并论证了其健全性。最后，我们在一组需要选择的依赖 HOL 问题上评估了扩展的翻译。