## Stream: new members

### Topic: Typeclasses in category_theory/limits

#### Markus Himmel (Mar 05 2020 at 07:32):

@Scott Morrison, while I was thinking about your comment on #2083 I noticed that I don't understand how the typeclasses in the limits library work. Say I have some concrete category where I can instantiate has_finite_products and has_equalizers explicitly. Now assume that there is some theorem that tells me something about an equalizer, but it requires has_finite_limits for some reason and infers the existence of equalizers from that (for example using #2083). If I use this theorem with finite_limits_from_equalizers_and_finite_products, do I get a statement about the nice equalizers I instantiated manually or about those constructed by finite_limits_from_equalizers_and_finite_products?

#### Scott Morrison (Mar 05 2020 at 07:34):

I'm not exactly sure what you mean, but I suspect a pessimistic answer is appropriate: "it depends". Certainly we could end up with non-definitionally equal instances of these typeclasses.

#### Johan Commelin (Mar 05 2020 at 07:53):

At the moment, all these typeclasses carry data. To what extent could we actually make them Props?

#### Johan Commelin (Mar 05 2020 at 07:54):

I guess that would mean an ugly amount of classical.choice all over the place. Which probably means that for all practical purposes the answer to my question is "No. Don't".

#### Markus Himmel (Mar 05 2020 at 07:55):

Maybe one could make has_equalizers a synonym for \forall f g, has_limit (parallel_pair f g)?

#### Scott Morrison (Mar 05 2020 at 07:56):

I'm not sure what you mean. parallel_pair f g isn't a shape

#### Markus Himmel (Mar 05 2020 at 07:57):

Sorry, that was a typo

Last updated: May 06 2021 at 21:09 UTC