Mercurial > hg > Members > atton > delta_monad

comparison agda/laws.agda @ 113:47f144540d51

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Delte trying code
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Fri, 30 Jan 2015 21:59:06 +0900
parents 0a3b6cb91a05
children e6bcc7467335
comparison
equal deleted inserted replaced
112:0a3b6cb91a05 113:47f144540d51
9 fmap : {A B : Set l} -> (A -> B) -> (F A) -> (F B) 9 fmap : {A B : Set l} -> (A -> B) -> (F A) -> (F B)
10 field 10 field
11 preserve-id : {A : Set l} (x : F A) → fmap id x ≡ id x 11 preserve-id : {A : Set l} (x : F A) → fmap id x ≡ id x
12 covariant : {A B C : Set l} (f : A -> B) -> (g : B -> C) -> (x : F A) 12 covariant : {A B C : Set l} (f : A -> B) -> (g : B -> C) -> (x : F A)
13 -> fmap (g ∙ f) x ≡ ((fmap g) ∙ (fmap f)) x 13 -> fmap (g ∙ f) x ≡ ((fmap g) ∙ (fmap f)) x
14 field
15 fmap-equiv : {A B : Set l} {f g : A -> B} -> ((x : A) -> f x ≡ g x) -> (x : F A) -> fmap f x ≡ fmap g x
16 open Functor 14 open Functor
17 15
18 record NaturalTransformation {l : Level} (F G : {l' : Level} -> Set l' -> Set l') 16 record NaturalTransformation {l : Level} (F G : {l' : Level} -> Set l' -> Set l')
19 {fmapF : {A B : Set l} -> (A -> B) -> (F A) -> (F B)} 17 {fmapF : {A B : Set l} -> (A -> B) -> (F A) -> (F B)}
20 {fmapG : {A B : Set l} -> (A -> B) -> (G A) -> (G B)} 18 {fmapG : {A B : Set l} -> (A -> B) -> (G A) -> (G B)}