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.
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
$\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$.
