-- Parametricity, relevance and erasure
-----------------------------------------

-- In uAgda every term is assumed to be parametric.
-- hence for an arbitrary function f...
\(A : *) (B : *) (f : A -> B) -> (

-- we can use the fact that it is parametric by using the postfix '!' operator:
fparam = f! : (x : A<) -> A! x -> B! (f< x),


-- Note that the "x" an irrelevant argument to f!. We say that it lies
-- in another relevance world. This is indicated by the postfix <
-- after its type.

-- that is ok, because we can always convert a term into a copy of it at 
-- a less relevant level (using that operator).


-- It is also possible to erase all the stuff less relevant than a
-- certain world by using the operator '%'. For example, after
-- erasing all the (level one) irrelevant stuff from the above type we
-- recover the original (check the normal form):

eraseType = ((x : A<) -> A! x -> B! (f< x)) % 1,


-- Indeed, f!%1 = f.
fAgain = fparam %1,


-- We can get binary parametricity by combination of unary
-- parametricity and erasure. See the following reference for
-- the explanation:

-- https://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=127466

fparam2 = f!!%2 : (x y : A<) -> A!!%2 x y -> B!!%2 (f< x) (f< y),


*)