Stream: new members
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_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
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
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