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" 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!

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!