Zulip Chat Archive

Stream: general

Topic: type-class loops in category theory

Floris van Doorn (Aug 31 2021 at 20:36):

I wrote a new linter that catches type-class 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:

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
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
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):


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