[TYPES] Admissibility of conversion rule for typed definitional equality

[Wassim Ait Moussa]

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