```module Haskell.Prim.Functor where

--------------------------------------------------
-- Functor

-- ** base
record Functor (f : Set → Set) : Set₁ where
infixl 1 _<&>_
infixl 4 _<\$>_ _<\$_ _\$>_
field
fmap : (a → b) → f a → f b
_<\$>_ : (a → b) → f a → f b
_<&>_ : f a → (a → b) → f b
_<\$_ : (@0 {{ b }} → a) → f b → f a
_\$>_ : f a → (@0 {{ a }} → b) → f b
void : f a → f ⊤
-- ** defaults
record DefaultFunctor (f : Set → Set) : Set₁ where
field fmap : (a → b) → f a → f b

infixl 1 _<&>_
infixl 4 _<\$>_ _<\$_ _\$>_

_<\$>_ : (a → b) → f a → f b
_<\$>_ = fmap

_<&>_ : f a → (a → b) → f b
m <&> f = fmap f m

_<\$_ : (@0 {{ b }} → a) → f b → f a
x <\$ m = fmap (λ b → x {{b}}) m

_\$>_ : f a → (@0 {{ a }} → b) → f b
m \$> x = x <\$ m

void : f a → f ⊤
void = tt <\$_
-- ** export
open Functor ⦃...⦄ public
{-# COMPILE AGDA2HS Functor existing-class #-}
-- ** instances
private
mkFunctor : DefaultFunctor t → Functor t
mkFunctor x = record {DefaultFunctor x}

fmap=_ : (∀ {a b} → (a → b) → f a → f b) → Functor f
fmap= x = record {DefaultFunctor (record {fmap = x})}
instance
iFunctorList : Functor List
iFunctorList = fmap= map

iFunctorMaybe : Functor Maybe
iFunctorMaybe = fmap= λ where
f Nothing  → Nothing
f (Just x) → Just (f x)

iFunctorEither : Functor (Either a)
iFunctorEither = fmap= λ where
f (Left  x) → Left x
f (Right y) → Right (f y)

iFunctorFun : Functor (λ b → a → b)
iFunctorFun = fmap= _∘_

iFunctorTuple₂ : Functor (a ×_)
iFunctorTuple₂ = fmap= λ f (x , y) → x , f y

iFunctorTuple₃ : Functor (a × b ×_)
iFunctorTuple₃ = fmap= λ where f (x , y , z) → x , y , f z

instance postulate iFunctiorIO : Functor IO
```