Zulip Chat Archive

Stream: general

Topic: is a type with parameters injective?


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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 _

view this post on Zulip 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