uAgda-1.0.0.2: tutorial/03.1-Parametricity-Use.ua

-- let's use parametricity in a useful way: prove that any
-- function of type (X : *) -> X -> X is the identity.

-- To simplify the example we use impredicativity here, use
-- the -I flag to enable it.

Eq = \A a b -> (P : A -> *) -> P a -> P b
   : (A : *<) -> A -> A -> *
   ,

Theorem = 
  (f : (A : *) -> A -> A) ->
  (A : *) ->
  (x : A) ->
  Eq A< x< (f A x)<,


proof = \(f : (A : *) -> (a : A) -> A) ->
        \(A : *) ->
        \(x : A) -> f! A< (Eq A< x<) x< (\_ p -> p)
      : Theorem


,
*