Samuel's Really Straightforward Proof of the Parametricity Result, extended (trivially) to dependent types.

[I'll eventually write a version which begins by explaining free theorems, but for now here's a proof for the cognoscenti]

Consider an agda expression, any typed agda expression whose type is a Set1. Here are two examples, including one using dependent types.

id : {a : Set}
   → a
   → a
id x = x

ff : {a : Set}
   → {s : a → a}
   → (F : a → Set)
   → (f : {x : a}
        → F x
        → F (s x))
   → {x : a}
   → (y : F x)
   → F (s (s x))
ff F f y = f (f y)

It is very straightforward to obtain a term, ff₁, which has the same type except that Set has been upgraded to a Set1. In fact, the expression ff already has the desired type, we just need to change its type annotation.

id₁ : {a : Set1}
    → a
    → a
id₁ x = x

ff₁ : {a : Set1}
    → {s : a → a}
    → (F : a → Set1)
    → (f : {x : a}
         → (F x)
         → (F (s x)))
    → {x : a}
    → (y : (F x))
    → (F (s (s x)))
ff₁ F f y = f (f y)

Now, let's make this change a bit more generic. Instead of fixing Set1, let's use an abstract target, Set#. Now, since agda doesn't know that Set# is a member of the Set hierarchy, the validity of the expression (x : a) does not follow from the fact that (a : Set#), as it would for (a : Set) or (a : Set1). For this reason, it is necessary to introduce the abstract type transformer (value# : Set# -> Set1), which inserts Set# into the type hierarchy.

It is very straightforward to obtain a term, ff#, which has the same type as ff except that Set has been upgraded to a Set# and value# has been inserted at the appropriate places. In fact, the expression ff already has the desired type, we again just need to change its type annotation.

id# : {a : Set#}
    → value# a
    → value# a
id# x = x

ff# : {a : Set#}
    → {s : value# a → value# a}
    → (F : value# a → Set#)
    → (f : {x : value# a}
         → value# (F x)
         → value# (F (s x)))
    → {x : value# a}
    → (y : value# (F x))
    → value# (F (s (s x)))
ff# F f y = f (f y)

And now the punchline is that ff# is precisely the proof of the free theorem for ff, using the following instantiations for Set# and result#.

record Set# : Set1 where
  field
    a  : Set
    a' : Set
    a~ : a → a' → Set

record value# (a# : Set#) : Set where
  open Set# a#
  field
    x  : a
    x' : a'
    x~ : a~ x x'

Even more free theorems can be obtained by using other instantiations. Note that in the usual formulation of the parametricity result, the type of the free theorems are usually given in a much longer, record-free form where each field is expanded into an individual parameter. It is tedious, but straightforward to convert between the two representations.

free-id' : {a : Set}
         → {a' : Set}
         → {a~ : a → a' → Set}
         → {x  : a }
         → {x' : a'}
         → a~ x x'
         → a~ (id x) (id x')
free-id' {a} {a'} {a~} {u} {u'} u~ = value#.x~ r# where
  a# : Set#
  a# = record {a = a; a' = a'; a~ = a~}

  u# : value# a#
  u# = record {x = u; x' = u'; x~ = u~}

  r# : value# a#
  r# = u#

free-ff' : {a : Set}
         → {a' : Set}
         → {a~ : a → a'
               → Set}
         → {s : a → a }
         → {s' : a' → a'}
         → {s~ : ∀ {x x'}
               → a~ x x'
               → a~ (s x) (s' x')}
         → {F : a → Set}
         → {F' : a' → Set}
         → (F~ : ∀ {x x'}
               → a~ x x'
               → F x → F' x'
               → Set)
         → {f : ∀ {x}
              → F x
              → F (s x)}
         → {f' : ∀ {x'}
               → F' x'
               → F' (s' x')}
         → (f~ : ∀ {x x' x~}
               → {y : F x }
               → {y' : F' x'}
               → F~ x~ y y'
               → F~ (s~ x~)
                    (f y) (f' y'))
         → ∀ {u u' u~}
         → {y : F u }
         → {y' : F' u'}
         → F~ u~ y y'
         → F~ (s~ (s~ u~))
              (ff F f y) (ff F' f' y')
free-ff' {a} {a'} {a~}
         {s} {s'} {s~}
         {F} {F'} F~
         {f} {f'} f~
         {u} {u'} {u~}
         {y} {y'} y~
         = value#.x~ r# where
  a# : Set#
  a# = record {a = a; a' = a'; a~ = a~}

  s# : value# a# → value# a#
  s# x# = let open value# x# in record
        { x = s x
        ; x' = s' x'
        ; x~ = s~ x~
        }

  F# : value# a# → Set#
  F# x# = let open value# x# in record
        { a = F x
        ; a' = F' x'
        ; a~ = F~ x~
        }

  f# : {x# : value# a#}
     → value# (F# x#)
     → value# (F# (s# x#))
  f# {x#} y# = let open value# y# in record
             { x = f x
             ; x' = f' x'
             ; x~ = f~ x~
             }

  u# : value# a#
  u# = record {x = u; x' = u'; x~ = u~}

  y# : value# (F# u#)
  y# = record {x = y; x' = y'; x~ = y~}

  r# : value# (F# (s# (s# u#)))
  r# = ff# F# f# y#