------------------------------------------------------------------------
-- Functors
------------------------------------------------------------------------
{-# OPTIONS --universe-polymorphism #-}
-- 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