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)