Mercurial > hg > Members > atton > delta_monad
comparison agda/laws.agda @ 90:55d11ce7e223
Unify levels on data type. only use suc to proofs
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 19 Jan 2015 12:11:38 +0900 |
parents | 6789c65a75bc |
children | bcd4fe52a504 |
comparison
equal
deleted
inserted
replaced
89:5411ce26d525 | 90:55d11ce7e223 |
---|---|
4 | 4 |
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} -> (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} (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} (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 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 : Level} (F G : Set l -> Set l) |
19 (functorF : Functor F) | 19 (functorF : Functor F) |
20 (functorG : Functor G) : Set (suc (l ⊔ ll)) where | 20 (functorG : Functor G) : Set (suc l) where |
21 field | 21 field |
22 natural-transformation : {A : Set l} -> F A -> G A | 22 natural-transformation : {A : Set l} -> F A -> G A |
23 field | 23 field |
24 commute : ∀ {A B} -> (f : A -> B) -> (x : F A) -> | 24 commute : ∀ {A B} -> (f : A -> B) -> (x : F A) -> |
25 natural-transformation (fmap functorF f x) ≡ fmap functorG f (natural-transformation x) | 25 natural-transformation (fmap functorF f x) ≡ fmap functorG f (natural-transformation x) |