Zulip Chat Archive

Stream: new members

Topic: is "subtype" injective?


view this post on Zulip Kenny Lau (Sep 13 2018 at 19:32):

if {x // p x} = {x // q x}, then is it true that p = q?

view this post on Zulip Chris Hughes (Sep 13 2018 at 19:33):

Pretty sure it's independent unless they're different sizes.

view this post on Zulip Kenny Lau (Sep 13 2018 at 19:36):

great, I just found another independent proposition

view this post on Zulip Kenny Lau (Sep 13 2018 at 19:36):

ZFC 1 : 0 Lean

view this post on Zulip Mario Carneiro (Sep 13 2018 at 19:57):

Lean has loads of independent propositions like this

view this post on Zulip Kenny Lau (Sep 13 2018 at 19:57):

ZFC aleph[0] : 0 Lean

view this post on Zulip Mario Carneiro (Sep 13 2018 at 19:57):

Equality of types is essentially "freely generated"; unless it's obviously true it's probably independent

view this post on Zulip Mario Carneiro (Sep 13 2018 at 19:58):

of course there is a whole cottage industry built around alternative models that fit in this gap (see: HoTT)

view this post on Zulip Mario Carneiro (Sep 13 2018 at 20:00):

the distance from axioms to independent statements is very short in lean:

inductive A. inductive B.
example : A = B := independent

view this post on Zulip Kenny Lau (Sep 13 2018 at 20:00):

wait what

view this post on Zulip Kenny Lau (Sep 13 2018 at 20:00):

well I suppose it makes sense

view this post on Zulip Kenny Lau (Sep 13 2018 at 20:01):

so we can essentially have two copies of empty and nobody will notice

view this post on Zulip Kenny Lau (Sep 13 2018 at 20:01):

also is there any way to create an inductive type?

view this post on Zulip Kenny Lau (Sep 13 2018 at 20:01):

inside a proof?

view this post on Zulip Kenny Lau (Sep 13 2018 at 20:01):

i.e. how much does Lean itself know about inductive types?

view this post on Zulip Mario Carneiro (Sep 13 2018 at 20:02):

oh wait, I forgot to define equality

prelude
inductive A. inductive B.
inductive eqA : Type → Type | refl : eqA A
example : eqA B := independent

view this post on Zulip Kenny Lau (Sep 13 2018 at 20:02):

lol

view this post on Zulip Mario Carneiro (Sep 13 2018 at 20:03):

inductive types in lean are essentially an axiom schema

view this post on Zulip Mario Carneiro (Sep 13 2018 at 20:04):

you have to write down the type specification, and then poof appears a new type constant

view this post on Zulip Mario Carneiro (Sep 13 2018 at 20:04):

so they only work at the top level

view this post on Zulip Kenny Lau (Sep 13 2018 at 20:04):

I see

view this post on Zulip Mario Carneiro (Sep 13 2018 at 20:05):

although you can always define a very general type and then narrow it down from inside a definition, i.e. defining a particular subtype of sigma of W type of whatever rather than writing a new inductive type


Last updated: May 16 2021 at 05:21 UTC