Zulip Chat Archive

Stream: new members

Topic: Typeclasses in category_theory/limits


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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".

view this post on Zulip 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)?

view this post on Zulip Scott Morrison (Mar 05 2020 at 07:56):

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

view this post on Zulip Markus Himmel (Mar 05 2020 at 07:57):

Sorry, that was a typo


Last updated: May 06 2021 at 21:09 UTC