Definition. Map_eq
Map X Y = {f | map f X Y}