# A universal embedding for the higher order structure of computational effects

### Reference:

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.* Berlin: Springer, pp. 301-315. (Lecture Notes in Computer Science)

### Related documents:

This repository does not currently have the full-text of this item.You may be able to access a copy if URLs are provided below.

### Official URL:

http://dx.doi.org/10.1007/3-540-44904-3_21

### Abstract

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.

### Details

Item Type | Book Sections |

Creators | Power, J. |

DOI | 10.1007/3-540-44904-3_21 |

Departments | Faculty of Science > Computer Science |

Status | Published |

ID Code | 5520 |

Additional Information | Typed lambda calculi and applications (Valencia, 2003) |

### Export

### Actions (login required)

View Item |