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 (Mar 22 2021 at 16:31):To model classical linear logic, you need a ∗-autonomous category with finite products and a linear exponential comonad. What kind of category also supports quantifiers without bringing in the full power of a topos?
Fawzi Hreiki (Mar 22 2021 at 16:39):I'd imagine something like a linear hyperdoctrine.
Fawzi Hreiki (Mar 22 2021 at 16:39):Although to get first-order logic you may want the fibres to be thin
Fawzi Hreiki (Mar 22 2021 at 16:40):But there's no reason why you can't have a hyperdoctrine where there fibres aren't thin, instead giving something more like a dependent type theory
Mike Stay (Mar 22 2021 at 17:10):Thanks, that's just what I was looking for.