Zulip Chat Archive

Stream: maths

Topic: category universes again


view this post on Zulip Reid Barton (Sep 05 2019 at 20:39):

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

view this post on Zulip Reid Barton (Sep 05 2019 at 20:42):

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)) := -- ...

view this post on Zulip Reid Barton (Sep 05 2019 at 20:45):

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

view this post on Zulip Reid Barton (Sep 05 2019 at 20:46):

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

view this post on Zulip Reid Barton (Sep 05 2019 at 20:47):

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.

view this post on Zulip Chris Hughes (Sep 05 2019 at 21:01):

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.

view this post on Zulip Scott Morrison (Sep 05 2019 at 22:13):

Oh dear.

view this post on Zulip Scott Morrison (Sep 05 2019 at 22:14):

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

view this post on Zulip Reid Barton (Sep 05 2019 at 22:27):

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

view this post on Zulip Scott Morrison (Sep 05 2019 at 22:53):

Yes.

view this post on Zulip Scott Morrison (Sep 05 2019 at 22:53):

Sorry to cause so much needless trouble here.

view this post on Zulip Keeley Hoek (Sep 06 2019 at 02:53):

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

view this post on Zulip Scott Morrison (Sep 06 2019 at 03:37):

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

view this post on Zulip Scott Morrison (Sep 06 2019 at 03:38):

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

view this post on Zulip Scott Morrison (Sep 06 2019 at 03:44):

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.

view this post on Zulip Scott Morrison (Sep 06 2019 at 03:59):

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

view this post on Zulip Scott Morrison (Sep 06 2019 at 04:12):

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.

view this post on Zulip Scott Morrison (Sep 06 2019 at 04:12):

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

view this post on Zulip Scott Morrison (Sep 06 2019 at 04:13):

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

view this post on Zulip Mario Carneiro (Sep 06 2019 at 04:21):

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

view this post on Zulip Scott Morrison (Sep 06 2019 at 04:22):

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

view this post on Zulip Scott Morrison (Sep 06 2019 at 04:23):

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

view this post on Zulip Scott Morrison (Sep 06 2019 at 04:23):

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

view this post on Zulip Scott Morrison (Sep 06 2019 at 04:25):

category_no_sorts

view this post on Zulip Scott Morrison (Sep 06 2019 at 04:25):

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

view this post on Zulip Kevin Buzzard (Sep 06 2019 at 05:57):

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.

view this post on Zulip Patrick Massot (Sep 06 2019 at 06:25):

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

view this post on Zulip Patrick Massot (Sep 06 2019 at 06:26):

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

view this post on Zulip Kevin Buzzard (Sep 06 2019 at 06:26):

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

view this post on Zulip Kevin Buzzard (Sep 06 2019 at 06:28):

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.

view this post on Zulip Reid Barton (Sep 06 2019 at 13:54):

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

view this post on Zulip Reid Barton (Sep 06 2019 at 13:54):

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

view this post on Zulip Johan Commelin (Sep 06 2019 at 13:55):

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

view this post on Zulip Johan Commelin (Sep 06 2019 at 13:55):

Part of me wishes we had cummulative universes.

view this post on Zulip Patrick Massot (Sep 06 2019 at 13:58):

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

view this post on Zulip Johan Commelin (Sep 06 2019 at 13:58):

Probably, yes.

view this post on Zulip Johan Commelin (Sep 06 2019 at 13:58):

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

view this post on Zulip Keeley Hoek (Sep 06 2019 at 14:08):

What kind of problems (linky-link?)

view this post on Zulip Scott Morrison (Sep 08 2019 at 04:17):

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

view this post on Zulip Keeley Hoek (Sep 08 2019 at 04:21):

I weep for Props

view this post on Zulip Keeley Hoek (Sep 08 2019 at 04:24):

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


Last updated: May 09 2021 at 10:11 UTC