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 ⟩