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: Optics and apartness

Spencer Breiner (Apr 06 2021 at 16:51):

Hi all! I was just looking at the recent preprint by @Benno van den Berg & Robert Passmann on Converse extensionality and apartness. Most of the paper is out of my depth, but this passage from the introduction jumped out at me:

Spencer Breiner (Apr 06 2021 at 16:52):

image.png

Spencer Breiner (Apr 06 2021 at 16:54):

I'm just wondering if the apartness information being "passed back" can be interpreted optically? I know there are connections between optics and linear logic/Dialectica translation (which is the theoretical locus of this paper), but not how they work, so this might be obvious to an initiate.

Jules Hedges (Apr 06 2021 at 16:57):

It sounds plausible, at least

Jules Hedges (Apr 06 2021 at 16:58):

It's crossed the mind of several people that a similar trick might be possible with continuous functions, which in some sense pass "approximate equality" backwards

John Baez (Apr 06 2021 at 17:51):

Backwards? If $f$ is continuous and $f(x) \approx f(y)$ we don't have $x \approx y$ in general.

If $f$ is continuous and $x \approx y$ then $f(x) \approx f(y)$.

Jules Hedges (Apr 06 2021 at 17:55):

Uh, yeah, I guess I mean it passes back some kind of apartness

Dylan Braithwaite (Apr 06 2021 at 18:07):

The obvious notion would be that it passes back open neighborhoods, no? Is there something more subtle going on than that?

John Baez (Apr 06 2021 at 18:10):

Continuous functions pass open neighborhoods backward and thus pass approximate equality forward. Once you understand why it works like this, you understand how two important approaches to continuity agree.

John Baez (Apr 06 2021 at 18:19):

For example, we can define continuity of a function $f: X \to Y$ between topological space by saying that for any net $x_\alpha$ in $X$ we have

$x_\alpha \to x \implies f(x_\alpha) \to f(x)$

i.e. "when some points $x_\alpha$ get close to $x$, the points $f(x_\alpha)$ get close to $f(x)$".

But this is equivalent to

$U$ open $\implies f^{-1}(U)$ open

for any set $U$ in $Y$.

John Baez (Apr 06 2021 at 18:22):

In synthetic differential geometry or nonstandard analysis we can simplify the net definition and define continuity by saying

$x \approx x'$ $\implies$ $f(x) \approx f(x')$

John Baez (Apr 06 2021 at 18:22):

So here we really see continuity passing approximate equality forwards.

Spencer Breiner (Apr 06 2021 at 22:13):

This isn't about continuity, just functionality. Specifically, the paper is about extracting computational content from function extensionality, which is apparently difficult (this is the part that is beyond me).

Spencer Breiner (Apr 06 2021 at 22:15):

In particular, if $f(x)\not=f(y)$, then $x\not=y$.

Spencer Breiner (Apr 06 2021 at 22:16):

Extensionality is hidden in here somewhere. I guess it's easier to see if we write it like this: $f(x)\not=g(y)$ implies $x\not=y$ or $f\not=g$.

Spencer Breiner (Apr 06 2021 at 22:18):

Really I should be writing $x\#y$ for the apartness relation, rather than $x\not=y$.

Spencer Breiner (Apr 06 2021 at 22:21):

Anyway, what's getting passed back is evidence of difference. I thought this felt somewhat analogous, e.g., the expression of reverse differential categories as optics.

Matteo Capucci (he/him) (Apr 07 2021 at 12:14):

In Shulman's paper about linear logic for constructive math there is a mention of sets with both an equality and an inequality predicate, and extensionality in both senses

Benno van den Berg (Apr 07 2021 at 12:58):

A few comments: First of all, nice to hear that people are interested in our paper! Secondly, I have heard the term "optics" but I do not really know what it is about. But from I understand it does have something to do with Dialectica and so does our paper, so there is bound to be a connection somehow. (In fact, something like reflecting apartness happens in the Dialectica toposes as well: this is one of the things I want to have a closer look at it in the future.) Thirdly, the reason why there is a tension between function extensionality and Dialectica is not so easy to explain: one can look at Howard's appendix of Troelstra's 344 or Kohlenbach's book on proof mining for the true story. The main problem is that extensionality gets upgraded by Dialectica to a strong version of it, which we call "converse extensionality" in the paper (see also Remark 4.15 in our paper and note that Dialectica interprets both AC and MP_n). It is hard to understand why that should be true constructively, unless you start making continuity assumptions (so there is a connection to continuity in that sense). We tried to avoid doing that as much as we could, but with limited success.