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.
Sjoerd Visscher (Nov 10 2021 at 14:06):This weekend I tweeted about using proarrow equipments in Haskell https://twitter.com/sjoerd_visscher/status/1457347734214742017 and then Denis Stoyanov pointed me to this paper https://groupoids.org.uk/pdffiles/rewrite2.pdf which talks about "connections" in double groupoids https://ncatlab.org/nlab/show/connection+on+a+double+category. They actually seem to be the same. Are they?
Here’s a visual proof that we can implement `Separable s` when we have `Adjunction s t` using the visual language of double categories (see https://hackage.haskell.org/package/squares-0.1.1/docs/Data-Square.html). The middle square is cotraverse, to its NW is leftAdjunct and to its SE is rightAdjunct. https://twitter.com/sjoerd_visscher/status/1456940011019018241 https://twitter.com/sjoerd_visscher/status/1457347734214742017/photo/1
- Sjoerd 슕 Visscher (@sjoerd_visscher) Nathanael Arkor (Nov 10 2021 at 14:18):Proarrow equipments are those double categories that have [[companions]] and [[conjoints]], but I'm not familiar enough with connections to know where they fit into this.
Sjoerd Visscher (Nov 10 2021 at 14:24):Indeed, and the connection page on nlab actually links to [[companions]]
Mike Shulman (Nov 10 2021 at 15:52):A connection is a functorially assigned choice of companions.
Sjoerd Visscher (Nov 11 2021 at 08:51):Ah I see. And if I understand correctly to get to a proarrow equipment you also need conjoints. But in double groupoids companions and conjoints are the same? That would explain why they call all the 4 "slide-around-the-corner" 2-cells "connections".
Sjoerd Visscher (Nov 11 2021 at 12:20):There's also more under "3. Thin structures in double categories" in [[thin element]] although I find that hard to follow.
Mike Shulman (Nov 11 2021 at 17:43):Yes, an invertible arrow has a companion iff its inverse has a conjoint.