Univalent Parametricity à la carte This repository contains an implementation of Univalent Parametricity with automatic translation thanks to MetaCoq. How to use TODO Example