# Zulip Chat Archive

## 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 `Prop`

s?

#### 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