\(f : * -> *) -> \(b : * ) -> type Defer data Map (a : *) (k : a -> b) (x : f a) in Defer