Universe polymorphism across Type and Prop

Stream: lean4

[Julien Marquet-Wagner]

I want to formalize some category theory.
The thing is, I chose to let my categories have their objects in Sort u, which means they can be Props.
Now, to formalize the Grothendieck construction, I need a Sigma type. Unfortunately, Sigma and PSigma either don't accept the right universes or don't live in the right universe for my purpose.
So I tried to write another variant of Sigma types, and after figuring out I need to set_option bootstrap.inductiveCheckResultingUniverse false I'm stuck here:

set_option bootstrap.inductiveCheckResultingUniverse false in
inductive MySigma.{u} (α : Sort u) (β : α → Sort u) : Sort u where
| mk (a : α) (b : β a)
-- (kernel) invalid reference to undefined universe level parameter 'u'

This can be reduced to a smaller example:

set_option bootstrap.inductiveCheckResultingUniverse false in
inductive MyFooBar (α : Sort u) : Sort u where
| mk (a : α) : MyFooBar α
-- (kernel) invalid reference to undefined universe level parameter 'u'

However, the following works:

set_option bootstrap.inductiveCheckResultingUniverse false in
inductive MyBazz (α : Sort u) : Sort u where
| mk : MyBazz α

Why does Lean do that?

[Julien Marquet-Wagner]

I might get asked so here is:

lean --version
Lean (version 4.16.0-pre, x86_64-unknown-linux-gnu, commit 9b2c8287b12a, Release)

[Floris van Doorn]

Why do you want MySigma to sometimes live in Prop? In previous versions of Lean such inductive sorts were allowed, but generate only a recursion principle eliminating to Prop (they wouldn't have so-called "large elimination"). Having large elimination for such inductive sorts would be inconsistent in general.
Apparently we now just disallow this behavior, to avoid that footgun, and place such inductive types always in Type _, which is what PSigma does. Why isn't that sufficient for your purposes?

[Edward van de Meent]

for more info, you can read ref4#prop-vs-type

[Eric Wieser]

This is the closed lean4#3310, where Sebastian Ullrich says:

bootstrap comes without warranty :)

[Julien Marquet-Wagner]

Let's say I write

universe u v
structure Category : Type (max u v) where
  obj : Sort u
  hom : obj → obj → Sort v
  -- [...]

The beginning of the problem is that obj and hom may live in Prop. I initially did that because I wanted to be able to say that a poset is a category where hom is a Prop.

And then I want to have a Grothendieck construction, so something that takes a functor F : C ⇒ Cat to a category ∫ F.
In practice, I use use Displayed Categories rather than a functor C ⇒ Cat:

structure Category.Displayed (C : Category.{u,v}) : Type (max u v) where
  obj : C.obj → Sort u
  hom : {a b : C.obj} → obj a → obj b → (a ⟶ b) → Sort v
  -- [...]

Then the Grothendieck construction should be

total_category : {C₀ : Category.{u,v}} → (C : Category.Displayed C₀) → Category.{u,v}

Now, how do I define (total_category C).obj? I want it to be (a₀ : C₀.obj) × (C.obj a₀) which has to be Type u, from the signature of total_category.
This would work right away if I had obj live in Type. But my initial choice was to have obj : Sort u, which means I need a variant of Sigmathat is polymorphic across all of Sort u, for all u.

[Eric Wieser]

Can you explain why PSigma doesn't work for you?

[Julien Marquet-Wagner]

Because PSigma : {α : Sort u} → (β : α → Sort v) → Type (max 1 u v)
I would need {α : Sort u} → (β : α → Sort v) → Sort (max u v)...

[Julien Marquet-Wagner]

I guess the morality of the story is that this kind of aggressively polymorphic functions was never an intended use case of Lean :laughing: and admittedly it's not a very important issue.

[Floris van Doorn]

Is there an issue if the type of total_category is

total_category : {C₀ : Category.{u,v}} → (C : Category.Displayed C₀) → Category.{max 1 u,max 1 v}

? (perhaps with one fewer max 1?)

[Floris van Doorn]

Having objects and homs of a category live in Sort u is perhaps useful. Of course, even if you choose Type u, you can still use docs#PLift to lift Sort u to Type u (and in particular Prop to Type).

[Markus Himmel]

@Julien Marquet-Wagner, #new members > ✔ Universe Restriction on CategoryTheory.Category @ 💬 might be an interesting read for you.

[Julien Marquet-Wagner]

Floris van Doorn said:

Is there an issue if the type of total_category is

total_category : {C₀ : Category.{u,v}} → (C : Category.Displayed C₀) → Category.{max 1 u,max 1 v}

? (perhaps with one fewer max 1?)

I'd say yes, it would be an issue, because the max 1 u breaks the universe combinatorics of the definition: with the definitions I gave of Category and Category.Displayed, the total category always live in the same universes as the base category.

[Julien Marquet-Wagner]

The choice I made in my project is that I preferred nice combinatorics above Prop-genericity.

[Julien Marquet-Wagner]

@Markus Himmel Interesting read indeed, thanks for the link!

[Julien Marquet-Wagner]

I'm just thinking: is the invalid reference to undefined universe level parameter 'u' message a sign of a kernel bug?

[Julien Marquet-Wagner]

I guess not, since Sebastian Ullrich seemed not concerned at all about it in lean4#3310, but I still find that message surprising

[Floris van Doorn]

I think it's fair to say that this option is not "officially supported".
Please note that if this bug were to be fixed, the resulting type would be absolutely useless for you: you wouldn't be able to define the projections or do anything with it that is not proving a proposition. This type doesn't have large elimination, so it can only be used to prove propositions (enabling large elimination is inconsistent).