Zulip Chat Archive

Stream: new members

Topic: Prove types unequal

Kevin Sullivan (Mar 07 2019 at 14:48):

How to prove, e.g., neq nat string?

Patrick Massot (Mar 07 2019 at 14:53):

I'm not sure you can

Jesse Michael Han (Mar 07 2019 at 15:13):

iirc Mario showed that his interpretation of Lean into ZFC + inaccessibles could be modified to identify any two countable types as the same set

Johannes Hölzl (Mar 07 2019 at 15:13):

I think you can only show inequality between types if their cardinality is different

Simon Hudon (Mar 07 2019 at 15:14):

@Johannes Hölzl I would think any property that differs between two types would be sufficient. I have a hard time coming up with another function than cardinality though

Patrick Massot (Mar 07 2019 at 15:16):

Yes this is what I remember from previous iterations of this question

Last updated: Dec 20 2023 at 11:08 UTC