### Abstract

Language | English |
---|---|

Pages | 810–827 |

Number of pages | 18 |

Journal | Mathematical Structures in Computer Science |

Volume | 29 |

Issue number | 6 |

Early online date | 22 Mar 2019 |

DOIs | |

Publication status | Published - 30 Jun 2019 |

### Fingerprint

### Keywords

- categorical semantics
- comprehension categories
- relational parametricity

### Cite this

}

*Mathematical Structures in Computer Science*, vol. 29, no. 6, pp. 810–827. https://doi.org/10.1017/S0960129518000336

**Universal properties for universal types in bifibrational parametricity.** / Ghani, Neil; Nordvall Forsberg, Fredrik; Orsanigo, Federico.

Research output: Contribution to journal › Article

TY - JOUR

T1 - Universal properties for universal types in bifibrational parametricity

AU - Ghani, Neil

AU - Nordvall Forsberg, Fredrik

AU - Orsanigo, Federico

PY - 2019/6/30

Y1 - 2019/6/30

N2 - In the 1980s, John Reynolds postulated that a parametrically polymorphic function is an ad-hoc polymorphic function satisfying a uniformity principle. This allowed him to prove that his set-theoretic semantics has a relational lifting which satisfies the Identity Extension Lemma and the Abstraction Theorem. However, his definition (and subsequent variants) has only been given for specific models. In contrast, we give a model-independent axiomatic treatment by characterising Reynolds’ definition via a universal property, and show that the above results follow from this universal property in the axiomatic setting.

AB - In the 1980s, John Reynolds postulated that a parametrically polymorphic function is an ad-hoc polymorphic function satisfying a uniformity principle. This allowed him to prove that his set-theoretic semantics has a relational lifting which satisfies the Identity Extension Lemma and the Abstraction Theorem. However, his definition (and subsequent variants) has only been given for specific models. In contrast, we give a model-independent axiomatic treatment by characterising Reynolds’ definition via a universal property, and show that the above results follow from this universal property in the axiomatic setting.

KW - categorical semantics

KW - comprehension categories

KW - relational parametricity

U2 - 10.1017/S0960129518000336

DO - 10.1017/S0960129518000336

M3 - Article

VL - 29

SP - 810

EP - 827

JO - Mathematical Structures in Computer Science

T2 - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

SN - 0960-1295

IS - 6

ER -