------------------------------------------------------------------------
-- 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 using (RawFunctor)
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 (f A₁.⊛ x)  (op f A₂.⊛ op x)

  op-<$> :  {i j X Y} (f : X  Y) (x : F₁ i j X) 
           op (f A₁.<$> x)  (f A₂.<$> 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