function.combine

Stream: lean4

[Kevin Buzzard]

It was pointed out on the Discord that docs4#Function.combine is not as universe polymorphic as one might expect, because of this line. Is this intentional (some sort of monad-related reason or something?)

[Mario Carneiro]

this is why I don't like variable

[Mario Carneiro]

in the context of combine it doesn't seem intentional

[Mario Carneiro]

is it like this in mathlib3?

[Eric Wieser]

Yes (edit: but in lean3 core, docs#function.combine)

[Eric Wieser]

I don't think variable is the culprit here; I would guess someone copied and pasted types and got fed up of writing universe variables.

[Eric Wieser]

At least in Lean3 you could write variables {A B C D E : Type*} and have it do the right thing; in lean 4 you have to deal with the fact that two types may accidentally be assigned the same universe

[Kyle Miller]

Here's a PR to change that subscript in the universe variable: mathlib4#4474

[Kyle Miller]

It only affects Function.combine

[Kyle Miller]

This ζ : Sort u₁ was also present in Lean 3 (in core)

[Kevin Buzzard]

Indeed it was discovered in Lean 3 and then it was noted that it had been carefully ported to Lean 4 :-)

[Notification Bot]

22 messages were moved from this topic to #lean4 > Unwanted universe metavariables by Eric Wieser.