So how does doing the same thing (rewriting) result in a "difference"?
Evaluating an expression is the same thing as providing the continuous transformation of the expression to normal form.
Proving f:A -> B is providing the continuous transformation of an expression of type A to an expression of type B.
You've never heard of dependent types? *tsk*tsk*tsk*godelian wrote: ↑Sat Mar 02, 2024 1:12 pm In your example, x=x generally evaluates to true, unless x is an undefined value of sorts. In that case, it may evaluate to false or undefined, but that depends on the language/implementation at hand. For example, null == null is true in C but undefined === undefined is false in JavaScript.
https://en.wikipedia.org/wiki/Dependent_type
That's what evaluation IS. It's a demonstration that two expressions are of equivalent value. EQUI. VALENT.
That's what the axiom of identity IS!
LHS ≡ RHS
You really need to re-examine what a Mathematics looks like from the lens of Univalent foundations; and from the intuition of a Computer Scientist.