Zulip Chat Archive

Stream: maths

Topic: Two universe levels


view this post on Zulip Thomas Eckl (Nov 04 2020 at 20:34):

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), BS and tB)))
term
  pred_to_sset (λ (t : T), exists_elem (λ (B : ↥𝒫 T), BS and tB))
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.

view this post on Zulip Reid Barton (Nov 04 2020 at 20:37):

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

view this post on Zulip Reid Barton (Nov 04 2020 at 20:38):

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

view this post on Zulip Reid Barton (Nov 04 2020 at 20:38):

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.

view this post on Zulip Reid Barton (Nov 04 2020 at 20:51):

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.

view this post on Zulip Reid Barton (Nov 04 2020 at 20:53):

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.

view this post on Zulip Mario Carneiro (Nov 04 2020 at 20:55):

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

view this post on Zulip Reid Barton (Nov 04 2020 at 20:56):

Aren't they both Subset T?

view this post on Zulip Mario Carneiro (Nov 04 2020 at 20:57):

Oh, so they are

view this post on Zulip Mario Carneiro (Nov 04 2020 at 20:57):

I thought the first one was just T, ignore me

view this post on Zulip Mario Carneiro (Nov 04 2020 at 20:57):

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

view this post on Zulip Mario Carneiro (Nov 04 2020 at 20:58):

What is the definition of Subset?

view this post on Zulip Reid Barton (Nov 04 2020 at 20:58):

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

view this post on Zulip Reid Barton (Nov 04 2020 at 20:59):

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

view this post on Zulip Reid Barton (Nov 04 2020 at 20:59):

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

view this post on Zulip Mario Carneiro (Nov 04 2020 at 21:00):

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

view this post on Zulip Reid Barton (Nov 04 2020 at 21:00):

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

view this post on Zulip Reid Barton (Nov 04 2020 at 21:01):

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

view this post on Zulip Mario Carneiro (Nov 04 2020 at 21:01):

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

view this post on Zulip Reid Barton (Nov 04 2020 at 21:01):

oh good point

view this post on Zulip Reid Barton (Nov 04 2020 at 21:02):

Maybe something earlier is indeed wrong then

view this post on Zulip Reid Barton (Nov 04 2020 at 21:03):

Anyways, that +1 has me worried

view this post on Zulip Reid Barton (Nov 04 2020 at 21:03):

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

view this post on Zulip Mario Carneiro (Nov 04 2020 at 21:03):

I don't actually know the context here

view this post on Zulip Thomas Eckl (Nov 04 2020 at 21:05):

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.

view this post on Zulip Mario Carneiro (Nov 04 2020 at 21:05):

Anything you can post is better than nothing

view this post on Zulip Mario Carneiro (Nov 04 2020 at 21:06):

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

view this post on Zulip Mario Carneiro (Nov 04 2020 at 21:07):

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

view this post on Zulip Mario Carneiro (Nov 04 2020 at 21:07):

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

view this post on Zulip Mario Carneiro (Nov 04 2020 at 21:12):

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

view this post on Zulip Reid Barton (Nov 04 2020 at 21:16):

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

view this post on Zulip Thomas Eckl (Nov 20 2020 at 16:18):

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.

view this post on Zulip Thomas Eckl (Nov 20 2020 at 16:24):

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 ...

view this post on Zulip Thomas Eckl (Nov 20 2020 at 16:27):

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.


Last updated: May 06 2021 at 18:20 UTC