Zulip Chat Archive

Stream: general

Topic: weird class error


view this post on Zulip Reid Barton (Dec 07 2018 at 02:28):

import category_theory.limits.limits
import category_theory.limits.types

universes u v

open category_theory

section
variables (C : Type u) [𝒞 : category.{u v} C] [limits.has_colimits C]
include 𝒞
def is_good : Prop := sorry
lemma is_good_of_has_object (X : C) : is_good C := sorry
end

def MyCat := Type v
instance : category MyCat := by dunfold MyCat; apply_instance
instance : limits.has_colimits.{v+1 v} MyCat := by dunfold MyCat; apply_instance
lemma MyCat_is_good : is_good MyCat.{v} := is_good_of_has_object MyCat.{v} punit.{v+1}

/-
error: failed to synthesize type class instance for
⊢ Π (J : Type v) (𝒥 : small_category J) (F : J ⥤ MyCat), limits.has_colimit F
error: synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized

inferred
  λ (J : Type v) (𝒥 : small_category J) (F : J ⥤ MyCat), MyCat.category_theory.limits.has_colimits F
-/

view this post on Zulip Reid Barton (Dec 07 2018 at 02:29):

Is my definition

@[class] def has_colimits :=
Π {J : Type v} {𝒥 : small_category J}, by exactI has_colimits_of_shape J C

already asking too much of the class system?

view this post on Zulip Reid Barton (Dec 07 2018 at 02:48):

Also strange: if I change has_colimits to a structure, then I need to add universe annotations to many of its use sites, even if I control for all the variables I'm aware of (same syntactic return universe, both assigned class after the fact, both given elab_simple)

view this post on Zulip Johan Commelin (Dec 07 2018 at 15:47):

I think I witnessed similar problems when I tried to get the stuff on presheaves in line with the merged limits PR. But I didn't investigate further.


Last updated: May 16 2021 at 21:11 UTC