Is the hierarchy fixed?

Stream: Type theory

[Mr Proof]

From spending a bit of time in Lean, and thinking about the pros and cons. One thing I notice was that Prop:Type doesn't make much sense to me any more than having Type:Prop
From my point of view Prop and Type are two universes, one not a type of the other. Is this just a design decision or is there any practical reason for it.
My preferred scheme would have been:

Prop:Universe0
Type:Universe0
Universe0:Universe1:..etc.

(This pretty much amounts to making Prop:Type1 instead of Prop:Type0.) Also probably a better name for "Type" would be "Data" since it is just the type of mathematical data like numbers etc. Having one of the types in type theory being called Type is a bit silly if you think about it.
Pros
The pro's of this scheme is a lot of terms are simplified. e.g. Instead of:
rfl.{u} {α : Sort u} {a : α} you could write rfl {α : Universe0} {a : α} as most of the time you only care about Prop and Type types anyway and not the higher universes. It makes the Curry-Howard correspondence a bit simpler for Prop and Type since these are just two types of the same Universe.
Cons
It would take a bit more typing to reason about higher universes. But probably wouldn't be needed for most mathematical tasks besides category theory.

My second point is that having all the math types having the same type "Type" seems a bit like a wasted opportunity. For example, why not have the number fields like Nat and Complex have the type Field, the topology types as Spaces and so on. Wouldn't this make it easier to do categorical comparisons? There is a paper here about what to do about things that have more than one category. Instead we do this this with the [Field] in the square brackets. You could have dependent categories like Commutative(±1) for (anti-) commutative fields.

So basically I'm wondering how much of this hierarchy is a design decision and how much is fundamental to how type theory works?

BTW. This is just for curiosity, I'm not expected anyone to go back and rewrite Lean!

[Eric Wieser]

This might be more suited to the #Type theory stream; want me to move it there? (I'll leave the notification message here so people still find it)

[Notification Bot]

This topic was moved here from #maths > Is the hierachy fixed? by Eric Wieser.

[Mario Carneiro]

There is a lot of flexibility in how you can set up a universe hierarchy. Basically any directed acyclic graph with no maximal element will do

[Mario Carneiro]

It just so happens that the simplest such hierarchy is the natural numbers

[Mario Carneiro]

The pro's of this scheme is a lot of terms are simplified. e.g. Instead of:
rfl.{u} {α : Sort u} {a : α} you could write rfl {α : Universe0} {a : α} as most of the time you only care about Prop and Type types anyway and not the higher universes.

This is basically saying not to use universe parametricity, which is problematic if you ever want to make use of those other types and find out after the fact that half of the library needs to be rewritten

[Mario Carneiro]

I don't see any reason why Prop : Type can't be true by your reading though. Why not think of Prop as a data type as well, if it's basically Bool with extra steps?

[Mario Carneiro]

on a reading that things are in Type if they are "small", Prop should also be in there

[Mario Carneiro]

In particular, having Prop in a higher universe means that Nat : Type but Set Nat : Type 1 because Set Nat := Nat -> Prop and Prop is "large" now

[Mario Carneiro]

so if we put those things together we observe that rfl doesn't prove equality of sets anymore!

[Mario Carneiro]

For example, why not have the number fields like Nat and Complex have the type Field, the topology types as Spaces and so on.

We actually have this in mathlib as well, these types are usually used as categories, such as docs#RingCat . It turns out to be more convenient not to use this unless we are explicitly working with the category though, because Int (the type) has to have one type, so it can't be RingCat and AddGroupCat at the same time. That means we really have intRing : RingCat such that intRing.carrier = Int, but now we have to be able to infer intRing given Int. This leads to a completely different library design known as "canonical structures", which is possible to do but very different from the typeclass approach

[Mr Proof]

It works just as well if you have Type:Prop it seems

[Mario Carneiro]

No, that one is inconsistent actually

[Mario Carneiro]

because then Type would be a proposition and all elements of it would be equal by proof irrelevance, so Unit = Empty and so you can prove false

[Mario Carneiro]

Classically Prop is really quite a small type, with only space for two distinct elements, not nearly enough to host a whole universe of data types

[Mr Proof]

What would happen if you had two distinct families:

Prop: Prop 1 :Prop 2: Prop 3:...
Type: Type 1: Type 2: Type 3:...

Is that ruled out I wonder?

[Mario Carneiro]

No, in fact this is the setup used in Agda (as I mentioned there is a lot of flexibility and different provers do different things)

[Mario Carneiro]

Actually I take it back, there are two hierarchies in Agda but you have Prop i : Type (i+1)

[Luigi Massacci]

Mr Proof said:

What would happen if you had two distinct families:

Prop: Prop 1 :Prop 2: Prop 3:...
Type: Type 1: Type 2: Type 3:...

Is that ruled out I wonder?

This is what Agda does: https://agda.readthedocs.io/en/v2.6.0/language/prop.html

[Mr Proof]

Well, my argument would be. If you are taking the time to define Set, is it much more work to add a SetRfl? Or does it all have to be added at the beginning for the whole hierachy?

[Mario Carneiro]

I'm not sure what you mean by Set and SetRfl there

[Mr Proof]

Well, you said rfl wouldn't cover the case of Set as that would be Type 1. But can't you just add another rfl when defining sets to cover that case?

[Mario Carneiro]

Are you saying that we should redefine rfl every time we need another universe?

[Mr Proof]

Not redefine. Just add an extra case

[Mario Carneiro]

that means that the first person who finds they need to use Type 2 for some reason would have to copy paste the whole standard library, otherwise nothing would be usable for it

[Mario Carneiro]

and if you copy paste equality then you will also have to copy paste all the tactics that use equality

[Trebor Huang]

How is Prop 1 : Prop 2 consistent? Surely True is not equal to False?

[Trebor Huang]

Agda has Prop i : Type (i+1) to be more accurate

[Trebor Huang]

whoops my zulip missed some messages randomly initially, it's already answered by Mario