## Stream: general

### Topic: universe max

#### Kenny Lau (Jul 12 2019 at 07:35):

example : (Type (max u v) ≃ Type u) ⊕ (Type (max u v) ≃ Type v) := sorry


#### Kenny Lau (Jul 12 2019 at 07:35):

Is this provable?

#### Floris van Doorn (Jul 12 2019 at 07:53):

I don't know, but if it is provable it's going to be tricky, since you cannot case on u <= v. Maybe there is a model where max u v is interpreted as some other function than max(u,v), growing more quickly?

e.g. max(u,v)+1

#### Mario Carneiro (Jul 12 2019 at 15:05):

It's not provable. The structure of universe levels is a very weak subtheory of PA; since there is no induction all the facts you get about general variables have to be given to you at the start. In short: if it's not obviously true, it's false

#### Mario Carneiro (Jul 12 2019 at 15:07):

In fact it's not even necessarily totally ordered, which gives a simple counterexample

#### Keeley Hoek (Jul 13 2019 at 03:47):

I know I've kind-of asked this before, but why would anyone want type theory to be like this? Is it just because extras (e.g. universes basically being nat) isn't needed in the bare-minimum you need to make everything work?

#### Mario Carneiro (Jul 13 2019 at 18:20):

It genuinely makes the theory axiomatically stronger. The problem with just adding these things is that there is always another meta level. The whole point of universes in the first place is that you get a type that can act as a meta theory over the first universe, and another one after that, "and so on". If you start taking that structure too seriously you will want to get a meta level above that, and the theory will become more complicated and powerful still and you still won't be happy because there are now more things that you can say but not prove.

#### Kevin Buzzard (Jul 13 2019 at 20:05):

Remember -- we only even have universes because Type in Type is inconsistent :-) Let's not take them too seriously.

Last updated: May 17 2021 at 22:15 UTC