------------------------------------------------------------------------
-- Indexed applicative functors
------------------------------------------------------------------------

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

module Category.Applicative.Indexed where

open import Function
open import Data.Product
open import Category.Functor

IFun : Set → Set₁
IFun I = I → I → Set → Set

record RawIApplicative {I : Set} (F : IFun I) : Set₁ where
  infixl  _⊛_ _<⊛_ _⊛>_
  infix   _⊗_

  field
    pure : ∀ {i A} → A → F i i A
    _⊛_  : ∀ {i j k A B} → F i j (A → B) → F j k A → F i k B

  rawFunctor : ∀ {i j} → RawFunctor (F i j)
  rawFunctor = record
    { _<$>_ = λ g x → pure g ⊛ x
    }

  private
    open module RF {i j : I} =
           RawFunctor (rawFunctor {i = i} {j = j})
           public

  _<⊛_ : ∀ {i j k A B} → F i j A → F j k B → F i k A
  x <⊛ y = const <$> x ⊛ y

  _⊛>_ : ∀ {i j k A B} → F i j A → F j k B → F i k B
  x ⊛> y = flip const <$> x ⊛ y

  _⊗_ : ∀ {i j k A B} → F i j A → F j k B → F i k (A × B)
  x ⊗ y = (_,_) <$> x ⊛ y