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.
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 and we should have an object equipped with a function such that for every morphism there exists such that . (The element need not be unique.) Think of as the set of strings and as an interpreter of a Turing complete language.
Is a there name for a weakened version of Cartesian closedness along these lines?
If you strengthen the property of to "for every morphism there exists such that , then it's called being "weakly cartesian closed".
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 ("weak simple products").
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.
Mike Shulman said:
If you strengthen the property of to "for every morphism there exists such that , then it's called being "weakly cartesian closed".
Ahh, that's what I expected, but somehow didn't find it!
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".
(Possibly they only talk about "weak exponentials" rather than the phrase "weakly cartesian closed".)
Or maybe even better is Jacopo Emmenegger's On the local cartesian closure of exact completions.
They emphasize the case where the category only has weak finite limits, where there's a lot more annoying bookkeeping.
You might also be interested in Turing categories