Salut James, T'avais raison de rester avec une égalité propositionnelle pour tes types quotient: renforcer l'égalité définitionnelle pour les types quotients pose des problèmes. Soit le type quotient A/F où A est le type de base et F est une fonction qui prend un argument de type A et renvoie la classe d'équivalence à laquel il appartient. Soit une élimination comme: Qrec: ?A/?F → (f : ?A → ?t) → (P : ∀ x,y . ?F x = ?F y → f x = f y) → ?t; qui dit que tu peux appliquer `f` au "contenu" d'un quotient ?A/?F pour autant que tu prouves avec `P` que `f` traite tous les éléments d'une même classe de la même manière. Le problème est que l'élimination ne garanti que l'égalité propositionnelle du résultat. Donc si tu permets à deux valeurs différentes de type A/F d'être définitionnellement égales, t'as un problème, parce que tu casses le principe que e₁ ≃ e₂ => E[e₁] ≃ E[e₂] Plus concrètement, disons que le constructeur des quotients est Qin, si tu as e₁ ≄ e₂ ∧ Qin e₁ ≃ Qin e₂ tu peux montrer que E[Qin e₁] = E[Qin e₂] parce que ton `Qrec` te donne cette `=` (i.e. égalité propositionnelle), mais tu ne peux pas montrer que cette égalité est vraie définitionnellement (`≃`), et en effet elle n'est pas vraie définitionnellement si le `f` de l'éliminateur est la fonction identité (qui est un cas possible si le contexte nous fournit la preuve `P`). Donc à moins de faire attention que `Qrec` renvoie toujours une valeur "normalisée", on perd la propriété de "subject reduction". 🙁 Étonnement, je n'ai encore pas vu une telle explication dans mes lectures. Toi? Stefan