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