Making sense of universes

Stream: general

[Praneeth Kolichala]

I'm having trouble understanding how Lean handles universes in category theory. For example, consider the following:

import topology.homotopy.fundamental_groupoid

noncomputable theory

universes u v w

abbreviation π := fundamental_groupoid.fundamental_groupoid_functor

variables {A : Top.{u}} {B : Top.{v}}

/-- The induced map of the left projection map X × Y → X -/
def proj_left : (π.obj (Top.of (A × B))).α ⥤ (π.obj A).α := π.map ⟨_, continuous_fst⟩

Note that this doesn't work because A and B are different universes. The error message is hard to decipher, so I don't know exactly what went wrong, however. If I change B to also be in universe u, then the example works. Similarly, if I change A to be in universe max u v, the example works. I guess this means that π.obj A has to be in the same universe as (π.obj (Top.of (A × B))).α.

What I want is for A to live in universe u, B to live in universe v, A × B to live in universe max u v, and then (π.obj A).α to be promoted to universe max u v.

Eventually, I want to be able to use the fundamental groupoid on spaces like I × X(where I is the unit interval), which is useful because it is the domain of homotopies. However, is using ulift to promote I to the same universe as X really the best way? Or can I make some of this projection stuff work even when the two spaces are in different universes?

[Adam Topaz]

Inspect the type of \pi.map after writing set_option pp.universes true

[Adam Topaz]

It's because of the fact that pi is a functor.

[Junyan Xu]

You are trying to apply fundamental_groupoid_functor: Top ⥤ category_theory.Groupoid to the morphism A × B ⟶ A in Top, but A × B and A aren't in the same universe, while objects in a category (Top here) have to be in the same universe, so there isn't such a morphism no matter which universe Lean specializes Top to. I think your best chance is to factor out the map part of fundamental_groupoid_functor as fundamental_groupoid_map that takes a continuous map argument (which is polymorphic in two independent universe variables for the source and the target) instead of a morphism in Top, and use it to define your proj_left instead.

[Reid Barton]

In lean-homotopy-theory I specialized most stuff to Type due to this issue (and because I felt no particular need to handle larger universes), e.g. in https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/src/homotopy_theory/topological_spaces/cylinder.lean