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: deprecated: id my structure

Topic: "weakly Cartesian closed"

Nathaniel Virgo (Sep 10 2023 at 03:21):

Consider a category where the objects are recursively defined data structures (e.g. defined as initial algebras of finite polynomial functors), and the morphisms are computable (partial) functions. (Functions in the sense of maths rather than programming - a morphism is a function such that there exists a program that implements it, rather than a program.)

Such a category is not Cartesian closed, because computable functions are not a recursively defined data type. However, we can recursively enumerate programs that evaluate to them, as long as we don't care that two programs might evaluate to the same function.

This means we can expect that for each pair of objects $X$ and $Y$ we should have an object $P$ equipped with a function $\mathrm{eval}\colon P\times X \to Y$ such that for every morphism $f\colon X\to Y$ there exists $1\xrightarrow{p}P$ such that $X\xrightarrow{f}Y = X\xrightarrow{\lambda ; p\times X} P\times X \xrightarrow{\mathrm{eval}} Y$. (The element $p$ need not be unique.) Think of $P$ as the set of strings and $\mathrm{eval}$ as an interpreter of a Turing complete language.

Is a there name for a weakened version of Cartesian closedness along these lines?

Mike Shulman (Sep 10 2023 at 03:46):

If you strengthen the property of $\rm eval$ to "for every morphism $f : A \times X \to Y$ there exists $p : A \to P$ such that $f = \mathrm{eval} \circ (p \times X)$, then it's called being "weakly cartesian closed".

Mike Shulman (Sep 10 2023 at 03:51):

People have studied this sort of property in the context of [[exact completion]]. A category weakly cartesian closed is almost necessary and sufficient for its free exact completion to be cartesian closed. I think what you actually need is something slightly stronger, the existence of weak right adjoints to pullback along product projections $X\times Y \to Y$ ("weak simple products").

Mike Shulman (Sep 10 2023 at 03:55):

And your category of data structures is related to the kinds of categories that people often want to exact-complete, since we often want to regard a data structure as a "presentation" of some set, but where there is a nontrivial equivalence relation of "presenting the same object". The exact completion thus incorporates such computable equivalence relations. In particular, the actual cartesian-closed exponentials in the exact completion are the "formal quotients" of the equivalence relation of "presenting the same function" on your data structure of codes.

Nathaniel Virgo (Sep 10 2023 at 04:19):

Mike Shulman said:

If you strengthen the property of $\rm eval$ to "for every morphism $f : A \times X \to Y$ there exists $p : A \to P$ such that $f = \mathrm{eval} \circ (p \times X)$, then it's called being "weakly cartesian closed".

Ahh, that's what I expected, but somehow didn't find it!

Mike Shulman (Sep 10 2023 at 04:33):

It doesn't appear to be on the nLab yet, unfortunately, but you can look in some papers about exact completions, like Carboni-Rosolini "Locally cartesian closed exact completions".

Mike Shulman (Sep 10 2023 at 04:33):

(Possibly they only talk about "weak exponentials" rather than the phrase "weakly cartesian closed".)

Mike Shulman (Sep 10 2023 at 04:37):

Or maybe even better is Jacopo Emmenegger's On the local cartesian closure of exact completions.

Mike Shulman (Sep 10 2023 at 04:37):

They emphasize the case where the category only has weak finite limits, where there's a lot more annoying bookkeeping.

Cole Comfort (Sep 10 2023 at 09:06):

You might also be interested in Turing categories