category theory universe issue?

Stream: general

[Kevin Buzzard]

question in progress -- ignore for now unless you're Scott

I am using a slightly modified mathlib but I am hoping this isn't the issue [update: it is]. The following innocuous-looking code:

import topology.opens
import category_theory.functor
import category_theory.instances.Top

open category_theory.instances

universes v u

variables {α : Type*} {β : Type*} [topological_space α] [topological_space β]
{f : α → β}

open topological_space

theorem is_open_map_of_open {α : Type*} [topological_space α] {s : set α} (hs : _root_.is_open s) :
  is_open_map (subtype.val : {x // x ∈ s} → α) := begin
  rintros _ ⟨t, ht, rfl⟩, convert is_open_inter _ _ _ ht hs,
  rw set.image_preimage_eq_inter_range,
  convert rfl,
  exact (set.range_coe_subtype s).symm
end

def is_open_map.map (h : is_open_map f) : opens α → opens β :=
λ U, ⟨f '' U.1, h U.1 U.2⟩

def functor.is_open_map.map (h : is_open_map f) : opens α ⥤ opens β :=
{ obj := is_open_map.map h,
  map := λ X Y hXY x ⟨a, ha, ha'⟩, begin rw ←ha', use a, exact ⟨hXY ha, rfl⟩ end,
  map_id' := λ _, rfl,
  map_comp' := λ _ _ _ _ _, rfl }

def inclusion (X : Top.{v}) (U : opens.{v} X) : opens.{v} ({x // x ∈ U.val}) ⥤ opens.{v} X :=
functor.is_open_map.map.{v v} (is_open_map_of_open U.2)

doesn't work. First I show that the inclusion of an open set is an open map. Then I define a function opens alpha -> opens beta from an open map alpha -> beta. Then I beef it up into a functor. Then I try and apply it in the situation of an open map. I get an error in the def of inclusion, a type mismatch hundreds of lines long because pp.all has been switched on by Lean.

The two terms look identical other than in one small place: diff output is

<     (@topological_space.opens.opens_category X)
---
>     (@category_theory.preorder_category
>        (@topological_space.opens
>           (@coe_sort category_theory.instances.Top (@category_theory.bundled.has_coe_to_sort topological_space) X)
>           (category_theory.instances.topological_space_unbundled X))
>        (@partial_order.to_preorder
>           (@topological_space.opens
>              (@coe_sort category_theory.instances.Top (@category_theory.bundled.has_coe_to_sort topological_space) X)
>              (category_theory.instances.topological_space_unbundled X))
>           (@topological_space.opens.partial_order
>              (@coe_sort category_theory.instances.Top (@category_theory.bundled.has_coe_to_sort topological_space) X)
>              (category_theory.instances.topological_space_unbundled X))))

I then attempt to verify that these terms are the same:

def inclusion (X : Top.{v}) (U : opens X) : opens ({x // x ∈ U.val}) ⥤ opens X :=
--functor.is_open_map.map (is_open_map_of_open U.2)
begin
have H :     (@topological_space.opens.opens_category X) =
     (@category_theory.preorder_category
        (@topological_space.opens
           (@coe_sort category_theory.instances.Top (@category_theory.bundled.has_coe_to_sort topological_space) X)
           (category_theory.instances.topological_space_unbundled X))
        (@partial_order.to_preorder
           (@topological_space.opens
              (@coe_sort category_theory.instances.Top (@category_theory.bundled.has_coe_to_sort topological_space) X)
              (category_theory.instances.topological_space_unbundled X))
           (@topological_space.opens.partial_order
              (@coe_sort category_theory.instances.Top (@category_theory.bundled.has_coe_to_sort topological_space) X)
              (category_theory.instances.topological_space_unbundled X)))),

exact functor.is_open_map.map (is_open_map_of_open U.2),
end

and this time the error (in the definition of H) is:

type mismatch at application
  opens.opens_category = category_theory.preorder_category (opens ↥X)
term
  category_theory.preorder_category (opens ↥X)
has type
  category_theory.category.{0 v+1}
    (@topological_space.opens.{v}
       (@coe_sort.{v+2 v+2} category_theory.instances.Top.{v}
          (@category_theory.bundled.has_coe_to_sort.{v+1 v+1} topological_space.{v})
          X)
       (category_theory.instances.topological_space_unbundled.{v} X)) : Type v
but is expected to have type
  category_theory.category.{v+1 (max (v+1) 1)}
    (@topological_space.opens.{v}
       (@coe_sort.{v+2 v+2} category_theory.instances.Top.{v}
          (@category_theory.bundled.has_coe_to_sort.{v+1 v+1} topological_space.{v})
          X)
       (category_theory.instances.topological_space_unbundled.{v} X)) : Type (v+1)

This time Lean seems to have switched universes on! The two terms are equal except for universes.

Is this the sort of thing I just have to deal with in category theory? @Reid Barton ?

[Kevin Buzzard]

Oh boggle I just checked with a vanilla mathlib and category_theory.instances.Top isn't there. That'll teach me to listen to Scott.

[Kevin Buzzard]

@Scott Morrison is this something to do with your modification category_theory.instances.Top of category_theory.instances.topological_spaces in your branch? I switched back to topological_spaces and now I see ulifts and plifts when I try to define the functor.

[Kevin Buzzard]

This is all something to do with turning hom sets from Type v into Prop.

[Kevin Buzzard]

Sorry, this is an issue with some of Scott's work in progress; I'll take it to github. I can get this to with in regular mathlib.

[Scott Morrison]

Sorry! :-) There is a big queue of PRs in category theory at the moment, making things a bit confusing.