From fa7db502a9ceb98a44a49811d799cdeb901e1f6c Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Thu, 1 Aug 2024 02:35:58 -0400 Subject: [PATCH] fix link to univalent parametricity --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 349a6a6..a327eb0 100644 --- a/README.md +++ b/README.md @@ -29,7 +29,7 @@ variant, and computing a proof that proves the corresponding implication. The plugin features a hierarchy of structures on relations, whose instances are computed from registered user-defined proof via parametricity. This hierarchy ranges from structure-less relations to an original formulation of type equivalence. The resulting framework generalizes [raw parametricity](https://arxiv.org/abs/1209.6336), -[univalent parametricity](https://arxiv.org/abs/1209.6336) and +[univalent parametricity](https://doi.org/10.1145/3429979) and [CoqEAL](https://github.com/coq-community/coqeal), and includes them in a unified framework. The plugin computes a parametricity translation "à la carte", by performing a fine-grained analysis of the requires properties for a given proof of relatedness. In particular, it is able to prove implications without resorting to full-blown type equivalence, allowing this way to perform