What does it mean if we disable K-rule in Agda?

TL;DR: Can I say, "K-rule in Agda enables people to match $$\forall a.a \equiv a$$ with $$refl$$"?

In https://agda.readthedocs.io/en/v2.5.4.1/language/without-k.html#without-k, K-rule is introduced as an implicit rule and it's defaultly enabled. If I understand it correctly, it means parameter of type $$\forall a.a \equiv a$$ can be matched with $$refl$$. If we disable K-rule, what will happen? What kind of codes is it going to prevent me writing? Because we can always construct $$\forall a . a \equiv a$$, even without K, we can always get an instance of $$T$$ by passing $$refl$$ to any functions with type $$\forall a.a \equiv a \rightarrow T$$.

Agda's doc has given me an example which indeed shows a circumstance that can only work with K:

K : {A : Set} {x : A} (P : x ≡ x → Set) →
P refl → (x≡x : x ≡ x) → P x≡x
K P p refl = p


In this code, if we can pattern match x≡x with refl, P refl can be trivially equivalent to P x≡x (but without K, we can't).

So does that mean: "K enables people to match $$\forall a.a \equiv a$$ with $$refl$$"? I didn't find the answer on the Agda doc.

If we disable K, will the semantic of Agda's equality type (CH-ISO) change?

Axiom K is related to "Uniqueness of Identity Proofs", which says is that any two proofs of equality are themselves equal to each other (i.e. are both Refl). Agda doesn't include K as an axiom, but it (and UIP) can be proved as a theorem using Agda's dependent pattern matching.

Axiom K is inconsistent with homotopy type theory, where the univalence axiom provides ways of constructing equalities other than refl. For example, if there are two functions that are pointwise equal, univalence asserts that there is an equality term equating them, but it cannot be refl if the functions have different implementations.

All removing K from Agda does is add restrictions to pattern matching, making fewer matches typecheck. The runtime semantics are unchanged, and no new programs typecheck.

For some excellent introductions on the subject, I recommend:

Pattern Matching without K

Unifiers as Equivalences

Both of these have more detailed versions in JFP if you have access to a subscription.

• But why can $a \equiv b$ be matched as refl while $a \equiv a$ cannot? Should the later expression just a specialized version of the previous one? – ice1000 Oct 10 '18 at 19:08
• @ice1000 You can, and you get a perfectly good logical system when you do that (i.e. vanilla Agda). But that system happens to be inconsistent with the univalence axiom. As for why it's not a specialized version of the previous one, in terms of unification, they're two different operations. The first yields a solution for $a$, namely $a := b$. But the second does not give a solution for $a$, it simply provides a reflexive equation, since $a := a$ will not allow unification to progress. If we allow $a \equiv a$ to be deleted, we can prove $K$. – jmite Oct 10 '18 at 20:31
• Does this mean we can only allow unification to progress if pattern matching is yielding solutions (which means $\forall a. a \equiv a$ can never be unified (pattern matched) with anything)? What does "delete" mean here in the sense of programming? (All these are under the context of Agda without K) – ice1000 Oct 10 '18 at 21:21
• I am wondering the same thing. What does delete mean? Can unification not progress unless $\forall a.a \equiv a$ is not present “somewhere”? – protossor Jan 30 at 6:50
• Also, IIUC, does this mean one can derive K : {A : Set} {x : A} {y : A} (P : x ≡ y → Set) → P refl → (p : x ≡ y) → P p in Agda withou k? – protossor Jan 30 at 16:30