Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- -- 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
- ,
- *
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement