path: root/src/Data/Maybe/Properties.idr

module Data.Maybe.Properties

export
mapFusion : (s : Maybe a) -> (f . g) <$> s = f <$> [| g s |]
mapFusion Nothing = Refl
mapFusion (Just x) = Refl