foo : (a : Type) -> (b : Type) -> a -> b
foo a a x = x