- Les niveaux d'univers d'un quotient, je ne les connais pas bien, mais
mon intuition me dit que `Quotient τ R` devrait pouvoir être dans le même niveau d'univers que celui de `τ`, quelque soit `R`, vu que c'est un "sous ensemble" de `τ`. Pas sûr si c'est vrai dans HoTT, par contre. J'imagine qu'en pratique ça fait probablement pas de grosse différence, donc ton choix est plus sûr.
Je sais pas si concrètement ça poserait des problèmes si le niveau d’univers de `Quotient` ignore celui de `τ`. Pour nous rassurer un peu, Cubical Agda utilise aussi le max des 2 niveaux :)
Oui, c'est le choix le plus sûr et dans presque tous les cas le niveau de `R` sera le même que celui de `τ` de toute façon, donc ça vaut pas la peine d'essayer d'être plus permissif.
Au fait, j’ai appris que dans l’absence de la ’set truncation’, si on construit le type quotient de `Unit` avec une relation totale quelconque, il se trouve que ça nous donnerait quelque chose qui est equivalent à S¹, c’est à dire le type avec les constructeurs suivants:
data S¹ : Type where base : S¹ loop : base ≡ base
En effet, dans HoTT ce type est considéré plus ou moins comme `Nat` (où zéro correspond à `base`, et le successeur correspond à l'application de `loop` via `transport, IIUC). Ça reste assez mystérieux pour moi.
Ah alors là, en fait j’ai déjà essayé de faire ça, mais il y a eu un petit problème lors de l’élaboration, j’ai rencontré l’erreur qui dit "Bug in the elaboration of a repeated metavar!”. Pour l’instant, je vais juste ajouter un commentaire dans le code.
Très bien, oui: mets un FIXME quand la version idéale ne marche pas.
Sinon, j’ai effectué tous les autres petits changements que vous avez conseillés :)
Avec les derniers changements que j'ai poussé dans `main` tu devrais pouvoir éliminer `type_quotient_type` et ajouter "Quotient" à `builtin_axioms` à la place.
Aussi, je crois que dans le commit:
Implement `Eq` constructor for `Quotient`
tu devrais ajuster la règle d'élimination du `cast` pour qu'il s'applique aussi à `cast + Quotient.eq` de même qu'il s'applique à `cast + Eq.eq` (et ajouter un test correspondant).
Stefan