### Abstract

Original language | English |
---|---|

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 |

Publisher | Springer |

Pages | 301-315 |

Number of pages | 15 |

Volume | 2701 |

DOIs | |

Publication status | Published - 2003 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer |

### Fingerprint

### Cite this

*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). Berlin: Springer. https://doi.org/10.1007/3-540-44904-3_21

**A universal embedding for the higher order structure of computational effects.** / Power, John.

Research output: Chapter in Book/Report/Conference proceeding › Chapter

*Typed Lambda Calculi and Applications 6th International Conference, TLCA 2003 Valencia, Spain, June 10–12, 2003 Proceedings.*vol. 2701, Lecture Notes in Computer Science, Springer, Berlin, pp. 301-315. https://doi.org/10.1007/3-540-44904-3_21

}

TY - CHAP

T1 - A universal embedding for the higher order structure of computational effects

AU - Power, John

N1 - Typed lambda calculi and applications (Valencia, 2003)

PY - 2003

Y1 - 2003

N2 - 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.

AB - 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.

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

U2 - 10.1007/3-540-44904-3_21

DO - 10.1007/3-540-44904-3_21

M3 - Chapter

VL - 2701

T3 - Lecture Notes in Computer Science

SP - 301

EP - 315

BT - Typed Lambda Calculi and Applications 6th International Conference, TLCA 2003 Valencia, Spain, June 10–12, 2003 Proceedings

PB - Springer

CY - Berlin

ER -