identity : (A : Set) @$\rightarrow$@ A @$\rightarrow$@ A
identity A x = x

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