Zulip Chat Archive
Stream: general
Topic: typeclass loops in category theory
Floris van Doorn (Aug 31 2021 at 20:36):
I wrote a new linter that catches typeclass loops (#8932), and I'm making some topics with some issues it found. I don't always know the best solution to fix these loops, so I'm hoping that someone who knows that part of mathlib better can fix these.
In category theory (@Scott Morrison @Bhavik Mehta @others) I found the following issues:
 docs#category_theory.adjunction.has_limit_comp_equivalence and docs#category_theory.under.category_theory.limits.has_limit loop together. See following example (which is supposed to fail)
import category_theory.adjunction.limits
import category_theory.limits.over
open category_theory
universe u
example {J : Type*} [small_category J] {C : Type*} [_inst_2 : category C]
{X : C} (F : J ⥤ under X) :
limits.has_limit F :=
by apply_instance
 Similarly, docs#category_theory.adjunction.has_colimit_comp_equivalence and docs#category_theory.over.category_theory.limits.has_colimit loop together
 docs#category_theory.forget₂.category_theory.reflects_isomorphisms loops together with docs#category_theory.has_forget_to_Type
import category_theory.concrete_category.reflects_isomorphisms
open category_theory
universe u
variables (C : Type (u+1)) [category C] [concrete_category.{u} C]
variables (D : Type (u+1)) [category D] [concrete_category.{u} D]
example [has_forget₂ C D] : reflects_isomorphisms (forget₂ C D) :=
by apply_instance

The instance docs#category_theory.abelian.pseudoelement.has_zero doesn't cause a loop per se, but
whenever we are trying to find an instance forhas_zero
applied to anycoe_sort
this instance (and allcategory
instances) are tried. Can we make this localized? 
docs#category_theory.quiver.hom.add_comm_group (and other instances on
single_obj
if they exist) is superfluous, since typeclass inference is happy to unfold docs#category_theory.single_obj.category_struct. I don't think this really causes issues, but you could consider removing it
import category_theory.preadditive.default
import category_theory.single_obj
open category_theory
variables {α : Type*} [ring α]
def foo (X Y : single_obj α) : add_comm_group (X ⟶ Y) :=
by apply_instance
#print foo  ring.to_add_comm_group
Adam Topaz (Aug 31 2021 at 20:38):
@Floris van Doorn Just double checking... do you mean docs#category_theory.limits.has_limit_equivalence_comp ? (The first link doesn't work in your message.)
Floris van Doorn (Aug 31 2021 at 20:39):
Oops, it's missing the category_theory
prefix. I mean docs#category_theory.adjunction.has_limit_comp_equivalence
Adam Topaz (Aug 31 2021 at 20:40):
Ah!
Floris van Doorn (Aug 31 2021 at 20:40):
I fixed the links in my first message
Scott Morrison (Sep 12 2021 at 01:02):
Sorry this took a while to get to: #9154 #9155 #9156 #9157.
Scott Morrison (Sep 12 2021 at 01:02):
Thanks for writer a new linter! They are a really valuable investment.
Last updated: Aug 03 2023 at 10:10 UTC