Category Theory
Zulip Server
Archive

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.

Stream: learning: questions

Topic: affine triposes and affine toposes

Matteo Capucci (he/him) (Jun 09 2021 at 10:51):

In Mike Shulman's expository paper about linear logic, he defines 'affine triposes' as follows:
affine-tripos.png
I have two questions regarding this

1. Why wasn't 'cartesian' replaced with 'monoidal' throughout?
2. Is there an equivalent to the Pitts construction for these triposes, i.e. a construction of some category whose internal theory coincides with the starting tripos? After the definition of affine tripos, it seems this is what's happening, but I don't recall an explicit tying up of all the various definitions into a category and an explicit relation of this with the original affine tripos.

Nathanael Arkor (Jun 09 2021 at 10:52):

Seems a question worth cc'ing @Mike Shulman on :)

Matteo Capucci (he/him) (Jun 09 2021 at 11:22):

Uh, definitely :blush:

Mike Shulman (Jun 09 2021 at 13:07):

Re 1, there's only one remaining occurrence of "cartesian", in the assumption that $\mathbf{T}$ is cartesian closed. If $\mathbf{T}$ were only monoidal closed, there would be no "product projections" with respect to which to formulate the third bullet point. One could imagine taking $\mathbf{T}$ to be only semicartesian, but I didn't feel like going down that rabbit hole. In particular, usually in first-order linear/affine logic the quantifiers are regarded as wholly additive, which suggests that the base category should be cartesian monoidal.

Mike Shulman (Jun 09 2021 at 13:09):

Re 2, I thought about that a bit, but wasn't able to make sense of it. There is a construction of a category of what you might call "affine sets", but it doesn't carry all the information of the original affine tripos, and in particular there's no obvious sense in which the affine predicates are incarnated as "subobjects" in it.

Matteo Capucci (he/him) (Jun 09 2021 at 13:29):

Mike Shulman said:

Re 1, there's only one remaining occurrence of "cartesian", in the assumption that $\mathbf{T}$ is cartesian closed. If $\mathbf{T}$ were only monoidal closed, there would be no "product projections" with respect to which to formulate the third bullet point. One could imagine taking $\mathbf{T}$ to be only semicartesian, but I didn't feel like going down that rabbit hole. In particular, usually in first-order linear/affine logic the quantifiers are regarded as wholly additive, which suggests that the base category should be cartesian monoidal.

I see, indeed I was thinking too that the most you can do is semicartesian with such a definition. On the other hand, (3) could be replaced with a more agnostic requirement that every map $f^* = T(f, \Omega)$ has both adjoints (perhaps forming a Wirthmuller context?).
Also, one could go the fibrational way and define an affine tripos to be some suitable notion of monoidal fibration with a power object (mimicking, for example, the definition in Chapter 2 here). I don't know/remember enough linear logic to understand whether this is sensible or not, though.

Matteo Capucci (he/him) (Jun 09 2021 at 13:30):

Mike Shulman said:

Re 2, I thought about that a bit, but wasn't able to make sense of it. There is a construction of a category of what you might call "affine sets", but it doesn't carry all the information of the original affine tripos, and in particular there's no obvious sense in which the affine predicates are incarnated as "subobjects" in it.

Ah, I see. This is a more interesting issue.

Matteo Capucci (he/him) (Jun 09 2021 at 13:35):

Matteo Capucci (he/him) said:

Mike Shulman said:

Re 2, I thought about that a bit, but wasn't able to make sense of it. There is a construction of a category of what you might call "affine sets", but it doesn't carry all the information of the original affine tripos, and in particular there's no obvious sense in which the affine predicates are incarnated as "subobjects" in it.

Ah, I see. This is a more interesting issue.

Forgive me if I continue speculating, could it help to enrich such a category in $\mathbf T$ itself?

Matteo Capucci (he/him) (Jun 09 2021 at 13:37):

It seems to me there's a mismatch between the 'external' non-linear logic of sets and the 'internal' linear logic we are trying to house.

Mike Shulman (Jun 09 2021 at 13:43):

BTW, I'm actually revising this paper at the very moment, so if there's something interesting to say here I might incorporate it. In particular, in response to referee comments I'm generalizing the semantic context to deal with intuitionistic and affine hyperdoctrines rather than just triposes, where the fiber categories may not be posets and there may not be a generic predicate. Also, the "standard interpretation" is being renamed the "antithesis translation".

Mike Shulman (Jun 09 2021 at 13:49):

For the purposes of this paper I'm not hugely interested in generalizing to semicartesian $\mathbf{T}$, since the main point is to study the antithesis translation applied to intuitionistic logic, and this always starts with a cartesian $\mathbf{T}$ and preserves it. However, if there's something interesting and not too difficult to say, it might be worth mentioning.

Mike Shulman (Jun 09 2021 at 14:54):

Matteo Capucci (he/him) said:

On the other hand, (3) could be replaced with a more agnostic requirement that every map $f^* = T(f, \Omega)$ has both adjoints.

A problem with this is how do you formulate a Beck-Chevalley condition? In the cartesian case, the BC condition for adjoints of an arbitrary $f^*$ refers to arbitrary pullback squares. When restricted to product projections this is sensible, since the pullback of a product projection is a product projection. And the product projection version generalizes to the semicartesian case directly, but the squares in question are no longer pullbacks. But in a noncartesian case with adjoints for non-projections, which squares should satisfy the BC condition?

Mike Shulman (Jun 09 2021 at 14:54):

could it help to enrich such a category in $\mathbf T$ itself?

why might it?

Matteo Capucci (he/him) (Jun 10 2021 at 14:55):

Mike Shulman said:

Matteo Capucci (he/him) said:

On the other hand, (3) could be replaced with a more agnostic requirement that every map $f^* = T(f, \Omega)$ has both adjoints.

A problem with this is how do you formulate a Beck-Chevalley condition? In the cartesian case, the BC condition for adjoints of an arbitrary $f^*$ refers to arbitrary pullback squares. When restricted to product projections this is sensible, since the pullback of a product projection is a product projection. And the product projection version generalizes to the semicartesian case directly, but the squares in question are no longer pullbacks. But in a noncartesian case with adjoints for non-projections, which squares should satisfy the BC condition?

I think BC would be replaced by the conditions imposed on the adjoint triple $\exists f \dashv f^* \dashv \forall f$ by the definition of Wirthmuller context. At least, this nlab article seems to be hinting at that.
If I recall correctly, the fact $f^*$ is strong monoidal is equivalent to ask directly for the Frobenius identity, which is one of the ways BC is useful to have for hyperdoctrines if I'm not mistaken.

Matteo Capucci (he/him) (Jun 10 2021 at 14:56):

Mike Shulman said:

could it help to enrich such a category in $\mathbf T$ itself?

why might it?

That was a shot in the dark... Feel free to ignore it.

Mike Shulman (Jun 10 2021 at 16:00):

BC conditions are about relating the $f$-adjunctions for different $f$'s.