# Zulip Chat Archive

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

s to `v`

s 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