Mercurial > hg > Members > atton > delta_monad
diff agda/laws.agda @ 126:5902b2a24abf
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 |
line wrap: on
line diff
--- a/agda/laws.agda Mon Feb 02 14:09:30 2015 +0900 +++ b/agda/laws.agda Tue Feb 03 11:45:33 2015 +0900 @@ -7,10 +7,12 @@ record Functor {l : Level} (F : Set l -> Set l) : Set (suc l) where field fmap : {A B : Set l} -> (A -> B) -> (F A) -> (F B) - field + field -- laws preserve-id : {A : Set l} (x : F A) → fmap id x ≡ id x covariant : {A B C : Set l} (f : A -> B) -> (g : B -> C) -> (x : F A) -> fmap (g ∙ f) x ≡ ((fmap g) ∙ (fmap f)) x + field -- proof assistant + 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 open Functor record NaturalTransformation {l : Level} (F G : Set l -> Set l)