Mercurial > hg > Members > atton > delta_monad
comparison agda/delta/monad.agda @ 136:b6dcbe8617a9
Delete unnecessary lines
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 15 Feb 2015 10:15:10 +0900 |
parents | d205ff1e406f |
children | 2bf1fa6d2006 |
comparison
equal
deleted
inserted
replaced
135:bb0b2fb49a93 | 136:b6dcbe8617a9 |
---|---|
7 open import delta.functor | 7 open import delta.functor |
8 open import nat | 8 open import nat |
9 open import laws | 9 open import laws |
10 | 10 |
11 module delta.monad where | 11 module delta.monad where |
12 | |
13 tailDelta-is-nt : {l : Level} {A B : Set l} {n : Nat} | |
14 (f : A -> B) -> (d : Delta A (S (S n))) -> | |
15 (tailDelta {n = n} ∙ (delta-fmap f)) d ≡ ((delta-fmap f) ∙ tailDelta {n = n}) d | |
16 tailDelta-is-nt f (delta x d) = refl | |
17 | 12 |
18 | 13 |
19 tailDelta-to-tail-nt : {l : Level} {A B : Set l} (n m : Nat) | 14 tailDelta-to-tail-nt : {l : Level} {A B : Set l} (n m : Nat) |
20 (f : A -> B) (d : Delta (Delta A (S (S m))) (S n)) -> | 15 (f : A -> B) (d : Delta (Delta A (S (S m))) (S n)) -> |
21 delta-fmap tailDelta (delta-fmap (delta-fmap f) d) ≡ delta-fmap (delta-fmap f) (delta-fmap tailDelta d) | 16 delta-fmap tailDelta (delta-fmap (delta-fmap f) d) ≡ delta-fmap (delta-fmap f) (delta-fmap tailDelta d) |
38 | 33 |
39 | 34 |
40 delta-eta-is-nt : {l : Level} {A B : Set l} -> {n : Nat} | 35 delta-eta-is-nt : {l : Level} {A B : Set l} -> {n : Nat} |
41 (f : A -> B) -> (x : A) -> (delta-eta {n = n} ∙ f) x ≡ delta-fmap f (delta-eta x) | 36 (f : A -> B) -> (x : A) -> (delta-eta {n = n} ∙ f) x ≡ delta-fmap f (delta-eta x) |
42 delta-eta-is-nt {n = O} f x = refl | 37 delta-eta-is-nt {n = O} f x = refl |
43 delta-eta-is-nt {n = S O} f x = refl | |
44 delta-eta-is-nt {n = S n} f x = begin | 38 delta-eta-is-nt {n = S n} f x = begin |
45 (delta-eta ∙ f) x ≡⟨ refl ⟩ | 39 (delta-eta ∙ f) x ≡⟨ refl ⟩ |
46 delta-eta (f x) ≡⟨ refl ⟩ | 40 delta-eta (f x) ≡⟨ refl ⟩ |
47 delta (f x) (delta-eta (f x)) ≡⟨ cong (\de -> delta (f x) de) (delta-eta-is-nt f x) ⟩ | 41 delta (f x) (delta-eta (f x)) ≡⟨ cong (\de -> delta (f x) de) (delta-eta-is-nt f x) ⟩ |
48 delta (f x) (delta-fmap f (delta-eta x)) ≡⟨ refl ⟩ | 42 delta (f x) (delta-fmap f (delta-eta x)) ≡⟨ refl ⟩ |