1
$\begingroup$

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.

$\endgroup$

1 Answer 1

3
$\begingroup$

$\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$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.