Applicative structure

Definition

Let $L$ be a typed language. An applicative structure for $L$ is a pair $(A,App)$ where $A$ is a family of sets $A^{\sigma }$ for each type $\sigma$, and $App$ is a family of functions ${App}^{\sigma ,\sigma \to \tau }:A^{\sigma }\times A^{\sigma \to \tau }\to A^{\tau }$ for each pair of types $\sigma ,\sigma \to \tau$