# Universal properties for universal types in bifibrational parametricity

MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE（2019）

Abstract

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.

MoreTranslated text

Key words

Relational parametricity,categorical semantics,comprehension categories

AI Read Science

Must-Reading Tree

Example

Generate MRT to find the research sequence of this paper

Chat Paper

Summary is being generated by the instructions you defined