## Stream: maths

### Topic: category theory universes

#### Kevin Buzzard (Dec 16 2019 at 12:20):

universes v u w
variables {C : Type u} [𝒞 : category.{v} C]
variables {X : Type w} [topological_space X]
def presheaf X C : Type (max u v w) := <insert maths here>
def : large_category (presheaf X C) := sorry


gives me

type mismatch at application
large_category (presheaf X C)
term
presheaf X C
has type
Type (max u v w) : Type (max (u+1) (v+1) (w+1))
but is expected to have type
Type (?+1) : Type (?+2)


Seems to me that Lean wants to know that "something is large". The risk is that if C is a small category then there won't be a universe small enough to contain my morphisms! I guess in that case I would rather have had a small category.

I'm going to make it a small category. A better approach would be to demand u>=1, which is fine here because u=1 in all the examples I care about, butI don't know how to manage that because of the delicate universe category-theory set-up -- I'm only just learning the basics.

#### Kevin Buzzard (Dec 16 2019 at 12:31):

Oh this is a nightmare. The morphisms have type max v w. Maybe I should just make a category :-/

#### Kevin Buzzard (Dec 16 2019 at 15:37):

I am back in hell

def XYZ: has_coe_to_fun (topological_space.presheaf X C) :=
by exact topological_space.presheaf.has_coe_to_fun

invalid type ascription, term has type
has_coe_to_fun (presheaf ?m_1 ?m_3) : Type (max (max ? ?) (max (?+1) 1) (?+1))
but is expected to have type
has_coe_to_fun (presheaf X C) : Type (max (max u v w) ?)
state:
X : Type w,
_inst_1 : topological_space X,
C : Type u,
𝒞 : category C
⊢ has_coe_to_fun (presheaf X C)


I just really want to say "switch the universes off, I honestly don't care and i think @Mario Carneiro is paranoid"

#### Kevin Buzzard (Dec 16 2019 at 15:38):

a little bit of type in type never hurt anyone.

#### Johan Commelin (Dec 16 2019 at 15:45):

I don't remember exactly, but this might have been one of the reasons why the category lib stopped using coercions for functors.

#### Kevin Buzzard (Dec 16 2019 at 15:50):

the computer scientists want us to be polymorphic and I just want sheaves of rings and I'll do anything they say about universes, as long as it works when stuff is Type 0 (sets) or Type 1 (classes) and the ZFC people will be happy. Why am I getting these obscure errors?

#### Kevin Buzzard (Dec 16 2019 at 15:52):

type mismatch at application
presheaf.res'.{?l_1 ?l_2} ℱ
term
ℱ
has type
presheaf.{v u w} X C : Type (max u v w)
but is expected to have type
presheaf.{?l_1 ?l_2 ?l_1} ?m_3 ?m_5 : Type (max ?l_1 ?l_2)


I don't know how to fix it with ulift. Am I supposed to be managing these universes myself?

#### Kevin Buzzard (Dec 16 2019 at 15:53):

I think I will try again with v, the universe of the morphisms in C being equal to w, the universe of the topological space X. In reality v and w are always sets so I'd even happily set v=w=0.

#### Chris Hughes (Dec 16 2019 at 15:54):

Looks like swapping all your ws to vs might help.

#### Kevin Buzzard (Dec 16 2019 at 15:54):

I'm letting w = v and it's working much better

#### Kevin Buzzard (Dec 16 2019 at 15:55):

w=v corresponds to the fact that mathematicians know that topological spaces and sets of morphisms are sets.

#### Kevin Buzzard (Dec 16 2019 at 15:55):

so they can live in the same universe

Last updated: May 06 2021 at 17:38 UTC