Recently an extension to higher-order logic -- called DHOL -- was introduced, enriching the language with dependent types, and creating a powerful extensional type theory. In this paper we propose two ways how choice can be added to DHOL. We extend the DHOL term structure by Hilbert's indefinite choice operator $\epsilon$, define a translation of the choice terms to HOL choice that extends the existing translation from DHOL to HOL and show that the extension of the translation is complete and give an argument for soundness. We finally evaluate the extended translation on a set of dependent HOL problems that require choice.

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