<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">Hi, Andrea.<div class=""><br class=""></div><div class="">I do not know much about parametricty at the dependently typed level.</div><div class="">I haven’t studied it much. &nbsp;</div><div class=""><br class=""></div><div class="">However, I would like to point out that the notion of parametricity and&nbsp;</div><div class="">its relation to natural transformations is more than folklore.&nbsp;</div><div class=""><br class=""></div><div class="">It goes back to John Reynolds one of the best PL researchers. &nbsp;See:</div><div class=""><br class=""></div><div class=""><a href="http://www.cs.bham.ac.uk/~udr/papers/logical-relations-and-parametricity.pdf" class="">http://www.cs.bham.ac.uk/~udr/papers/logical-relations-and-parametricity.pdf</a></div><div class=""><br class=""></div><div class="">For some history on the subject.</div><div class=""><br class=""></div><div class="">Very best,</div><div class="">Harley</div><div class=""><br class=""><div><blockquote type="cite" class=""><div class="">On Oct 6, 2015, at 4:24 AM, Andrea Vezzosi &lt;<a href="mailto:sanzhiyan@gmail.com" class="">sanzhiyan@gmail.com</a>&gt; wrote:</div><br class="Apple-interchange-newline"><div class="">It is FP folklore that polymorphic functions of type<br class=""><br class="">(a : Set) -&gt; F a -&gt; G a<br class=""><br class="">correspond to natural transformations via parametricity.<br class="">(Assuming F and G are "Functor"s)<br class=""><br class="">So it was a bit surprising to me that the result fails in dependent type theory.<br class=""><br class="">open import Data.Product<br class="">open import Data.Unit<br class="">open import Data.Empty<br class="">open import Data.Bool<br class="">open import Relation.Binary.PropositionalEquality<br class=""><br class="">S : Set â†’ Set₁<br class="">S X = Î£ Set \ R â†’ R â†’ X<br class=""><br class="">mapS : âˆ€ {X Y} â†’ (X â†’ Y) â†’ S X â†’ S Y<br class="">mapS f (R , g) = (R , \ x â†’ f (g x))<br class=""><br class="">eta : âˆ€ {X} â†’ S X â†’ S X<br class="">eta (R , g) = (Σ R \ r â†’ âˆ€ r' â†’ g r â‰¡ g r') , (λ x â†’ g (proj₁ x))<br class=""><br class="">postulate<br class=""> &nbsp;eta-nat : âˆ€ {X Y} â†’ (f : X â†’ Y) â†’ âˆ€ s â†’ eta (mapS f s) â‰¡ mapS f (eta s)<br class=""><br class="">counter : âˆ€ {X : Set} â†’ eta (mapS (λ _ â†’ tt) (X , (λ x â†’ x)))<br class=""> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;≡ mapS (λ _ â†’ tt) (eta (X , (λ x â†’ x)))<br class="">counter {X} = eta-nat {X} {⊤} _ (X , (λ x â†’ x))<br class=""><br class="">empty-sigma : Î£ Bool (λ r â†’ (r' : Bool) â†’ r â‰¡ r') â†’ âŠ¥<br class="">empty-sigma (b , p) with p (not b)<br class="">empty-sigma (true , p) | ()<br class="">empty-sigma (false , p) | ()<br class=""><br class="">impossible : âŠ¥<br class="">impossible = empty-sigma (subst (\ x -&gt; x) (cong proj₁ (counter {Bool}))<br class=""> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(true , (λ _ â†’ refl)))<br class="">_______________________________________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class="">https://lists.chalmers.se/mailman/listinfo/agda<br class=""></div></blockquote></div><br class=""></div></body></html>