Skip to content

Commit 11bbb4e

Browse files
committed
chore(CategoryTheory/Presentable/Basic): remove bad instance (leanprover-community#27941)
The instance `HasCardinalFilteredColimits.hasColimitsOfShape` is bad because it has no way to infer the value of `κ`. Almost a year ago there was a change to type classes, which causes Lean to not give a warning about this, in leanprover/lean4#5376 and I would like to fix that.
1 parent 2c4e63c commit 11bbb4e

1 file changed

Lines changed: 0 additions & 2 deletions

File tree

Mathlib/CategoryTheory/Presentable/Basic.lean

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -160,8 +160,6 @@ class HasCardinalFilteredColimits : Prop where
160160
hasColimitsOfShape (J : Type w) [SmallCategory J] [IsCardinalFiltered J κ] :
161161
HasColimitsOfShape J C := by intros; infer_instance
162162

163-
attribute [instance] HasCardinalFilteredColimits.hasColimitsOfShape
164-
165163
instance [HasColimitsOfSize.{w, w} C] : HasCardinalFilteredColimits.{w} C κ where
166164

167165
end

0 commit comments

Comments
 (0)