------------------------------------------------------------------------
-- Functors
------------------------------------------------------------------------
-- Note that currently the functor laws are not included here.
module Category.Functor where
open import Function
record RawFunctor (f : Set → Set) : Set₁ where
infixl 4 _<$>_ _<$_
field
_<$>_ : ∀ {a b} → (a → b) → f a → f b
_<$_ : ∀ {a b} → a → f b → f a
x <$ y = const x <$> y