------------------------------------------------------------------------ -- The Agda standard library -- -- Functors ------------------------------------------------------------------------ -- Note that currently the functor laws are not included here. module Category.Functor where open import Function open import Level record RawFunctor {ℓ} (F : Set ℓ → Set ℓ) : Set (suc ℓ) where infixl 4 _<$>_ _<$_ field _<$>_ : ∀ {A B} → (A → B) → F A → F B _<$_ : ∀ {A B} → A → F B → F A x <$ y = const x <$> y