------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed applicative functors
------------------------------------------------------------------------

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

module Category.Applicative.Indexed where

open import Category.Functor
open import Data.Product
open import Function
open import Level
open import Relation.Binary.PropositionalEquality as P using (_≡_)

IFun : ∀ {i} → Set i → (ℓ : Level) → Set _
IFun I ℓ = I → I → Set ℓ → Set ℓ

record RawIApplicative {i f} {I : Set i} (F : IFun I f) :
                       Set (i ⊔ suc f) where
  infixl 4 _⊛_ _<⊛_ _⊛>_
  infix  4 _⊗_

  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

  zipWith : ∀ {i j k A B C} → (A → B → C) → F i j A → F j k B → F i k C
  zipWith f x y = f <$> x ⊛ y

-- Applicative functor morphisms, specialised to propositional
-- equality.

record Morphism {i f} {I : Set i} {F₁ F₂ : IFun I f}
                (A₁ : RawIApplicative F₁)
                (A₂ : RawIApplicative F₂) : Set (i ⊔ suc f) where
  module A₁ = RawIApplicative A₁
  module A₂ = RawIApplicative A₂
  field
    op      : ∀ {i j X} → F₁ i j X → F₂ i j X
    op-pure : ∀ {i X} (x : X) → op (A₁.pure {i = i} x) ≡ A₂.pure x
    op-⊛    : ∀ {i j k X Y} (f : F₁ i j (X → Y)) (x : F₁ j k X) →
              op (A₁._⊛_ f x) ≡ A₂._⊛_ (op f) (op x)

  op-<$> : ∀ {i j X Y} (f : X → Y) (x : F₁ i j X) →
           op (A₁._<$>_ f x) ≡ A₂._<$>_ f (op x)
  op-<$> f x = begin
    op (A₁._⊛_ (A₁.pure f) x)       ≡⟨ op-⊛ _ _ ⟩
    A₂._⊛_ (op (A₁.pure f)) (op x)  ≡⟨ P.cong₂ A₂._⊛_ (op-pure _) P.refl ⟩
    A₂._⊛_ (A₂.pure f) (op x)       ∎
    where open P.≡-Reasoning