uAgda-1.1.0.0: 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.

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 (\y -> Eq A x y) x (\_ p -> p)
      : Theorem
,
#