module Prelude.Functor where

open import Agda.Primitive
open import Prelude.Function

record Functor {a b} (F : Set a  Set b) : Set (lsuc a  b) where
  infixl 4 _<$>_ _<$_
  field
    fmap :  {A B}  (A  B)  F A  F B
  _<$>_ = fmap

  _<$_ :  {A B}  A  F B  F A
  x <$ m = fmap (const x) m

open Functor {{...}} public