A higher-order structure is a computability model $C$ possessing a weak terminal $(I,i)$, and endowed with the following for each $A, B \in \vert C \vert$

• a choice of datatype $A \Rightarrow B \in \vert C \vert$
• a partial function $\cdot_{AB} : (A \Rightarrow B) \times A \rightharpoonup B$ (external to the structure of $C$).

The weak terminal picks out a subset $A^\#$ for each $A \in |C|$, namely the set of elements of the form $f(i)$ where $f \in C[I, A]$ and $f(i) \downarrow$.

A higher-order (computability) model is a higher-order structure $C$ satisfying the following conditions for some (or equivalently any) weak terminal $(I,i)$

1. A partial function $f : A \rightharpoonup B$ is present in $C[A,B]$ iff there exists $\hat{f} \in C[I, A \Rightarrow B]$ such that $$\hat{f}(i) \downarrow, \quad \forall a \in A. \ \hat{f}(i) \cdot a \simeq f(a)$$
2. For any $A,B \in \vert C \vert$, there exists $k_{AB} \in (A \Rightarrow B \Rightarrow A)^\#$ such that $$\forall a. \ k_{AB} \cdot a \downarrow, \quad \forall a,b. \ k_{AB} \cdot a \cdot b = a$$
3. For any $A,B,C \in \vert C \vert$, there exists $$s_{ABC} \in ((A \Rightarrow B \Rightarrow C) \Rightarrow (A \Rightarrow B) \Rightarrow (A \Rightarrow C))^\#$$ such that $$\forall f,g. \ s_{ABC} \cdot f \cdot g \downarrow, \quad \forall f,g,a. \ s_{ABC} \cdot f \cdot g \cdot a \simeq (f \cdot a) \cdot (g \cdot a)$$