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.
Mike Stay (Jun 01 2020 at 17:04):This paper by Shirahata introduces a notion of "linear comprehension" (that follows the principles of linear logic:
Screen-Shot-2020-06-01-at-11.03.00-AM.png
Mike Stay (Jun 01 2020 at 17:06):Comprehensions are what the Mitchell-Benabou language of a topos formalizes. Is there a topos of such linear sets?
sarahzrf (Jun 04 2020 at 23:00):it probably won't be a topos
sarahzrf (Jun 04 2020 at 23:01):topoi are cartesian as part of their definition
sarahzrf (Jun 04 2020 at 23:07):but @Mike Shulman's "affine triposes" may be what you want
sarahzrf (Jun 04 2020 at 23:08):actually, no, sorry, that's not right—those have an affine logic, but they don't have pervasive affine-ness requirements in arbitrary morphisms, oops