Injectivity of arrow type constructor

Stream: Is there code for X?

[Alex Keizer]

Is the following provable (in Lean 4)?

example {α β β' : Sort _} [Inhabited α] :
    (α → β) = (α → β') → β = β' :=
  by
    intro h;
    sorry

Intuitively, it seems like it should be true, if every function into \beta can be cast to a function into \beta', and vice-versa, the types should have exactly the same inhabitants, right? Can I prove that in Lean 4?

[Reid Barton]

It is not provable.

[Patrick Massot]

It's actually much worse than "not provable". It's not a good question in the flavor of type theory that Lean (or Coq) is using. If you think that you need this result then there is an important mismatch about the intuition you have of those foundations and the way they are actually meant to be used.

[Yaël Dillies]

Also, this doesn't hold if you replace equalities by equivalences.

example : (ℕ → fin 2) ≃ (ℕ → fin 3) → fin 2 ≃ fin 3 := sorry -- impossible

[Alex Keizer]

Patrick Massot said:

It's actually much worse than "not provable". It's not a good question in the flavor of type theory that Lean (or Coq) is using. If you think that you need this result then there is an important mismatch about the intuition you have of those foundations and the way they are actually meant to be used.

To be fair, my intuition did feel like it might be reaching the edge of what I can answer in Lean, hence me asking whether it's provable.
I'm not interested in this result per se, It just seemed very useful while trying to prove the following congruence lemma

theorem heq_congr_fun {α β β' : Type u} {f : α → β} {f' : α → β'} (a : α) :
    HEq f f' → HEq (f a) (f' a) :=
  by
    intro h;
    sorry

Luckily, there was some #XY going on, and I found another way to prove my end-goal that doesn't need the congruence after all.

[Reid Barton]

I think it was not really "luck".

[Floris van Doorn]

I agree with Reid that usually when you need a result like that, you've already gone in a wrong direction before.
Your statement of heq_congr_fun is also not provable in Lean, since it implies your original example (at least for inhabited β).
You need to also assume β = β' to make heq_congr_fun provable: https://github.com/leanprover/lean2/blob/8072fdf9a0b31abb9d43ab894d7a858639e20ed7/library/logic/cast.lean#L28

[Alex Keizer]

Yeah, in my case β = β' does in fact hold, which is how I made it work. Thanks for pointing out where to look!

[Reid Barton]

In general, if x : a and y : b, a HEq x y is not useful unless you can already prove that a = b.

[Eric Rodriguez]

huh? docs#type_eq_of_heq

[Kyle Miller]

Yeah, I'm not sure what Reid is referring to -- part of HEq is that the types of the two terms are equal. If there's a rule, I think it's that HEq is not useful unless you can somehow use the type equality to substitute out one type for another everywhere.

The heq version of congr_arg works, for example (but you need to have a more complicated dependent type for the function):

-- Lean 3
theorem heq_congr_arg {α α' β : Type*} {f : Π {α : Type*}, α → β} (a : α) (a' : α') :
  a == a' → f a = f a' :=
begin
  intro he,
  cases he,
  refl
end

[Reid Barton]

I mean just knowing a = b is not useful except in a situation like a = C i, b = C j, and you have a proof of i = j. (Or if a and b are defeq but then you didn't need HEq.)

[Reid Barton]

Like you can derive false from (0 : nat) == (1 : nat), but you can't derive false from (0 : nat) == (1 : int), even though it implies that nat = int.

[Eric Rodriguez]

I mean, it seems pretty sensible to me. If the underlying set is ℕ, and you encode ℤ as {1, -1, 0, 2, -2, 3, -3, ...}, that wouldn't be contradictory at all

[Reid Barton]

Right and that's why, unless you already had a way to prove the types equal, a HEq hypothesis is not useful

[Eric Rodriguez]

Ah, maybe i'm being pedantic but do you mean sort of "how" they are equal? Whether the encoding is id or whatever

[Reid Barton]

I'm pretty sure I still mean what I said the first time: h : x == y is only ever useful if, without using h, you can already prove a = b

[Reid Barton]

However, this isn't meant to be a metatheorem, just an observation based on experience.

[Reid Barton]

Eric Rodriguez said:

Ah, maybe i'm being pedantic but do you mean sort of "how" they are equal? Whether the encoding is id or whatever

It is somehow related to this because there is only a very limited set of ways to prove that two types are equal.

[David Wärn]

Reid Barton said:

I'm pretty sure I still mean what I said the first time: h : x == y is only ever useful if, without using h, you can already prove a = b

Just to elaborate on this point: h : x == y really means we have e : a = b (where x : a and y : b) together with h' : eq.rec a e = b. In general, if we don't know what e is, then we have no way to determine eq.rec a e, so h' isn't really useful. On the other hand, for any 'concrete' proof e' : a = b, we can evaluate eq.rec a e' explicitly. And eq.rec a e' = eq.rec a e by proof irrelevance. So in this case h' actually tells us something useful, namely that eq.rec a e' = b.