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

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

    {-# OPTIONS --cubical-compatible --safe #-}

    module Effect.Functor where

    open import Data.Unit.Polymorphic.Base using (⊤)
    open import Function.Base using (const; flip)
    open import Level using (Level; suc; _⊔_)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_)

    private
      variable
        ℓ ℓ′ ℓ″ : Level
        A B X Y : Set ℓ

    record RawFunctor (F : Set ℓ → Set ℓ′) : Set (suc ℓ ⊔ ℓ′) where
      infixl 4 _<$>_ _<$_
      infixl 1 _<&>_
      field
        _<$>_ : (A → B) → F A → F B

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

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

      ignore : F A → F ⊤
      ignore = _ <$_

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

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