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

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

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

    module Effect.Applicative.Indexed where

    open import Effect.Functor using (RawFunctor)
    open import Data.Product.Base using (_×_; _,_)
    open import Function.Base using (const; constᵣ)
    open import Level using (Level; suc; _⊔_)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
    open import Relation.Binary.PropositionalEquality.Properties
      using (module ≡-Reasoning)

    private
      variable
        a b c i f : Level
        A : Set a
        B : Set b
        C : Set c

    IFun : Set i → (ℓ : Level) → Set (i ⊔ suc ℓ)
    IFun I ℓ = I → I → Set ℓ → Set ℓ

    ------------------------------------------------------------------------
    -- Type, and usual combinators

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

      field
        pure : ∀ {i} → A → F i i A
        _⊛_  : ∀ {i j k} → 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} → F i j A → F j k B → F i k A
      x <⊛ y = const <$> x ⊛ y

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

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

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

      zip : ∀ {i j k} → F i j A → F j k B → F i k (A × B)
      zip = zipWith _,_

    ------------------------------------------------------------------------
    -- Applicative with a zero

    record RawIApplicativeZero
           {I : Set i} (F : IFun I f) :
           Set (i ⊔ suc f) where
      field
        applicative : RawIApplicative F
        ∅           : ∀ {i j} → F i j A

      open RawIApplicative applicative public

    ------------------------------------------------------------------------
    -- Alternative functors: `F i j A` is a monoid

    record RawIAlternative
           {I : Set i} (F : IFun I f) :
           Set (i ⊔ suc f) where
      infixr 3 _∣_
      field
        applicativeZero : RawIApplicativeZero F
        _∣_             : ∀ {i j} → F i j A → F i j A → F i j A

      open RawIApplicativeZero applicativeZero public

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

    record Morphism {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} → F₁ i j A → F₂ i j A
        op-pure : ∀ {i} (x : A) → op (A₁.pure {i = i} x) ≡ A₂.pure x
        op-⊛    : ∀ {i j k} (f : F₁ i j (A → B)) (x : F₁ j k A) →
                  op (f A₁.⊛ x) ≡ (op f A₂.⊛ op x)

      op-<$> : ∀ {i j} (f : A → B) (x : F₁ i j A) →
               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)  ≡⟨ cong₂ A₂._⊛_ (op-pure _) refl ⟩
        A₂._⊛_ (A₂.pure f) (op x)       ∎
        where open ≡-Reasoning