La logique d'ordre supérieur des types dépendants (DHOL), récemment introduite, offre un compromis intéressant entre expressivité et support automatisé. Elle sacrifie la décidabilité du système de types afin d'étendre considérablement l'expressivité par rapport à HOL standard, tout en conservant un support robuste pour la démonstration automatique de théorèmes via une transformation correcte et complète vers HOL. Dans cet article, nous exploitons cette conception pour étendre DHOL avec des types raffinés et des types quotients. Ces deux fonctionnalités sont fréquemment demandées par les praticiens, mais rarement fournies par les démonstrateurs automatiques de théorèmes, car elles nécessitent un typage intrinsèquement indécidable, ce qui les rend très difficiles à inverser vers un système de types décidable. Cependant, comme DHOL gère déjà ce travail complexe, leur ajout est non seulement réalisable, mais aussi élégant et simple. Plus précisément, nous ajoutons des types raffinés et des types quotients comme cas particuliers de sous-types, ce qui évite des modifications coûteuses de représentation en remplaçant les cartes d'inclusion ou de projection canoniques pertinentes par des cartes d'identité. Nous présentons des preuves d'exactitude et de complétude, ainsi que la syntaxe, la sémantique et la transformation vers HOL pour le langage étendu.
