Typeclasses in category_theory/limits

Stream: new members

[Markus Himmel]

@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]

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]

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

[Johan Commelin]

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]

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

[Scott Morrison]

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

[Markus Himmel]

Sorry, that was a typo