1
------------------------------------------------------------------------
3
------------------------------------------------------------------------
5
-- Note that currently the functor laws are not included here.
7
module Category.Functor where
9
open import Data.Function
11
record RawFunctor (f : Set → Set) : Set₁ where
15
_<$>_ : ∀ {a b} → (a → b) → f a → f b
17
_<$_ : ∀ {a b} → a → f b → f a
18
x <$ y = const x <$> y