:: (a -> c) -> (a, b) -> (c, b) package:Agda

mapFst f = f -*- id