HEq congr

Stream: mathlib4

[Violeta Hernández]

The docstring in docs#HEq mentions

One important non-theorem is the analogue of congr: If HEq f g and HEq x y and f x and g y are well typed it does not follow that HEq (f x) (g y). (This does follow if you have f = g instead.)

Is there an actual counterexample to this? Or is it one of those "morally true but can't be proven" things?

[Violeta Hernández]

(If it's the former, then I'd love to see this added to the counterexamples folder)

[Yury G. Kudryashov]

AFAIR, there is a model of Lean where all types with the same cardinality are equal. Then it's possible that (α → β) = (α → γ) with some functions "accidentally" equal but β ≠ γ.

[Yury G. Kudryashov]

(at least, ZFC doesn't imply that such an example is impossible, even for α = Fin 2)

[Yury G. Kudryashov]

Note: I'm repeating some things I've heard here, without deep understanding of the matter.

[Violeta Hernández]

That makes a lot of sense, thanks!