As stated in equality at nLab, "computational equality" is about computational steps which take for example, $s(s(0))+ s(0)$ to $s(s(s(0)))$ and it acts exactly and can be considered same as definitional equality (at least in type theory).
But then if we consider $p$ in $p:Id_\mathbb{N}(a+b, b+a)$ as computation steps taking $a+b$ to $b+a$ then what is the difference between computation steps in $p$ and computation steps in above mentioned computational equality which prevents $p$ to be considered sort of a definitional equality? Are they of different computation level/form?
Or in other words, if I have got it correctly, what is the difference between $p$ in $p:Id_\mathbb{N}(a+b, b+a)$ and $p'$ in $p':Id_\mathbb{N}(s(s(0))+s(0), s(s(s(0)))) $ so that one can be considered almost the same thing as definitional equality but not the other one?
As an example following are the Agda codes in proving above mentioned reactions from Programming language foundations in Agda: Natural Numbers and [Programming language foundations in Agda: Proof by induction][3]correspondingly:
_ : 2 + 3 ≡ 5
=
-
begin
2+3
≡⟨⟩ -- is shorthand for
(suc (suc zero)) + (suc (suc (suc zero)))
≡⟨⟩ -- inductive case
suc ((suc zero) + (suc (suc (suc zero))))
≡⟨⟩ -- inductive case
suc (suc (zero + (suc (suc (suc zero)))))
≡⟨⟩ -- base case
suc (suc (suc (suc (suc zero))))
≡⟨⟩ -- is longhand for
5
∎
+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
begin
m + zero
≡⟨ +-identityʳ m ⟩
m
≡⟨⟩
zero + m
∎
+-comm m (suc n) =
begin
m + suc n
≡⟨ +-suc m n ⟩
suc (m + n)
≡⟨ cong suc (+-comm m n) ⟩
suc (n + m)
≡⟨⟩
suc n + m
∎
In my understanding both thing are computational steps that take you from left hand side to the right hand side!
Would you please answer it both intuitively and technically?
P.S. I found the following piece in Homotopy Type Theory(§1.1 p.22) which I thought might be the answer to part of my own question:
Whether or not two expressions are equal by definition is just a matter of expanding out the definitions; in particular, it is algorithmically decidable (though the algorithm is necessarily meta-theoretic, not internal to the theory).
I guess the above paragraph is talking about $\alpha$ and $\beta$ expansions. But if that is true then it raises the question that: What does a proof of a proposition has in addition to function application that makes it a different equality? Is it that beside application we do have function definitions as well in a proof definition?!