§ Theorems for free
These are personal notes I made of a custom notation for denoting the relations
from the theorems for free paper. I developed the notation since I wanted
to keep track of what types are floating around and what the relations are doing.
We interpret types as sets. If elements belong to the relation, ie, if (a, a') ∈ R ⊂ AxA
,
we will denote this as a[A R A']a'
. We will now write down some inference
rules:
 We define
ReflB
as a[Bool ReflB Bool]a
 We define
ReflI
as i[Int ReflI Int]i
 The product of two relations
[A R B]
, [X S Y]
is called as RxS
, and is defined as: (a,x)[AxX RxS BxY](b,y)
iff: ∀ abxy, a[A R B]b ∧ x[X S Y]y
.  The list space of a
[A R B]
is called [A* [A R B] B*]
, and is defined as: la[A* [A R B] B*]lb
iff: ∀ la lb, la = lb ∧ (∀ i, la[i][A R B]lb[i])
 The function space of two relations
[A R B]
, [X S Y]
is called [A>X R>S B>Y]
, and is defined as: f[A>X R>S B>Y]g
iff: ∀ a b, a[A R B]b => f(a)[X S Y]g(b)
.  The type family space of two relations is a function that takes a relation
[A R B]
and produces a new relation: g[FA  [A R B]  FB]h
. The relation takes as parameter a relation [A R B]
for each choice.  The space of relations of
∀X.F(X)
is a relation defined by: g[A>FA  ∀X.F(X) [FA [A R B] FB] B>FB]h
∀ A B R, (g A)[FA  [A R B]  FB](h B)
.
§ Parametricity theorem
The parametricity thm states that for all terms (r: R)
, we can deduce
r[R rel(R) R]r
where rel(R)
is the relation that fits the type, and is
derived from the above rules.
§ Parametricity for lists when the relation is a function:
The list space of a [A R B]
is called [A* [A R B] B*]
,
and is defined as: la[A* [A R B] B*]lb
iff:

∀ la lb, la = lb ∧ (∀ i, la[i][A R B]lb[i])
Now, let us take a special case where [A R B]
is a function δ: A > B
. That is:
If this is the case, then we can simplify the math to be:

la[A* [A R B] B*]lb <=> ∀ la lb, la = lb ∧ (∀ i, la[i][A R B]lb[i])

la[A* [A R B] B*]lb <=> ∀ la lb, la = lb ∧ (∀ i, δ(la[i]) = lb[i]

la[A* [A R B] B*]lb <=> ∀ la lb, map δ la = lb
§ Parametricity to prove rearrangements

r[∀ X. X* > X*]r

(r A)[A*>A*  [A*>A* [A R B] B*>B*]  B*>B*](r B)

as[A* [A R B] B*]bs => (r A as)[A* [A R B] B*](r B bs)
 Pick
[A R B]
to be a function δ: A > B
. Ie, a[A R B]b
iff δ(a) = b
.  This lets us convert all occrences of
α[A R B]ω
into ω = δ(α)
.  Hence,
as[A* [A R B] B*]bs
becomes map δ as = bs
.  Hence,
(r A as)[A* [A R B] B*](r B bs)
becomes map δ (r A as) = (r B bs)
 In toto, this let us replace
bs
with map δ as
. We derive: 
map δ (r A as) = (r B bs)

map δ (r A as) = (r B (map δ as)

map δ . (r A) = (r B) . map δ
 Replace
bs[i]
with δ(as[i])
to get result: δ(r A as[i]) = r B δ(as[i])
, which was indeed what we were looking for.
§ References