is "subtype" injective?

Stream: new members

[Kenny Lau]

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

[Chris Hughes]

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

[Kenny Lau]

great, I just found another independent proposition

[Kenny Lau]

ZFC 1 : 0 Lean

[Mario Carneiro]

Lean has loads of independent propositions like this

[Kenny Lau]

ZFC aleph[0] : 0 Lean

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

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

[Kenny Lau]

wait what

[Kenny Lau]

well I suppose it makes sense

[Kenny Lau]

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

[Kenny Lau]

also is there any way to create an inductive type?

[Kenny Lau]

inside a proof?

[Kenny Lau]

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

[Mario Carneiro]

oh wait, I forgot to define equality

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

[Kenny Lau]

lol

[Mario Carneiro]

inductive types in lean are essentially an axiom schema

[Mario Carneiro]

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

[Mario Carneiro]

so they only work at the top level

[Kenny Lau]

I see

[Mario Carneiro]

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