# Zulip Chat Archive

## 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