← Back to branch summary

~ubuntu-branches/ubuntu/saucy/agda-stdlib/saucy-proposed

« back to all changes in this revision

Viewing changes to src/Category/Applicative/Indexed.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2010-01-08 23:35:09 UTC
  • Revision ID: james.westby@ubuntu.com-20100108233509-l6ejt9xji64xysfb
Tags: upstream-0.3
Import upstream version 0.3

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Category/Applicative/Indexed.agda
 
1
------------------------------------------------------------------------
 
2
-- Indexed applicative functors
 
3
------------------------------------------------------------------------
 
4
 
 
5
-- Note that currently the applicative functor laws are not included
 
6
-- here.
 
7
 
 
8
module Category.Applicative.Indexed where
 
9
 
 
10
open import Data.Function
 
11
open import Data.Product
 
12
open import Category.Functor
 
13
 
 
14
IFun : Set → Set₁
 
15
IFun I = I → I → Set → Set
 
16
 
 
17
record RawIApplicative {I : Set} (F : IFun I) : Set₁ where
 
18
  infixl 4 _⊛_ _<⊛_ _⊛>_
 
19
  infix  4 _⊗_
 
20
 
 
21
  field
 
22
    pure : ∀ {i A} → A → F i i A
 
23
    _⊛_  : ∀ {i j k A B} → F i j (A → B) → F j k A → F i k B
 
24
 
 
25
  rawFunctor : ∀ {i j} → RawFunctor (F i j)
 
26
  rawFunctor = record
 
27
    { _<$>_ = λ g x → pure g ⊛ x
 
28
    }
 
29
 
 
30
  private
 
31
    open module RF {i j : I} =
 
32
           RawFunctor (rawFunctor {i = i} {j = j})
 
33
           public
 
34
 
 
35
  _<⊛_ : ∀ {i j k A B} → F i j A → F j k B → F i k A
 
36
  x <⊛ y = const <$> x ⊛ y
 
37
 
 
38
  _⊛>_ : ∀ {i j k A B} → F i j A → F j k B → F i k B
 
39
  x ⊛> y = flip const <$> x ⊛ y
 
40
 
 
41
  _⊗_ : ∀ {i j k A B} → F i j A → F j k B → F i k (A × B)
 
42
  x ⊗ y = (_,_) <$> x ⊛ y