We give a universal embedding of the semantics for the first order fragment of the computational λ-calculus into a semantics for the whole calculus. In category theoretic terms, which are the terms of the paper, this means we give a universal embedding of every small Freyd-category into a closed Freyd-category. The universal property characterises the embedding as the free completion of the Freyd-category as ca [→, Set]-enriched category under conical colimits. This embedding extends the usual Yoneda embedding of a small category with finite products into its free cocompletion, i.e., the usual category theoretic embedding of a model of the first order fragment of the simply typed λ-calculus into a model for the whole calculus, and similarly for the linear λ-calculus. It agrees with an embedding previously given in an ad hoc way without a universal property, so it shows the definitiveness of that construction.
|Title of host publication||Typed Lambda Calculi and Applications 6th International Conference, TLCA 2003 Valencia, Spain, June 10–12, 2003 Proceedings|
|Place of Publication||Berlin|
|Number of pages||15|
|Publication status||Published - 2003|
|Name||Lecture Notes in Computer Science|
Power, J. (2003). A universal embedding for the higher order structure of computational effects. In Typed Lambda Calculi and Applications 6th International Conference, TLCA 2003 Valencia, Spain, June 10–12, 2003 Proceedings (Vol. 2701, pp. 301-315). (Lecture Notes in Computer Science). Springer. https://doi.org/10.1007/3-540-44904-3_21