------------------------------------------------------------------------ -- The Agda standard library -- -- Indexed applicative functors ------------------------------------------------------------------------ -- Note that currently the applicative functor laws are not included -- here. {-# OPTIONS --without-K --safe #-} module Category.Applicative.Indexed where open import Category.Functor using (RawFunctor) open import Data.Product using (_×_; _,_) open import Function hiding (Morphism) open import Level open import Relation.Binary.PropositionalEquality as P using (_≡_) 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) ≡⟨ P.cong₂ A₂._⊛_ (op-pure _) P.refl A₂._⊛_ (A₂.pure f) (op x) where open P.≡-Reasoning