Mercurial > hg > Members > atton > delta_monad

comparison agda/laws.agda @ 126:5902b2a24abf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove mu-is-nt for DeltaM with fmap-equiv
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 Feb 2015 11:45:33 +0900
parents 673e1ca0d1a9
children d205ff1e406f
comparison
equal deleted inserted replaced
125:6dcc68ef8f96 126:5902b2a24abf
5 module laws where 5 module laws where
6 6
7 record Functor {l : Level} (F : Set l -> Set l) : Set (suc l) where 7 record Functor {l : Level} (F : Set l -> Set l) : Set (suc l) where
8 field 8 field
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 -- laws
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 -- proof assistant
15 fmap-equiv : {A B : Set l} {f g : A -> B} -> ((x : A) -> f x ≡ g x) -> (fx : F A) -> fmap f fx ≡ fmap g fx
14 open Functor 16 open Functor
15 17
16 record NaturalTransformation {l : Level} (F G : Set l -> Set l) 18 record NaturalTransformation {l : Level} (F G : Set l -> Set l)
17 {fmapF : {A B : Set l} -> (A -> B) -> (F A) -> (F B)} 19 {fmapF : {A B : Set l} -> (A -> B) -> (F A) -> (F B)}
18 {fmapG : {A B : Set l} -> (A -> B) -> (G A) -> (G B)} 20 {fmapG : {A B : Set l} -> (A -> B) -> (G A) -> (G B)}