## Stream: maths

### Topic: category universes again

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

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


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

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

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

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

Oh dear.

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

#### Reid Barton (Sep 05 2019 at 22:27):

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

Yes.

#### Scott Morrison (Sep 05 2019 at 22:53):

Sorry to cause so much needless trouble here.

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

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

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

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

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

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

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

#### Scott Morrison (Sep 06 2019 at 04:13):

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

#### Mario Carneiro (Sep 06 2019 at 04:21):

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

#### Scott Morrison (Sep 06 2019 at 04:22):

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

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

#### Scott Morrison (Sep 06 2019 at 04:23):

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

#### Scott Morrison (Sep 06 2019 at 04:25):

category_no_sorts

#### Scott Morrison (Sep 06 2019 at 04:25):

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

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

#### Patrick Massot (Sep 06 2019 at 06:25):

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

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

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

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

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

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

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

#### Johan Commelin (Sep 06 2019 at 13:55):

Part of me wishes we had cummulative universes.

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

Probably, yes.

#### Johan Commelin (Sep 06 2019 at 13:58):

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

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

#### Keeley Hoek (Sep 08 2019 at 04:21):

I weep for Props

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