## Stream: general

### Topic: sparse categories

#### Scott Morrison (Mar 30 2019 at 09:05):

@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 (Mar 30 2019 at 10:00):

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 (Mar 30 2019 at 10:00):

It's a universe issue?

#### Kevin Buzzard (Mar 30 2019 at 10:05):

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 (Mar 30 2019 at 10:20):

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

#### Scott Morrison (Mar 30 2019 at 10:27):

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 (Mar 30 2019 at 10:34):

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 (Mar 30 2019 at 10:35):

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 (Mar 30 2019 at 10:35):

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

Last updated: May 10 2021 at 17:39 UTC