------------------------------------------------------------------------
-- The Agda standard library
--
-- Functors
------------------------------------------------------------------------

-- Note that currently the functor laws are not included here.

{-# OPTIONS --without-K --safe #-}

module Category.Functor where

open import Function
open import Level

open import Relation.Binary.PropositionalEquality

record RawFunctor {} (F : Set   Set ) : Set (suc ) where
  infixl 4 _<$>_ _<$_
  infixl 1 _<&>_

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

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

  _<&>_ :  {A B}  F A  (A  B)  F B
  _<&>_ = flip _<$>_

-- A functor morphism from F₁ to F₂ is an operation op such that
-- op (F₁ f x) ≡ F₂ f (op x)

record Morphism {} {F₁ F₂ : Set   Set }
                (fun₁ : RawFunctor F₁)
                (fun₂ : RawFunctor F₂) : Set (suc ) where
  open RawFunctor
  field
    op     : ∀{X}  F₁ X  F₂ X
    op-<$> : ∀{X Y} (f : X  Y) (x : F₁ X) 
             op (fun₁ ._<$>_ f x)  fun₂ ._<$>_ f (op x)