uAgda-1.1.0.0: tutorial/03-Parametricity.ua

-- 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),

-- 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)) % 0,


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


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

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

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


*)