Comment by js8

Yeah, but a similar thing works with programs (terms in normal forms in triage calculus). There is equality of terms and equivalence with respect to beta reduction.

(I used equal to mean the latter, this is colloquial, so I should watch my language.)

And what I am saying in my version of univalence is not that these two are the same, but rather, we can simulate beta-reduction equivalence using self-interpretation.

My version of the axiom states, that two terms x, y are beta-equivalent iff the term interpret(quote(x)) is beta-equivalent to term interpret(quote(y)).

(Note that quote() is identity function in triage calculus, I only write it for clarity.)

So my axiom postulates that the metalogical notion of equivalence is equivalent to the one we can study using whatever interpret() - a self-interpreter - is.

Whether my axiom is related to univalence in HoTT, I am not sure. But it feels similar.