## Stream: new members

### Topic: is "subtype" injective?

#### Kenny Lau (Sep 13 2018 at 19:32):

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

#### Chris Hughes (Sep 13 2018 at 19:33):

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

#### Kenny Lau (Sep 13 2018 at 19:36):

great, I just found another independent proposition

ZFC 1 : 0 Lean

#### Mario Carneiro (Sep 13 2018 at 19:57):

Lean has loads of independent propositions like this

#### Kenny Lau (Sep 13 2018 at 19:57):

ZFC aleph[0] : 0 Lean

#### Mario Carneiro (Sep 13 2018 at 19:57):

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

#### 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)

#### 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

wait what

#### Kenny Lau (Sep 13 2018 at 20:00):

well I suppose it makes sense

#### Kenny Lau (Sep 13 2018 at 20:01):

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

#### Kenny Lau (Sep 13 2018 at 20:01):

also is there any way to create an inductive type?

inside a proof?

#### Kenny Lau (Sep 13 2018 at 20:01):

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

#### 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

lol

#### Mario Carneiro (Sep 13 2018 at 20:03):

inductive types in lean are essentially an axiom schema

#### Mario Carneiro (Sep 13 2018 at 20:04):

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

#### Mario Carneiro (Sep 13 2018 at 20:04):

so they only work at the top level

I see

#### 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