idris-0.9.5: lib/Prelude/Morphisms.idr

module Prelude.Morphisms

data Morphism : Set -> Set -> Set where
    Homo : (a -> b) -> Morphism a b

($) : Morphism a b -> a -> b
(Homo f) $ a = f a