## Stream: new members

### Topic: Inductive decls

#### Keeley Hoek (May 31 2019 at 08:00):

Why is it illegal to declare

inductive foo
| mk (f : foo → ℕ)


#### Keeley Hoek (May 31 2019 at 08:01):

whereas

inductive foo'
| mk (f : ℕ → foo')


is fine?

#### Keeley Hoek (May 31 2019 at 08:01):

Is there an (easy?) proof of false?

#### Edward Ayers (May 31 2019 at 08:23):

I think the first problem is that it's not clear what the recursor should be.

#### Kenny Lau (May 31 2019 at 08:24):

yeah I was thinking about that.

#### Edward Ayers (May 31 2019 at 08:25):

And then all of the sensible definitions of rec let you make infinite descending terms. edit: or derive false or something.

#### Edward Ayers (May 31 2019 at 08:27):

The thing to look up is called "strict positivity"

#### Rob Lewis (May 31 2019 at 08:32):

constant foo : Type
constant mk {α} (f : foo → α) : foo
constant inj {α} : Π x : foo, {f : foo → α // x = mk f}

noncomputable def self_app {α} (a : foo) : α :=
let ⟨f, hf⟩ := inj a in f a

noncomputable def ta {α} (nf : α → α) : α := self_app $mk$ λ a, nf $self_app a example : false := ta id  #### Keeley Hoek (May 31 2019 at 08:42): Awesome! Thanks for the demo. If I make mk increase universe level by one the demo fails; universe u constant foo : Type u constant mk {α} (f : foo.{u} → α) : foo.{u + 1} constant inj {α} : Π x : foo, {f : foo → α // x = mk f} noncomputable def self_app {α} (a : foo) : α := let ⟨f, hf⟩ := inj a in f a noncomputable def ta {α} (nf : α → α) : α := self_app$ mk $λ a, nf$ self_app a

example : false := ta id


Am I safe now? If so, is there any way to make lean build this?

#### Rob Lewis (May 31 2019 at 08:58):

universe u

constant foo : Type u
constant mk {α} (f : foo.{u} → α) : foo.{u + 1}
constant inj {α} : Π x : foo, {f : foo → α // x = mk f}

noncomputable def self_app {α} (a : foo) : α :=
let ⟨f, hf⟩ := inj (mk $λ _, trivial) in f a noncomputable def ta {α} (nf : α → α) : α := self_app$ mk $λ a, nf$ self_app a

example : false := ta id


#### Keeley Hoek (May 31 2019 at 09:27):

Actually, I'm not quite sure I understand---why is \alpha free to vary in those axioms? If I force \alpha to be \nat, can it work?

#### Mario Carneiro (May 31 2019 at 09:30):

the short answer is "no, this type violates cantor's theorem"

#### Mario Carneiro (May 31 2019 at 09:35):

I agree that something is funny in Rob's example. We don't need ta, it's already a contradiction in self_app if we instantiate alpha as false

#### Mario Carneiro (May 31 2019 at 09:36):

and also self_app isn't diagonalizing in the second version

#### Rob Lewis (May 31 2019 at 09:37):

Yeah, I just copied it from the StackOverflow answer, I'm sure there are shorter ways.

#### Mario Carneiro (May 31 2019 at 09:38):

I would guess that you are actually safe if mk bumps the universe, but this is not the sort of definition lean can handle. It's recursive in a weird way - foo.{n+1} is defined in terms of foo.{n}

#### Mario Carneiro (May 31 2019 at 09:41):

Rob, I think that inj is not a reasonable axiom - if you just look at inj it says foo -> foo -> A for all A

#### Rob Lewis (May 31 2019 at 09:41):

Oh, wait, I see what you're saying.

#### Rob Lewis (May 31 2019 at 09:41):

Heh, we just had our coffee break and it's kicking in now.

#### Rob Lewis (May 31 2019 at 09:43):

You're right, that's too strong. But I'm not convinced that bumping the universe saves you, could you explain?

#### Mario Carneiro (May 31 2019 at 09:44):

you have to have a fixed alpha, like Keeley says

#### Mario Carneiro (May 31 2019 at 09:44):

right now you can use mk with one alpha and inj with another - and that's actually what you are doing in the proof, you use mk with true and inj with false

#### Mario Carneiro (May 31 2019 at 09:45):

Imagine you could just define foo.{u+1} := foo.{u} -> nat, that would satisfy all the axioms

#### Mario Carneiro (May 31 2019 at 09:46):

it's not really recursive, since for each fixed u it's a finite number of arrows

#### Mario Carneiro (May 31 2019 at 09:47):

in fact such a type probably even exists, since Set.{u} grows faster than foo.{u}

#### Mario Carneiro (May 31 2019 at 09:54):

Thinking about it more carefully, I think this is not definable. If it was, then we could define level.{u} : nat which is equal to u as a nat

#### Mario Carneiro (May 31 2019 at 09:56):

Set.{u} almost lets you define level, but you can only guarantee u or more inaccessible cardinals in it. There is a sort of cardinal collapsing property here - the theory can't tell if you just take one of the Type u universes out and shift the indexes of everything else down

#### Keeley Hoek (May 31 2019 at 09:57):

Looking at Set more than I have before, it seems like the way to get around having a foo -> Prop is choosing an indexing type \alpha and looking at maps \alpha -> foo instead. Since you can choose the indexing type as large as you want, isn't there some sort of bijection between these two pieces of data?

#### Mario Carneiro (May 31 2019 at 09:58):

that's why Set lives in a higher universe

#### Keeley Hoek (May 31 2019 at 09:58):

(modulo a quotient of such maps by permutations of the indexing type and change of indexing type)

#### Mario Carneiro (May 31 2019 at 09:58):

you can't instantiate Set.{u} with Set.{u} as the index type

For sure

#### Mario Carneiro (May 31 2019 at 10:01):

so you don't get a cantor contradiction, instead you just end up proving that Set.{u} is (a lot) smaller than Set.{u+1}

#### Keeley Hoek (May 31 2019 at 12:21):

Regarding your comments on level, why would it be bad if level.{u} : nat existed?

#### Keeley Hoek (May 31 2019 at 12:21):

(Sorry for using you to learn about type theory)

(deleted)

#### Mario Carneiro (May 31 2019 at 19:09):

@Keeley Hoek It wouldn't necessarily be bad if level.{u} existed, but I'm pretty sure it's independent

#### Floris van Doorn (May 31 2019 at 19:10):

(oops, I replied to the wrong thread)

Last updated: May 14 2021 at 07:19 UTC