Comment by zmgsabst
8 hours ago
HoTT distinguishes equality from equivalence.
Univalence says that equality is equivalent to equivalence, ie, formalizing the notion of when we can use equivalence rather than equality as a step in a proof. In practice, we often only care about proofs “up to equivalence”.
A way to think about this:
- equality is an identity map
- equivalence is an isomorphism
For example, 2 in Z and 2 in R do not have an identity map between them — but do have an isomorphism.
I think the key insight of univalence is not collapsing equivalence into equality — but allowing it to remain a second truth relation.
We don’t want 2 in Z to be equal to 2 in R (because we collapse type distinction), but we do want them to be equivalent — so we can do equivalent reasoning about arithmetic in R to reach conclusions about Z.
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.