has_binary_products etc.

Stream: new members

[Markus Himmel]

What is the intended way to instantiate has_binary_products for some specific category? In my case it is easy to instantiate has_limit (pair X Y) for all objects X and Y (using binary_fan etc.), but to then give an instance of has_limits_of_shape (discrete walking_pair) it is required to know that for all F : discrete walking_pair ⥤ C we have F = pair (F.obj walking_pair.left) (F.obj walking_pair.right), which is not hard to show using functor.ext, but I am wondering whether this is really the intended way to provide an instance of has_binary_products. One could of course work with F directly, but then you don't get useful tools like binary_fan.mk. The same question applies to has_equalizers (but not to has_kernels, which is directly defined via has_limit (parallel_pair f 0)).

[Johan Commelin]

Equality of functors is discouraged. But I think there is something like has_limit_of_iso, and F \iso pair (F.. left) (F.. right) seems like a useful fact to me.

[Johan Commelin]

Gluing those together is hopefully not a problem. But @Scott Morrison has a better overview then I do.

[Scott Morrison]

Yes, this is a wobbly part of the API still. :-(

[Scott Morrison]

Have you had a look at my WIP PR #1622?

[Scott Morrison]

I'd definitely avoid using functor.ext, it will come back and bite you later, I suspect.

[Scott Morrison]

But maybe providing a generic function for upgrading has_limit (pair X Y) for all X and Y into a has_limits_of_shape (discrete walking_pair) would be a good addition to the library? (Using transport along the natural isomorphism, as Johan sketched.)

[Markus Himmel]

Using a natural isomorphism sounds good, I'll look into it.