is a type with parameters injective?

Stream: general

[Scott Buckley]

forgive me for perhaps not using the correct terminology. what i want to know is similar to below:

lemma type_something_injectivity: ∀ {T1 T2:Type} {l1:list T1} {l2:list T2},
  l1 == l2 ->
  T1 = T2
:= begin
  ???
end

Is the above provable?

More specifically, I have some inductive type vexp: forall (T:Type 0), T -> Type 1, and I want to know that vexp T1 v1 == vexp T2 v2 -> T1 = T2 and v1 == v2

does this make sense?

[Mario Carneiro]

Yes it makes sense to ask this question, and the answer is that it is usually independent in lean and sometimes provably false

[Mario Carneiro]

import logic.function

inductive noninj (T : set Type) : Type
| mk : noninj

example : ¬ (∀ x y, noninj x = noninj y → x = y) :=
function.cantor_injective _

[Scott Buckley]

I thought that may be the case, however I couldn't understand why, but your example makes it clear. Thanks very much! :)