← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda-stdlib/raring

« back to all changes in this revision

Viewing changes to src/Category/Functor.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2011-02-25 22:28:40 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110225222840-jt16gl302kca7h0g
Tags: 0.5-1~ubuntu1
https://launchpad.net/bugs/725364
http://bugs.debian.org/573807
http://bugs.debian.org/598708

* Upload to Ubuntu from Debian's VCS due to delays in unstable caused by
  the GHC 7 transition (LP: #725364)
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [0fb0600] Standards-Version → 3.9.1, no changes required
* [d3f13b8] Update required Agda version to 2.2.8
* [cc1f5c8] Imported Upstream version 0.4
* [2c82171] Add watch file
* [9251e0b] Imported Upstream version 0.5
* [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

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Category/Functor.agda
2
2
-- Functors
3
3
------------------------------------------------------------------------
4
4
 
 
5
{-# OPTIONS --universe-polymorphism #-}
 
6
 
5
7
-- Note that currently the functor laws are not included here.
6
8
 
7
9
module Category.Functor where
8
10
 
9
 
open import Data.Function
 
11
open import Function
 
12
open import Level
10
13
 
11
 
record RawFunctor (f : Set → Set) : Set₁ where
 
14
record RawFunctor {ℓ} (F : Set ℓ → Set ℓ) : Set (suc ℓ) where
12
15
  infixl 4 _<$>_ _<$_
13
16
 
14
17
  field
15
 
    _<$>_ : ∀ {a b} → (a → b) → f a → f b
 
18
    _<$>_ : ∀ {A B} → (A → B) → F A → F B
16
19
 
17
 
  _<$_ : ∀ {a b} → a → f b → f a
 
20
  _<$_ : ∀ {A B} → A → F B → F A
18
21
  x <$ y = const x <$> y