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