[TYPES] Admissibility of conversion rule for typed definitional equality

[Meven Lennon-Bertrand]

Hi Wassim,

I'd be very surprised if this rules was admissible, although I don't 
quite have a formal refutation.

But consider the following setting: a function f : (x : nat) -> P such 
that P[0/x] = nat -> nat, and a term t such that t = 0 : nat. How do you 
deduce that f 0 0 = f t t? First, by congruence of application (and 
since by reflexivity f = f : (x : nat) -> P), we have f 0 = f t : P[0]. 
To use congruence again, though, you need to turn this into f 0 = f t : 
nat -> nat. How are you going to do that without the rule you think is 
admissible? Reflexivity, symmetry and transitivity don't change the 
types at which the conversion(s) happen, so they won't help. And all 
other rules (congruences and basic equalities, like β and η) change the 
terms. I guess your idea was to use the conversion rule for typability 
since that allows you to conclude f 0 : nat -> nat, but I don't think 
that this is of any use here.

Best,

Meven LENNON-BERTRAND
Postdoc – Inria & IRIF, Université Paris Cité
https://urldefense.com/v3/__http://www.meven.ac__;!!IBzWLUs!RLNIoSoYq3NnOSiQZdBRAeimWLDke5TxmhuJVBUVW6cZ1mxKHNnPzscZQ7JHQQDhkSbHtBPbwnY5E55ASmPJNkHIKRtRsudx0QHuVQ$ 


On 15/06/2026 18:03, Wassim Ait Moussa wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list  ]
> Hey all,
>
> In the typed presentations of definitional equality for dependently typed
> systems I've come across (Such as UTT
> <https://urldefense.com/v3/__https://www.lfcs.inf.ed.ac.uk/reports/94/ECS-LFCS-94-304/index.html__;!!IBzWLUs!U-3GuY4s1OJlYhS9u14MO64vFqV5L3njo_1o9t3lvwjHoPQkW1nX8w2QNuIk9F_exafScYcaNqgwY6zOcvkdSrXLOqaGznCQfD0$ > or Agda
> Lite <https://urldefense.com/v3/__https://jesper.sikanda.be/files/thesis-final-digital.pdf__;!!IBzWLUs!U-3GuY4s1OJlYhS9u14MO64vFqV5L3njo_1o9t3lvwjHoPQkW1nX8w2QNuIk9F_exafScYcaNqgwY6zOcvkdSrXLOqaGhOKnsjk$ >), there
> seems to be a conversion rule of the form of "If a = a' at type A, and A =
> B then a = a' at type B".
>
> I would tend to believe such a rule is admissible. Would anyone have a
> refutation of that, or some example of a work in which such a rule is not
> needed ?
>
> Thanks!
> Wass