------------------------------------------------------------------------
-- 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  _<$>_ _<$_

  field
    _<$>_ : ∀ {A B} → (A → B) → F A → F B

  _<$_ : ∀ {A B} → A → F B → F A
  x <$ y = const x <$> y