identity : (A : Set) -> A -> A
identity A x = x

identity-zero : Nat
identity-zero = identity Nat zero