category universes again

Stream: maths

[Reid Barton]

@Scott Morrison While updating lean-homotopy-theory to current mathlib I (or actually lean) noticed that the current formula for the universe level of functors is wrong. Worse, it doesn't really seem to be possible to fix it.

[Reid Barton]

The current formula is:

structure functor (C : Type u₁) [category.{v₁} C] (D : Type u₂) [category.{v₂} D] :
  Type (max v₁ v₂ u₁ u₂) := -- ...

But this isn't right, because the homs of C and D live in Sort v₁ and Sort v₂ respectively not Type v₁ and Type v₂.
The correct formula would be

structure functor (C : Type u₁) [category.{v₁} C] (D : Type u₂) [category.{v₂} D] :
  Sort (max v₁ v₂ (u₁+1) (u₂+1)) := -- ...

[Reid Barton]

For example, suppose C and D are both small_category.{w}. Then v₁ = v₂ = w+1 and u₁ = u₂ = w. The type of functors from C to D should again be a Type w. But according to the current formula it is a Type (w+1).
This caused this definition to fail: https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/src/category_theory/bundled.lean#L27
(I know Cat is in mathlib now, but I'd rather first get the current version of my library to build with current mathlib before taking advantage of new mathlib features.)

[Reid Barton]

However, if we use the corrected formula, then we have a problem in functor_category: we want to make functors the objects of a category but they form a Sort _, not a Type _.

[Reid Barton]

So making objects be a Type u and morphisms a Sort v isn't compatible with assigning the correct universe level to functors, as far as I can see.

[Chris Hughes]

I think there was a time when the objects of a category were a Sort as well, bu Scott changed it, and I think it might have just been because he couldn't think of a reason why anyone would do that.

I think Sort valued homs might not be as useful as anticipated at first because they don't really work with limits as they are not small categories according to Lean.

[Scott Morrison]

Oh dear.

[Scott Morrison]

I think the solution is going to be to abandon again Sort-valued morphisms, which, as Chris says, have not ended up being usable.

[Reid Barton]

So back to the original Type for both objects and morphisms then?

[Scott Morrison]

Yes.

[Scott Morrison]

Sorry to cause so much needless trouble here.

[Keeley Hoek]

Maybe it's pointless, but am I right in thinking that we could also just allow Sort 0 objects again and everything would be fine? (And perhaps Reid has given the first example of someone wanting to construct a category with Sort 0 object?)

It's kinda nice having functors to Prop

[Scott Morrison]

I agree that having functors to Prop is really nice, and the reason I started generalising to Sort was to allow this.

[Scott Morrison]

My student Yiming did a bunch of work trying to do transport-across-isomorphisms automatically, and it relied heavily on the possibility of Prop valued functors. Not having them would not make her work impossible, but there would be a lot of extra plifts, which hopefully would all be invisible to the user, but ...

[Scott Morrison]

In case it's useful to any one, here is the PR that generalised everything to Sort, and here is the PR that partially reverted this, forcing objects into Type.

[Scott Morrison]

I am very tempted to hope that Keeley's suggestion is viable (i.e. that PR #1122 was ill-considered, and should be reverted).

[Scott Morrison]

Back when everything was in Sort, we had

structure functor (C : Sort u₁) [category.{v₁} C] (D : Sort u₂) [category.{v₂} D] : Sort (max u₁ v₁ u₂ v₂ 1) := ...

and I think this was also wrong according to Reid's analysis, because of that 1 appearing in the max.

[Scott Morrison]

The discussion explaining this 1 in the max in the original PR was at https://github.com/leanprover-community/mathlib/pull/824#discussion_r270540901

[Scott Morrison]

where while it's wrong, we decided it perhaps wasn't harmful.

[Mario Carneiro]

If you don't put the 1 in the projections won't work

[Scott Morrison]

Yes, I don't think there's any way of getting around having the 1.

[Scott Morrison]

The question is --- do we switch to objects and homs in Type (i.e. pre #824), or switch to objects and homs in Sort (ie. between #824 and #1122).

[Scott Morrison]

I've just made a branch which moves everything back to Type.

[Scott Morrison]

category_no_sorts

[Scott Morrison]

But I'm still tempted to go the other way.

[Kevin Buzzard]

Sorry to cause so much needless trouble here.

Leo stressed to me today that it was really important to treat Lean 3 experimentally and to try a lot of stuff and see what works.

[Patrick Massot]

He'll be disappointed we still haven't tried unification hints seriously

[Patrick Massot]

although we very clearly see how we don't manage to use the current type class system

[Kevin Buzzard]

He wants feedback of this nature. He is well aware that we complain about coercions and they will be different in Lean 4.

[Kevin Buzzard]

He's going to try something new with coercions because we are not happy with what he has. He's going to try something new with group laws because he thinks to_additive is a dirty hack. He hears our problems and responds.

I was reading Cyril Cohen's notes on unification hints only a week or so ago.

[Reid Barton]

I mildly prefer going back to using Type for both objects and morphisms because everything seemed to work a bit more smoothly then. When we switched to Sort I had to specify a number of additional universe levels in lean-homotopy-theory (I'm not 100% sure it was related to the Sort change, and I don't understand why exactly why the change would cause those universe levels to be needed, but it seemed like the most likely explanation at the time).

[Reid Barton]

Using Sort would be more appealing if we unified preorder with category.{0}, but I don't think that is going to happen

[Johan Commelin]

And of course it would be very appealing if it made preorder small categories in general... but that's also not going to happen.

[Johan Commelin]

Part of me wishes we had cummulative universes.

[Patrick Massot]

If I understand correctly, having cummulative universes would create exactly as many (different) issues. There is some conservation law at work.

[Johan Commelin]

Probably, yes.

[Johan Commelin]

That's why only part of me wishes this (-;

[Keeley Hoek]

What kind of problems (linky-link?)

[Scott Morrison]

@Reid Barton, okay, there's a PR up for restoring everything to live in Type. I'd be game to complete the branch where I moved everything to Sort instead (I will miss Prop valued functors; Yiming's partial work on induction along isomorphisms really relied on this, and I would like to complete this sometime). But I won't do that unless you tell me there's a chance you'd be happy to merge that instead.

[Keeley Hoek]

I weep for Props

[Keeley Hoek]

Transport of structure for e.g. local rings is equivalent to the existence of a functor from the core of CommRing to the category of is_local R Props, and the morphisms in the latter are Sorts