Où est la preuve que Coq + Excluded Middle est cohérent

J'ai vu (et entendu) qu'il a affirmé qu'il est sûr d'ajouter l'axiome classique du milieu exclu à Coq, mais je n'arrive pas à trouver un document soutenant cette affirmation. Les articles que je vois répertoriés sur le wiki Coq sur le milieu exclu montrent une incohérence avec l'ensemble imprédicatif.

En effet, il semble que Coquand déclare que l'ajout du milieu exclu (un habitant de ) est incohérent pour CoC dans la section 4.5.3 de sa description (PDF) de la métathéorie de CoC. Cependant, cette section est un peu abstraite pour moi, donc je peux très bien le mal interpréter.$A+\neg A$

En fait, dans la section 4.5.3, il ne dit pas tout à fait que l'imprédicativité EM + est incohérente. Il dit que lorsque vous l'assumez, le modèle doit devenir dégénérativement non pertinent pour la preuve (l'interprétation de tous les types autres que Prop peut avoir au plus un élément). Andy Pitts décrit un phénomène similaire: "Les types de puissance non triviaux ne peuvent pas être des sous-types de types polymorphes" .

Pour les versions prédicatives de la théorie des types, il est probablement plus facile de simplement faire la preuve de cohérence que pour Google - la stratification de l'univers vous donne tout ce dont vous avez besoin pour le modèle de type théorique simple des types (c'est-à-dire que les types sont des ensembles, les termes sont cartes) pour travailler. Observez simplement que les ensembles sont fermés sous des sommes et des produits indexés, et familiarisez-vous avec l'axiome du remplacement lors de l'interprétation des univers. C'est une mauvaise pratique académique, bien sûr, mais la preuve en vaut la peine.