<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. </div><div class=""><br class=""></div><div class="">However, I would like to point out that the notion of parametricity and </div><div class="">its relation to natural transformations is more than folklore. </div><div class=""><br class=""></div><div class="">It goes back to John Reynolds one of the best PL researchers. 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 <<a href="mailto:sanzhiyan@gmail.com" class="">sanzhiyan@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class="">It is FP folklore that polymorphic functions of type<br class=""><br class="">(a : Set) -> F a -> 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=""> 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=""> ≡ 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 -> x) (cong proj₁ (counter {Bool}))<br class=""> (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>