Zulip Chat Archive

Stream: general

Topic: sparse categories


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

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

view this post on Zulip Kevin Buzzard (Mar 30 2019 at 10:00):

It's a universe issue?

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

view this post on Zulip Scott Morrison (Mar 30 2019 at 10:20):

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

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

view this post on Zulip 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 := { }.

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

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