# Proving transitivity in an intuitionistic type theory without the K rule

In Agda, if I disable axiom $$\mathbb{K}$$ I'm not able to prove $$\forall\{A : \textbf{Set}\}\{a\ b : A\}\{p\ q : a \equiv b\} \to p \equiv q,$$ which I guess is normal since the system does not truncate equalities. However, I'm still able to prove transitivity $$\forall \{A : \textbf{Set}\}\{a\ b\ c : A\} \to (b \equiv c) \to (a \equiv b) \to (a \equiv c)$$ by pattern matching on $$\textit{refl}$$s, i.e. $$\textit{trans }\textit{refl }\textit{refl} = \textit{refl}$$. Am I missing something obvious here? What axiom is the system applying to assume the path is the reflexivity path (is it axiom $$\mathbb{J}$$?)? Thanks in advance.

$$\newcommand{\J}{\mathsf{J}} \newcommand{\K}{\mathsf{K}} \newcommand{\refl}{\mathsf{refl}}$$
Yes, this just uses axiom $$\J$$. $$\K$$ is only necessary for translating certain particular cases of pattern matching.
$$\J$$ works when you have an identity like $$p : E \equiv a$$, where $$a$$ is a variable that doesn't occur in $$E$$. Then you can reduce the proof obligation to one where we have replaced $$p$$ by $$\refl : E \equiv E$$ while replacing $$a$$ with $$E$$. In Agda, this is presented as matching on the case $$\refl$$ (and 'matching' $$a$$ with the pattern $$.E$$ if it's an explicit argument). In the $$\mathsf{trans}$$ case, this easily applies both times (and there are variables on both sides, so you could also consider an opposite version of $$\J$$ where $$E$$ is on the right).
The proof that all identities $$a \equiv b$$ are equal fails this rule. Using the above method, one match will refine $$p$$ to $$\refl$$ and $$b$$ to $$a$$, meaning the second match is on $$q : a \equiv a$$. Now $$a$$ is on both sides, and we can't justify the match with $$\J$$, and require $$\K$$.