Abstract :
During this talk, we will first review the notion of parametricity and its application to automatic proof transport. We will then look at the framework of univalent parametricity and a new variant univalent relational parametricity which fully scales to CIC