## Stream: general

### Topic: is a type with parameters injective?

#### Scott Buckley (May 02 2018 at 14:02):

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 (May 02 2018 at 15:28):

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 (May 02 2018 at 15:30):

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 (May 03 2018 at 01:38):

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

Last updated: May 18 2021 at 16:25 UTC