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 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: Dec 20 2023 at 11:08 UTC