← 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/Predicate.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/Applicative/Predicate.agda
 
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
 
4
-- Applicative functors on indexed sets (predicates)
 
5
------------------------------------------------------------------------
 
6
 
 
7
-- Note that currently the applicative functor laws are not included
 
8
-- here.
 
9
 
 
10
module Category.Applicative.Predicate where
 
11
 
 
12
open import Category.Functor.Predicate
 
13
open import Data.Product
 
14
open import Function
 
15
open import Level
 
16
open import Relation.Unary
 
17
open import Relation.Unary.PredicateTransformer using (Pt)
 
18
 
 
19
------------------------------------------------------------------------
 
20
 
 
21
record RawPApplicative {i ℓ} {I : Set i} (F : Pt I ℓ) :
 
22
                       Set (i ⊔ suc ℓ) where
 
23
  infixl 4 _⊛_ _<⊛_ _⊛>_
 
24
  infix  4 _⊗_
 
25
 
 
26
  field
 
27
    pure : ∀ {P} → P ⊆ F P
 
28
    _⊛_  : ∀ {P Q} → F (P ⇒ Q) ⊆ F P ⇒ F Q
 
29
 
 
30
  rawPFunctor : RawPFunctor F
 
31
  rawPFunctor = record
 
32
    { _<$>_ = λ g x → pure g ⊛ x
 
33
    }
 
34
 
 
35
  private
 
36
    open module RF = RawPFunctor rawPFunctor public
 
37
 
 
38
  _<⊛_ : ∀ {P Q} → F P ⊆ const (∀ {j} → F Q j) ⇒ F P
 
39
  x <⊛ y = const <$> x ⊛ y
 
40
 
 
41
  _⊛>_ : ∀ {P Q} → const (∀ {i} → F P i) ⊆ F Q ⇒ F Q
 
42
  x ⊛> y = flip const <$> x ⊛ y
 
43
 
 
44
  _⊗_ : ∀ {P Q} → F P ⊆ F Q ⇒ F (P ∩ Q)
 
45
  x ⊗ y = (_,_) <$> x ⊛ y
 
46
 
 
47
  zipWith : ∀ {P Q R} → (P ⊆ Q ⇒ R) → F P ⊆ F Q ⇒ F R
 
48
  zipWith f x y = f <$> x ⊛ y