First, I've already looked up into several related materials, including the HoTT book & this question.
But I'm still confused, and I'm wishing for a explanation free from Agda, but directly from its mathematical formula. After removing the dot notation, J axiom then says like this, whose type signature is completely the same in the answer of the question I've mentioned above:
J : forall {A : Set} {C : (x y : A) → (x ≡ y) → Set} →
(c : ∀ x → C x x refl) →
(x y : A) → (p : x ≡ y) → C x y p
, noticing that the last line asks us to provide x, y and p. Then why
J c x x refl = c x
, (the only difference is that I've removed the dot notation)? Or to say, why the second x is written in x rather than y?
I have actually thought over this question and got my explanation, but I cannot make sure if I am correct. J's type signature is in the propositional world, but its definition is in the judgmental world. We are constructing the propositional equality class step by step but all judgmental equal variables can be instantly rewritten into each other, and when we are using J we should already have x judgmentally equal to y(since we are about to provide a path for that). But if my reasoning makes flawless sense, looking back into that question, why we are writing
cong : ∀ { a b} { A : Set a } { B : Set b }
(f : A → B ) {m n} → m ≡ n → f m ≡ f n
cong f {x} {y} p = J {C = \x y p → f x ≡ f y}
(\_ → refl)
x y p
again where the last line is providing x, y, p but not x, x, p?
When you pattern match on p at refl in the definition of J, its type is refined from x ≡ y to x ≡ x (since the type of the constructor refl is ∀ {x} -> x ≡ x, i.e. it sets both indices to x), which means we can refine both the left- and the right-hand sides by x ~ y, which is both why the y in the pattern becomes x (or, alternatively, .x in Agda to make it explicit that it is an inaccessable pattern), and also why c x : C x x refl passes on the right-hand side for the result type C x y p.