universe max

Stream: general

[Kenny Lau]

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

[Kenny Lau]

Is this provable?

[Floris van Doorn]

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?

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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

[Keeley Hoek]

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]

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]

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