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.
Faré (Apr 10 2020 at 09:34):If A is a datatype, what do -A, 1/A, 1/2 A mean, if anything?
James Wood (Apr 10 2020 at 09:38):Faré said:
If A is a datatype, what do -A, 1/A, 1/2 A mean, if anything?
Not standardly, but there's some discussion of it here: https://groups.google.com/forum/#!topic/hott-cafe/jbPtbnnAczY
Faré (Apr 10 2020 at 09:40):Maybe they kind of make sense in linear logic?
cancels one choice for ... maybe some weird operation to modify a program by invalidating a possible choice?
cancels in a product, so is like in linear logic, indicates that some function/continuation/operator/blah is consuming .
James Wood (Apr 10 2020 at 09:45):Still then, I think it's quite difficult. You don't have , and you'd probably be missing a similar law for the additive negation.
James Wood (Apr 10 2020 at 09:46):(Instead, you have .)
James Wood (Apr 10 2020 at 09:47):I think I've thought about things like this before, and ended up with tensor and par collapsing. Maybe that'd be acceptable for what you're wanting, but it wasn't for me.
Bob Atkey (Apr 10 2020 at 09:49):Tensor and Par collapsing essentially gets you a compact closed category, which one can think of as the categorification of abelian groups.
James Wood (Apr 10 2020 at 09:51):Oh, that's a good point!
vikraman (Apr 10 2020 at 15:09):Some of these can be made sense of in the context of reversible programming languages, some papers are listed here: https://amr-sabry.luddy.indiana.edu/research/ and a recent draft here: https://arxiv.org/abs/2002.07020
Sam Tenka (Apr 10 2020 at 15:59):Also see Blass's "7 trees in 1"