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

{-# OPTIONS --universe-polymorphism #-}

-- 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