## Stream: maths

### Topic: Two universe levels

#### 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), 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 (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

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

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

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

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

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

#### Reid Barton (Nov 04 2020 at 20:56):

Aren't they both Subset T?

Oh, so they are

#### Mario Carneiro (Nov 04 2020 at 20:57):

I thought the first one was just T, ignore me

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

#### Mario Carneiro (Nov 04 2020 at 20:58):

What is the definition of Subset?

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

#### Reid Barton (Nov 04 2020 at 20:59):

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

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

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

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

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

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

oh good point

#### Reid Barton (Nov 04 2020 at 21:02):

Maybe something earlier is indeed wrong then

#### Reid Barton (Nov 04 2020 at 21:03):

Anyways, that +1 has me worried

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

#### Mario Carneiro (Nov 04 2020 at 21:03):

I don't actually know the context here

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

#### Mario Carneiro (Nov 04 2020 at 21:05):

Anything you can post is better than nothing

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

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

#### Mario Carneiro (Nov 04 2020 at 21:07):

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

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

#### Reid Barton (Nov 04 2020 at 21:16):

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

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

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

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