Mercurial > hg > Members > atton > delta_monad
diff agda/similar.agda @ 29:e0ba1bf564dd
Apply level to some functions
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 07 Oct 2014 15:09:17 +0900 |
parents | 6e6d646d7722 |
children | c2f40b6d4027 |
line wrap: on
line diff
--- a/agda/similar.agda Tue Oct 07 14:55:40 2014 +0900 +++ b/agda/similar.agda Tue Oct 07 15:09:17 2014 +0900 @@ -1,17 +1,19 @@ open import list open import basic + +open import Level open import Relation.Binary.PropositionalEquality open ≡-Reasoning module similar where -data Similar (A : Set) : Set where +data Similar {l : Level} (A : Set l) : (Set (suc l)) where similar : List String -> A -> List String -> A -> Similar A -fmap : {A B : Set} -> (A -> B) -> (Similar A) -> (Similar B) +fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> (Similar A) -> (Similar B) fmap f (similar xs x ys y) = similar xs (f x) ys (f y) -mu : {A : Set} -> Similar (Similar A) -> Similar A +mu : {l : Level} {A : Set l} -> Similar (Similar A) -> Similar A mu (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = similar (lx ++ llx) x (ly ++ lly) y return : {A : Set} -> A -> Similar A @@ -23,10 +25,23 @@ returnSS : {A : Set} -> A -> A -> Similar A returnSS x y = similar [[ (show x) ]] x [[ (show y) ]] y +--monad-law-1 : mu ∙ (fmap mu) ≡ mu ∙ mu -monad-law-1 : mu ∙ (fmap mu) ≡ mu ∙ mu -monad-law-1 = {!!} +monad-law-1 : {l : Level} {A : Set l} -> (s : Similar (Similar (Similar A))) -> ((mu ∙ (fmap mu)) s) ≡ ((mu ∙ mu) s) +monad-law-1 s = begin + ((mu ∙ (fmap mu)) s) + ≡⟨⟩ + mu (fmap mu s) + ≡⟨ {!!} ⟩ + mu (mu s) + ≡⟨⟩ + ((mu ∙ mu) s) + ∎ + + + +{- --monad-law-2 : mu ∙ fmap return ≡ mu ∙ return ≡id monad-law-2-1 : mu ∙ fmap return ≡ mu ∙ return monad-law-2-1 = {!!} @@ -35,7 +50,8 @@ monad-law-2-2 = {!!} monad-law-3 : ∀{f} -> return ∙ f ≡ fmap f ∙ return -monad-law-3 = {!!} +monad-law-3 = {!!} monad-law-4 : ∀{f} -> mu ∙ fmap (fmap f) ≡ fmap f ∙ mu -monad-law-4 = {!!} +monad-law-4 = {!!} +-}