5
$\begingroup$

TL;DR: Can I say, "K-rule in Agda enables people to match $ \forall a.a \equiv a $ with $ \mathit{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 $ \mathit{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 $ \mathit{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 $ \mathit{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?

Improve this question
$\endgroup$

2 Answers 2

Reset to default
3
$\begingroup$

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.

Improve this answer
$\endgroup$
6
  • $\begingroup$ 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? $\endgroup$
    – ice1000
    Commented Oct 10, 2018 at 19:08
  • $\begingroup$ @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$. $\endgroup$
    – Joey Eremondi
    Commented Oct 10, 2018 at 20:31
  • 1
    $\begingroup$ 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) $\endgroup$
    – ice1000
    Commented Oct 10, 2018 at 21:21
  • $\begingroup$ I am wondering the same thing. What does delete mean? Can unification not progress unless $ \forall a.a \equiv a $ is not present “somewhere”? $\endgroup$
    – tgeng
    Commented Jan 30, 2019 at 6:50
  • $\begingroup$ 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? $\endgroup$
    – tgeng
    Commented Jan 30, 2019 at 16:30
1
$\begingroup$

I'm studying this myself and I think the only essential distinction between K and J is that:

  • The user of K is expected to provide a type P : x ≡ x → Set depending on some loop about x (a closed path).

  • The user of J is expected to provide a type Q : (y : A) → x ≡ y → Set depending on a general path that could be either open or closed. Since Q isn't allowed to assume that it is closed, J is more restrictive on the user. You can define P = Q x but the reverse is not in general possible.

From a homotopic point of view, K is not possible because the structure of P is too rigid; the lack of an adjustable endpoint y : A prevents P from being continuously transported along arbitrary paths.

This is evidenced by the code below:

K : {A : Set} {x : A} (P : x ≡ x → Set)
  → P refl → (p : x ≡ x) → P p
K P d p = {- impossible in HoTT/CuTT -}

J' : {A : Set} {x : A} (Q : (y : A) → x ≡ y → Set)
   → Q x refl → (p : x ≡ x) → Q x p
J' Q d p = Cubical.Foundations.Prelude.J Q d p
Improve this answer
$\endgroup$
1
  • $\begingroup$ Yes! That's also how I would say it after many years of studying of HoTT. $\endgroup$
    – ice1000
    Commented Jul 20, 2023 at 14:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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