You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Jacques Carette (Mar 16 2023 at 22:04):The context here is that of [[polynomial+functor]]. In the concrete terms of @David Spivak 's Poly: An abundant categorical setting for mode-dependent dynamics section 2.4, I'd like to know when two Lens should be considered equivalent. In other words, I'm interested in the Setoid-enriched version of Poly.
In theory, I think I should be able to decategorify Gylterud's Definition 2.1.2 from Symmetric Containers, but I am not confident that I've worked it out properly. Similarly, I think Definition 7 of Universal Properties of Bicategories of Polynomials is also 'it'.
Note that I am not interested in polynomial functors but rather polynomials themselves; the functors are the extension of the polynomials, or generated by them.
Jacques Carette (Mar 16 2023 at 22:12):The above might be off by 1, given some of the other things I'm reading. I was taking polynomials as objects, and morphisms as... morphisms.
So it might be needed to shift everything up by 1. But the question remains: when are two morphisms of polynomials equivalent?
Spencer Breiner (Mar 16 2023 at 22:30):By a polynomial, do you mean the representation as a bundle?
Spencer Breiner (Mar 16 2023 at 22:31):Perhaps the question (or a question), is whether this bundle should be a fibration or an arbitrary map.
Jacques Carette (Mar 16 2023 at 23:29):I think my answer is Definition 3.3 in A cartesian bicategory of polynomial functors in homotopy type theory, I just need to unpack it. The tricky part is that the definition of polynomial morphism is a 'cartesian' morphism (which is fine), and that's not what is often done in containers-land.