Mercurial > hg > Members > atton > delta_monad

comparison agda/laws.agda @ 87:6789c65a75bc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Split functor-proofs into delta.functor
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 19 Jan 2015 11:00:34 +0900
parents 5c083ddd73ed
children 55d11ce7e223
comparison
equal deleted inserted replaced
86:5c083ddd73ed 87:6789c65a75bc
8 field 8 field
9 fmap : ∀{A B} -> (A -> B) -> (F A) -> (F B) 9 fmap : ∀{A B} -> (A -> B) -> (F A) -> (F B)
10 field 10 field
11 preserve-id : ∀{A} (x : F A) → fmap id x ≡ id x 11 preserve-id : ∀{A} (x : F A) → fmap id x ≡ id x
12 covariant : ∀{A B C} (f : A -> B) -> (g : B -> C) -> (x : F A) 12 covariant : ∀{A B C} (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 open Functor 14 open Functor
15 15
16 16
17 17
18 record NaturalTransformation {l ll : Level} (F G : Set l -> Set l) 18 record NaturalTransformation {l ll : Level} (F G : Set l -> Set l)