Source code on Github
------------------------------------------------------------------------
-- The Agda standard library
--
-- Applicative functors
------------------------------------------------------------------------

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

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

module Category.Applicative where

open import Level using (Level; suc; _⊔_)
open import Data.Unit
open import Category.Applicative.Indexed

private
  variable
    f : Level

RawApplicative : (Set f  Set f)  Set (suc f)
RawApplicative F = RawIApplicative {I = } λ _ _  F

module RawApplicative {F : Set f  Set f}
                      (app : RawApplicative F) where
  open RawIApplicative app public

RawApplicativeZero : (Set f  Set f)  Set (suc f)
RawApplicativeZero F = RawIApplicativeZero {I = }  _ _  F)

module RawApplicativeZero {F : Set f  Set f}
                          (app : RawApplicativeZero F) where
  open RawIApplicativeZero app public

RawAlternative : (Set f  Set f)  Set _
RawAlternative F = RawIAlternative {I = }  _ _  F)

module RawAlternative {F : Set f  Set f}
                      (app : RawAlternative F) where
  open RawIAlternative app public