space (i.e. an element of ), any element of is a finite subset of and therefore also coherent, and we have Stable functions Functions between types are seen as stable functions between coherence spaces. A stable function is defined to be one which respects approximants and satisfies a certain stability axiom. Formally, is a stable function when It is monotone with respect to the subset order (respects approximation, categorically, is a functor over the poset ): It is continuous (categorically, preserves filtered colimits): where is the directed union over , the set of finite approximants of . It is stable: Categorically, this means that it preserves the pullback: Product space In order to be considered stable, functions of two arguments must satisfy the criterion 3 above in this form: which would mean that in addition to stability in each argument alone, the pullback is preserved with stable functions of two arguments. This leads to the definition of a product space which makes a bijection between stable binary functions (functions of two arguments) and stable unary functions (one argument) over the product space. The product coherence space is a product in the categorical sense i.e. it satisfies the universal property for products. It is defined by the equations: (i.e. the set of tokens of is the coproduct (or disjoint union) of the token sets of and . Tokens from differents sets are always coherent and tokens from the same set are coherent exactly when they are coherent in that set. References . . Mathematical logic