category theory universes

Stream: maths

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

a little bit of type in type never hurt anyone.

[Johan Commelin]

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]

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]

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]

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]

Looks like swapping all your ws to vs might help.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

so they can live in the same universe