← Back to branch summary

~ubuntu-branches/ubuntu/utopic/agda-stdlib/utopic-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: 2011-05-24 10:26:15 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110524102615-9tontf43bq9ym690
Tags: 0.5-1
http://bugs.debian.org/573807
http://bugs.debian.org/598708
* [9251e0b] Imported Upstream version 0.5
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [2c82171] Add watch file
* [0518fa6] No longer need procps | hurd BD as we no longer have the ticker
* [daf2445] Don't use upstream's make install — handled ourselves by
  dh_install
* [1b86533] Update watchfile to point at new location
* [637f47d] Remove debian/gbp.conf as we are no longer building for exp
* [cc88671] Require Agda 2.2.10
* [e99dab5] Set maximum stack size to 1G to prevent overflows in the build
* [251cd1d] Run the test suite manually
* [a7db697] Set the variable in the emacs loading script properly
* [540ca3f] Improve short description
* [6b3e794] Add dependencies on compatible versions of the Agda library
* [7127678] Standards-Version bump to 3.9.2, no changes required
* [9d0ae30] Update to use ghc instead of ghc6
* [3f6879a] Set Maintainer to my d.o email address

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Category/Applicative/Indexed.agda
2
2
-- Indexed applicative functors
3
3
------------------------------------------------------------------------
4
4
 
 
5
{-# OPTIONS --universe-polymorphism #-}
 
6
 
5
7
-- Note that currently the applicative functor laws are not included
6
8
-- here.
7
9
 
8
10
module Category.Applicative.Indexed where
9
11
 
10
 
open import Data.Function
 
12
open import Category.Functor
11
13
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
 
14
open import Function
 
15
open import Level
 
16
open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
17
 
 
18
IFun : ∀ {i} → Set i → (ℓ : Level) → Set _
 
19
IFun I ℓ = I → I → Set ℓ → Set ℓ
 
20
 
 
21
record RawIApplicative {i f} {I : Set i} (F : IFun I f) :
 
22
                       Set (i ⊔ suc f) where
18
23
  infixl 4 _⊛_ _<⊛_ _⊛>_
19
24
  infix  4 _⊗_
20
25
 
40
45
 
41
46
  _⊗_ : ∀ {i j k A B} → F i j A → F j k B → F i k (A × B)
42
47
  x ⊗ y = (_,_) <$> x ⊛ y
 
48
 
 
49
  zipWith : ∀ {i j k A B C} → (A → B → C) → F i j A → F j k B → F i k C
 
50
  zipWith f x y = f <$> x ⊛ y
 
51
 
 
52
-- Applicative functor morphisms, specialised to propositional
 
53
-- equality.
 
54
 
 
55
record Morphism {i f} {I : Set i} {F₁ F₂ : IFun I f}
 
56
                (A₁ : RawIApplicative F₁)
 
57
                (A₂ : RawIApplicative F₂) : Set (i ⊔ suc f) where
 
58
  module A₁ = RawIApplicative A₁
 
59
  module A₂ = RawIApplicative A₂
 
60
  field
 
61
    op      : ∀ {i j X} → F₁ i j X → F₂ i j X
 
62
    op-pure : ∀ {i X} (x : X) → op (A₁.pure {i = i} x) ≡ A₂.pure x
 
63
    op-⊛    : ∀ {i j k X Y} (f : F₁ i j (X → Y)) (x : F₁ j k X) →
 
64
              op (A₁._⊛_ f x) ≡ A₂._⊛_ (op f) (op x)
 
65
 
 
66
  op-<$> : ∀ {i j X Y} (f : X → Y) (x : F₁ i j X) →
 
67
           op (A₁._<$>_ f x) ≡ A₂._<$>_ f (op x)
 
68
  op-<$> f x = begin
 
69
    op (A₁._⊛_ (A₁.pure f) x)       ≡⟨ op-⊛ _ _ ⟩
 
70
    A₂._⊛_ (op (A₁.pure f)) (op x)  ≡⟨ P.cong₂ A₂._⊛_ (op-pure _) P.refl ⟩
 
71
    A₂._⊛_ (A₂.pure f) (op x)       ∎
 
72
    where open P.≡-Reasoning