← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to examples/outdated-and-incorrect/AIM6/Cat/lib/Logic/Structure/Monoid.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
examples/outdated-and-incorrect/AIM6/Cat/lib/Logic/Structure/Monoid.agda
1
 
 
2
 
module Logic.Structure.Monoid where
3
 
 
4
 
import Logic.Equivalence
5
 
import Logic.Operations as Operations
6
 
 
7
 
open Logic.Equivalence using (Equivalence; module Equivalence)
8
 
open Operations.Param
9
 
 
10
 
data Monoid (A : Set)(Eq : Equivalence A) : Set where
11
 
  monoid :
12
 
    (z   : A)
13
 
    (_+_ : A -> A -> A)
14
 
    (leftId : LeftIdentity Eq z _+_)
15
 
    (rightId : RightIdentity Eq z _+_)
16
 
    (assoc : Associative Eq _+_) ->
17
 
    Monoid A Eq
18
 
 
19
 
 
20
 
module Projections where
21
 
 
22
 
  zero : {A : Set}{Eq : Equivalence A} -> Monoid A Eq -> A
23
 
  zero (monoid z _ _ _ _) = z
24
 
 
25
 
  plus : {A : Set}{Eq : Equivalence A} -> Monoid A Eq -> A -> A -> A
26
 
  plus (monoid _ p _ _ _) = p
27
 
 
28
 
  leftId : {A : Set}{Eq : Equivalence A}(Mon : Monoid A Eq) -> LeftIdentity Eq (zero Mon) (plus Mon)
29
 
  leftId (monoid _ _ li _ _) = li
30
 
 
31
 
  rightId : {A : Set}{Eq : Equivalence A}(Mon : Monoid A Eq) -> RightIdentity Eq (zero Mon) (plus Mon)
32
 
  rightId (monoid _ _ _ ri _) = ri
33
 
 
34
 
  assoc : {A : Set}{Eq : Equivalence A}(Mon : Monoid A Eq) -> Associative Eq (plus Mon)
35
 
  assoc (monoid _ _ _ _ a) = a
36
 
 
37
 
module Monoid {A : Set}{Eq : Equivalence A}(Mon : Monoid A Eq) where
38
 
 
39
 
  zero    = Projections.zero Mon
40
 
  _+_     = Projections.plus Mon
41
 
  leftId  = Projections.leftId Mon
42
 
  rightId = Projections.rightId Mon
43
 
  assoc   = Projections.assoc Mon
44