Zulip Chat Archive

Stream: maths

Topic: category theory universes


view this post on Zulip 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.

view this post on Zulip 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 :-/

view this post on Zulip 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"

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 15:38):

a little bit of type in type never hurt anyone.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Dec 16 2019 at 15:54):

Looks like swapping all your ws to vs might help.

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 15:54):

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

view this post on Zulip 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.

view this post on Zulip 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