Is the congr analogue for HEq false or just simply unprovabl

Stream: lean4

[metakuntyyy]

From the docs:

One public important non-theorem is the analogue of [congr](https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#congr): If f ≍ g and x ≍ y and f x and g y are well typed it does not follow that One public important non-theorem is the analogue of congr: If f ≍ g and x ≍ y and f x and g y are well typed it does not follow that f x ≍ g y. (This does follow if you have f = g instead.) However if a and b have the same type then a = b and a ≍ b are equivalent.. (This does follow if you have f = g instead.) However if a and b have the same type then a = b and a ≍ b are equivalent.

This makes me wonder if you can actually prove that HEq congr is false? Do there exist f,g that are HEq and x and y that are HEq such that f x ≍ g y is false? Or is it simply undecidable and you can't prove either statement.

[Aaron Liu]

You can't prove it's true and you can't prove it's false

[Aaron Liu]

unless Lean's type theory is inconsistent in which case you can do both

[metakuntyyy]

Do you have any reference of the undecidability? I couldn't find anything.

[Aaron Liu]

There was a thread I'll see if I can find it

[Kenny Lau]

@metakuntyyy there's no need to complicate everything, it boils down to the fact that ((α → β) = (α → γ)) → (β = γ) is independent of Lean, and the way to understand it is "I can't prove it", or "I could come up with a way to assign types so that it's true, and another way so it's false"

[metakuntyyy]

Thanks. I figured that it's independent. There was a topic that discussed that Nat = Int is undecidable because there are two models in which one is true and the other one is false. I don't remember the details of it but surely the same assignment could be done for HEq.

Why I'm asking is I worked with some API regarding cycles and I stumbled upon heterogeneous recursors, which made me wonder how important that concept is. I think the main use is that it makes certain definitions possible. This is the definition in question https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/List/Cycle.html#Cycle.next. I assume it's to deal with dependent functions and to be more flexible.

[Kevin Buzzard]

An argument that's good enough for me is "if Mat=Int is independent then surely this more complicated thing is"