← Back to branch summary

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

« back to all changes in this revision

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

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 09:46:46 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805094646-zqd0c4m8ndngqg6x
Tags: 0.8-1
* [4ca6fd0] Update debian/watch to fetch tarballs from github
* [84d4313] Imported Upstream version 0.8
* [7b08243] debian/control: Require agda 2.4.x per upstream
* [37e7e10] debian/control: Standards-Version → 3.9.5, no changes required.
* [9051b9d] Run upstream's "GenerateEverything" script

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Category/Monad/Indexed.agda
14
14
 
15
15
record RawIMonad {i f} {I : Set i} (M : IFun I f) :
16
16
                 Set (i ⊔ suc f) where
17
 
  infixl 1 _>>=_ _>>_
18
 
  infixr 1 _=<<_
 
17
  infixl 1 _>>=_ _>>_ _>=>_
 
18
  infixr 1 _=<<_ _<=<_
19
19
 
20
20
  field
21
21
    return : ∀ {i A} → A → M i i A
27
27
  _=<<_ : ∀ {i j k A B} → (A → M j k B) → M i j A → M i k B
28
28
  f =<< c = c >>= f
29
29
 
 
30
  _>=>_ : ∀ {i j k a} {A : Set a} {B C} →
 
31
          (A → M i j B) → (B → M j k C) → (A → M i k C)
 
32
  f >=> g = _=<<_ g ∘ f
 
33
 
 
34
  _<=<_ : ∀ {i j k B C a} {A : Set a} →
 
35
          (B → M j k C) → (A → M i j B) → (A → M i k C)
 
36
  g <=< f = f >=> g
 
37
 
30
38
  join : ∀ {i j k A} → M i j (M j k A) → M i k A
31
39
  join m = m >>= id
32
40