Edit - Stack Overflow

Skip to main content

1. Home
2. Questions
3. AI Assist
4. Tags
5. Challenges
6. Chat
7. Articles
8. Users
9. Companies
11. Communities for your favorite technologies. Explore all Collectives
Stack Internal

Stack Overflow for Teams is now called Stack Internal. Bring the best of human thought and AI automation together at your work.
Try for free Learn more
Bring the best of human thought and AI automation together at your work. Learn more

You are not logged in. Your edit will be placed in a queue until it is peer reviewed.

We welcome edits that make the post easier to understand and more valuable for readers. Because community members review edits, please try to make the post substantially better than how you found it, for example, by fixing grammar or adding additional resources and hyperlinks.

Required fields*

Rev

Title*

Body*

I was trying to prove K (with without-K) using J to see what goes wrong when we try to do that.

That's all well and good, but in the process of playing around I noticed that agda refuses to match with refl any term (that I tried) of type `Id A x x` (saying something along the lines of "can't unify `x₁ ≟ x₁`").

For example, agda refuses to case split on p in the following example:
```agda
data 𝟙 : Type where
 * : 𝟙

test : {l : Level} {A : Type l} -> (x : A) -> (p : x ≡ x) -> 𝟙
test {l} {A} x p = ?
```

but the following snippet is fine:

```agda
data 𝟙 : Type where
 * : 𝟙

test : {l : Level} {A : Type l} -> (x : A) -> (p : x ≡ x) -> 𝟙
test {l} {A} x p = J {A = A} {x = x} (λ y path -> 𝟙) {y = x} p *
```

Isn't using J here like this essentially the same as case-splitting on p and assuming it to be refl? If yes, then why does agda refuse to split on p in the earlier example?

For reference the type of the J rule being used is this:
```agda
J : {A : Set a} {x : A} (B : (y : A) → x ≡ y → Set b)
 {y : A} (p : x ≡ y) → B x refl → B y p
```

Draft saved

Draft discarded

Tags

Edit Summary*

Cancel

7

They're not "essentially the same" because in your use of J, you don't use the type information you learn from the dependent pattern match. A better challenge would be to try to prove test : {l : Level} {A : Set l} -> (x : A) -> (p : x ≡ x) -> p ≡ refl using J. It's obviously easy if you allow pattern matching with K. Note that this challenge requires you to use the fact that p must be reflexivity, something you learn from the pattern match on p.

Dominique Devriese
– Dominique Devriese

2025年10月24日 12:31:34 +00:00
Commented Oct 24, 2025 at 12:31
To put what @DominiqueDevriese said in another way: your use of J could be replaced with an equivalent use of subst, and the version of subst in which x and y are judgementally equal is obviously derivable without K (you just ignore the path x ≡ x and return the identity function P x → P x).

Naïm Camille Favier
– Naïm Camille Favier

2025年10月24日 12:39:20 +00:00
Commented Oct 24, 2025 at 12:39
@DominiqueDevriese I had tried to do exactly that (knowing that it requires K) before asking this question. The reason I asked this question was to know why we have to reject pattern matching on x=x to make our system such that it doesn't use K. I may be wrong, but what I'm picking up is that J allows us to prove propositions on x=y, but when we pattern match on x=x, we are proving a proposition on x=x using J, which looks something like J (λ y path -> P path) [...], where P : x=x -> Type. But this is a type error as P cannot be applied to path as it is of type x=y, not x=x.

HPSmash77
– HPSmash77

2025年10月24日 12:50:34 +00:00
Commented Oct 24, 2025 at 12:50
Not matching x=x with refl avoids this

HPSmash77
– HPSmash77

2025年10月24日 12:51:06 +00:00
Commented Oct 24, 2025 at 12:51
Is the reasoning in my first comment correct?

HPSmash77
– HPSmash77

2025年10月24日 12:53:33 +00:00
Commented Oct 24, 2025 at 12:53

| Show 2 more comments

How to Edit

Correct minor typos or mistakes
Clarify meaning without changing it
Add related resources or links
Always respect the author’s intent
Don’t use edits to reply to the author

How to Format

create code fences with backticks ` or tildes ~
```
like so
```
add language identifier to highlight code
```python
def function(foo):
print(foo)
```
put returns between paragraphs
for linebreak add 2 spaces at end
_italic_ or **bold**
indent code by 4 spaces
backtick escapes `like _so_`
quote by placing > at start of line
to make links (use https whenever possible)

<https://example.com>

[example](https://example.com)

<a href="https://example.com">example</a>

formatting help »
asking help »

How to Tag

A tag is a keyword or label that categorizes your question with other, similar questions. Choose one or more (up to 5) tags that will help answerers to find and interpret your question.

complete the sentence: my question is about...
use tags that describe things or concepts that are essential, not incidental to your question
favor using existing popular tags
read the descriptions that appear below the tag

If your question is primarily about a topic for which you can't find a tag:

combine multiple words into single-words with hyphens (e.g. python-3.x), up to a maximum of 35 characters
creating new tags is a privilege; if you can't yet create a tag you need, then post this question without it, then ask the community to create it for you

popular tags »