Difference between computation in proposition proof and definitional computation?
What Agda is showing you in the source code in both cases are the propositional proofs, i.e., elements of the identity type. In Agda the judgemental (definitional) equality is invisible to the user. Agda uses it in the background to verify that terms have required types. When it has to compare $a$ and $b$, it normalizes both of them (based on judgemental equalities, such as $\beta$-reduction) and compares the normalized values for syntactic equalities. There is a theorem which says that $a$ and $b$ are judgementally equal if, and only if, they have syntactically equal normal forms.

When judgemental equality has the property that things are equal preciely when they have syntactically equal normal forms, then people sometimes call it computational equality because it "computes" by computing normal forms. There is a lot of confusion in terminology.

To test judgmental equality in Agda, we can use refl to show that two things are judgmentally equal (because the rule for refl states that refl a has type b ≡ c if, and only if, b and c are both judgmentally equal to a). Here are some examples:

 open import Relation.Binary.PropositionalEquality
 open import Data.Nat

 -- this works, the normal form of 2 + 3 is 5
 p : 2 + 3 ≡ 5
 p = refl

 -- this works, the normal form of 0 + m is m
 q : ∀ m → 0 + m ≡ m
 q _ = refl

 -- this does not work, because hte normal form of m + 0 is m
 -- r : ∀ m → m + 0 ≡ m
 -- r _ = refl


You can also show that $2 + 3 = 5$ by providing an element p' of 2 + 3 ≡ 5 which is not refl, such as the one you posted in the question. In the text you read, they were just trying to demonstrate the normalization steps by making them explicit as elements of an identity type (without saying so explicitly, probably). The thing to remember is that in Agda you will never see "a proof of judgemental equality", as that always happens in the background.