sparse categories

Stream: general

[Scott Morrison]

@Reid Barton, @Floris van Doorn, I was experimenting with sparse categories (I think they are an excellent idea), but ran into this pesky issue:

import category_theory.category

universes u v

namespace category_theory

variables {C : Type u} [category_struct.{v} C]

instance sparse_category [∀ X Y : C, subsingleton (X ⟶ Y)] : category.{v} C := { }

lemma foo [∀ X Y : C, subsingleton (X ⟶ Y)] (X Y : C) (f : X ⟶ Y) : 𝟙 X ≫ f = f :=
begin
  simp,
end

end category_theory

For some reason the simp fails, and can't apply the simp lemma category.id_comp. I can't work out what's going on here. Any ideas??

[Kevin Buzzard]

lemma foo [∀ X Y : C, subsingleton (X ⟶ Y)] (X Y : C) (f : X ⟶ Y) : 𝟙 X ≫ f = f :=
begin
  refine category.id_comp _ f, -- goals accomplished!
end
/-
kernel failed to type check declaration 'foo' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  ∀ {C : Type u} [_inst_1 : category_struct C] [_inst_2 : ∀ (X Y : C), subsingleton (X ⟶ Y)] (X Y : C)
  (f : X ⟶ Y), 𝟙 X ≫ f = f
elaborated value:
  λ {C : Type u} [_inst_1 : category_struct C] [_inst_2 : ∀ (X Y : C), subsingleton (X ⟶ Y)] (X Y : C)
  (f : X ⟶ Y), category.id_comp C f
nested exception message:
invalid reference to undefined universe level parameter 'v'
-/

[Kevin Buzzard]

It's a universe issue?

[Kevin Buzzard]

set_option pp.universes true
set_option pp.notation false

lemma foo [∀ X Y : C, subsingleton (X ⟶ Y)] (X Y : C) (f : X ⟶ Y) : 𝟙 X ≫ f = f :=
begin
  refine category.id_comp' _ f, -- goals accomplished!
end
/-
kernel failed to type check declaration 'foo' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  ∀ {C : Type u} [_inst_1 : category_struct.{v u} C]
  [_inst_2 : ∀ (X Y : C), subsingleton.{v+1} (has_hom.hom.{v u} X Y)] (X Y : C) (f : has_hom.hom.{v u} X Y),
    eq.{v+1} (category_struct.comp.{v u} (category_struct.id.{v u} X) f) f
elaborated value:
  λ {C : Type u} [_inst_1 : category_struct.{v u} C]
  [_inst_2 : ∀ (X Y : C), subsingleton.{v+1} (has_hom.hom.{v u} X Y)] (X Y : C) (f : has_hom.hom.{v u} X Y),
    category.id_comp'.{v u} C f
nested exception message:
invalid reference to undefined universe level parameter 'v'
-/

[Scott Morrison]

ah... that looks like it could be the problem!

[Scott Morrison]

Hmm... it's a problem, but apparently not the problem!

lemma foo [∀ X Y : C, subsingleton.{v} (X ⟶ Y)] (X Y : C) (f : X ⟶ Y) : 𝟙 X ≫ f = f :=
begin
  refine category.id_comp' _ f, -- goals accomplished!
end

works, but you still can't prove that lemma by simp.

[Scott Morrison]

hmm, okay. For some reason that I don't understand simp can't cope with synthesising category instances via instance sparse_category [∀ X Y : C, subsingleton (X ⟶ Y)] : category.{v} C := { }.

[Scott Morrison]

The workaround is just to have this be a def instead, and you just use it to build the instance once and for all, rather than looking up the subsingleton instances at each use.

[Scott Morrison]

(That's probably the more sensible use anyway.)