# CCCs, computational calculi and point-surjectivity

The models of some computational calculi are in a correspondence with Cartesian Closed Categories with an object $$U$$ that has some relationship to its exponential object $$U^U$$ e.g. a retraction between $$U$$ and $$U^U$$ gives $$\lambda$$-algebra whereas those with enough points and $$U \cong U^U$$ admitting extensionality

One possible relationship between $$U$$ and $$U^U$$ is (weak) point-surjectivity which is defined as there existing a function $$\phi : U \rightarrow U^U$$ such that for all points $$p: 1 \rightarrow U^U$$, there exists a point $$u : 1 \rightarrow U$$ and $$\phi \circ u = p$$.

This relationship is relevant to $$\lambda$$-calculi as the $$F: D \rightarrow D^D$$ sided arrow in the retraction for lambda models and in the isomorphism can be seen to be point-surjective. Furthermore point-surjectivity appears in Lawvere's Fixed Point Theorem which can be used to derive the First-Fixed-Point theorem for the (I have written a derivation here however it has been rushed so apologies for mistakes).

A question that I have been contemplating is whether point-surjectivity corresponds to any existing class of automata or combinatorial calculi. Longo and Moggi in "A Category-Theoretic Characterization of Functional Completeness" (https://doi.org/10.1016/0304-3975(90)90122-X) outline the categorical models associated with combinatory algebras however it is not immediately obvious to me whether we point-surjectivity corresponds to this formulation however my intuition says otherwise. I have managed to derive several combinators in an applicative structure induced by a point-surjective $$F: U \rightarrow U^U$$ in the standard way as outlined in Chapter 5 of Barendregt's "The Lambda Calculus: It's Syntax and Semantics". These are the Mockingbird combinator $$\textbf{M} x = x x$$, the Identity combinator $$\textbf{I} x = x$$, and the combinator $$\textbf{F} x y = y$$. Derivations can be found here. I am unsure if this is an exhaustive list of the combinators that can be derived or if this set has any meaningful interpretation.

Any guidance or insights would be greatly welcomed!