Two universe levels

Stream: maths

[Thomas Eckl]

How do you debug code (guess what I want to define in HoTT) producing the following error message:

type mismatch at application
  is_open (pred_to_sset (λ (t : ↥T), exists_elem (λ (B : ↥𝒫 T), B∈S and t∈B)))
term
  pred_to_sset (λ (t : ↥T), exists_elem (λ (B : ↥𝒫 T), B∈S and t∈B))
has type
  hott.subset.Subset.{(max ?l_1 ?l_2)
    (max (max ?l_1 ?l_2) ((max ?l_1 ?l_2)+1) (max ?l_3 ((max ?l_1 ?l_2)+1)) ?l_1 ?l_2)}
    T : Type (max
        (max ?l_1 ?l_2)
        ((max (max ?l_1 ?l_2) ((max ?l_1 ?l_2)+1) (max ?l_3 ((max ?l_1 ?l_2)+1)) ?l_1 ?l_2)+1))
but is expected to have type
  hott.subset.Subset.{(max ?l_1 ?l_2) (max ?l_1 ?l_2)} T : Type ((max ?l_1 ?l_2)+1)

It seems that only the universe levels but not the type themselves don't coincide. But first of all I don't understand why several universe levels are attached to types. Where do they come from? How are they resolved? So second, what has gone wrong?
I am looking for general strategies, and maybe documentation for the universe handling.

[Reid Barton]

First I would check whether what I think I'm doing actually makes sense, and whether existing definitions have the universe levels I expect

[Reid Barton]

here it looks like one of these will uncover a problem, since the universe levels you have are not just not the same but in fact definitely different

[Reid Barton]

because you have (max ?l_1 ?l_2) appearing in the expected type, but something that's at least (max ?l_1 ?l_2)+1 in the actual type.

[Reid Barton]

Thomas Eckl said:

Where do they come from? How are they resolved? So second, what has gone wrong?

They come from things like {X : Type*} or universe u, X : Type u. They're resolved by unification or by being specified explicitly using the foo.{u v} notation that appears in the error message. Hard to guess what specifically is wrong without seeing the code.

I am looking for general strategies, and maybe documentation for the universe handling.

This doesn't really qualify as a strategy, but set_option pp.universes true together with #checking the definitions involved is a good start.

[Reid Barton]

B : ↥𝒫 T

I'm guessing this means B : T -> hProp and that hProp also has a universe parameter, and it's not clear to me who is choosing it or what the correct choice is. I would start by trying to figure out the universe levels of everything by hand.

[Mario Carneiro]

But to be clear, the problem here has nothing to do with the universes. To first order you can just ignore all universe arithmetic and focus on the types, which don't match in this error message

[Reid Barton]

Aren't they both Subset T?

[Mario Carneiro]

Oh, so they are

[Mario Carneiro]

I thought the first one was just T, ignore me

[Mario Carneiro]

It seems that Subset T has a free universe parameter, which is usually the source of the problem

[Mario Carneiro]

What is the definition of Subset?

[Reid Barton]

I'm guessing it's a bundled subset, the first universe level argument is the universe of T and the second is the universe of the hProp that cuts out the subset

[Reid Barton]

pred_to_sset is the constructor for a bundled subset, T is a bundled topological space

[Reid Barton]

and I think there is potentially some kind of predicativity issue with the definition of the subset

[Mario Carneiro]

The pervasive appearance of max ?l_1 ?l_2 is also worrisome, it probably means that a definition has an unnecessary universe argument

[Reid Barton]

yeah, my guess is ?l_1 is the universe level of the underlying type of T and ?l_2 is the level of the hProp in is_open

[Reid Barton]

I have no idea whether it's correct to have one or two universe levels in the definition of a topological space... universe sizes for propositions hurts my head a bit

[Mario Carneiro]

I don't think so, after all Subset's first argument is max ?l_1 ?l_2

[Reid Barton]

oh good point

[Reid Barton]

Maybe something earlier is indeed wrong then

[Reid Barton]

Anyways, that +1 has me worried

[Reid Barton]

I think the definition of this subset has to quantify over (what I assume is the basis) S and not over all subsets of T

[Mario Carneiro]

I don't actually know the context here

[Thomas Eckl]

You are too fast for me ... There is a reason why I didn't want to describe the underlying code - it's rather involved. Subset T is actually a structure, consisiting of a (HoTT) Set, a map from this set to T, and a certificate that this map is injective (which is a (HoTT) Prop in the end. And indeed, Set and Prop have a free universe parameter for the underlying type.

[Mario Carneiro]

Anything you can post is better than nothing

[Mario Carneiro]

staring at an error message without knowing the signature of the definition or the surroundings is harder than you might think

[Mario Carneiro]

in any case I'm not about to go get the hott repo so I'm not to bothered about making it compile

[Mario Carneiro]

in particular, I would like to see the complete def that sourced this error

[Mario Carneiro]

Anyway these error messages will be much clearer if you put in actual universe parameters instead of unification variables. Then lean will be able to simplify things like (max (max ?l_1 ?l_2) ((max ?l_1 ?l_2)+1) to just u+1, and the problem may actually go away entirely

[Reid Barton]

What are the types of T and S, with universe parameters included?

[Thomas Eckl]

OK, I finally managed to wrestle enough time from teaching to figure this out:

The problem is as described in the HoTT book, 3.5 and 10.1.3/4: If A : Type u is a type in the universe u then the type of predicates A -> Prop.{u}, feeding elements of A into propositions in the universe u, is in the universe u+1. If you interpret this type of predicates as the power set of A (assuming that A is a HoTT set) and build predicates on this power set, you will end up in universe u+2.

[Thomas Eckl]

The problem can be resolved by propositional resizing, see the HoTT book, 3.5. This is good news for me because propositional resizing Prop.{u+1} -> Prop.{u} can be constructed from the Law of the Excluded Middle in the universe u+1 (HoTT book, Ex.3.10) and ultimately from the Axiom of Choice, using Diaconescu's Theorem (HoTT book, Thm.10.1.14). And I have no qualms to assume these axioms ...

[Thomas Eckl]

As an aside to HoTT 3 - savvy people: I am actually not able to type Prop.{u+1} but always need to use trunctype.{u} -1 - annoying. Set.{u} works however - strange.