Mercurial > hg > Members > atton > delta_monad

comparison agda/delta.agda @ 96:dfe8c67390bd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Unify Levels in delta
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 20 Jan 2015 16:25:53 +0900
parents bcd4fe52a504
children ebd0d6e2772c
comparison
equal deleted inserted replaced
95:cf372fbcebd8 96:dfe8c67390bd
30 n-tail O = id 30 n-tail O = id
31 n-tail (S n) = tailDelta ∙ (n-tail n) 31 n-tail (S n) = tailDelta ∙ (n-tail n)
32 32
33 33
34 -- Functor 34 -- Functor
35 delta-fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> (Delta A) -> (Delta B) 35 delta-fmap : {l : Level} {A B : Set l} -> (A -> B) -> (Delta A) -> (Delta B)
36 delta-fmap f (mono x) = mono (f x) 36 delta-fmap f (mono x) = mono (f x)
37 delta-fmap f (delta x d) = delta (f x) (delta-fmap f d) 37 delta-fmap f (delta x d) = delta (f x) (delta-fmap f d)
38 38
39 39
40 40
98 tailDelta (n-tail n (mono x)) ≡⟨ refl ⟩ 98 tailDelta (n-tail n (mono x)) ≡⟨ refl ⟩
99 tailDelta (n-tail n (mono x)) ≡⟨ cong (\t -> tailDelta t) (tail-delta-to-mono n x) ⟩ 99 tailDelta (n-tail n (mono x)) ≡⟨ cong (\t -> tailDelta t) (tail-delta-to-mono n x) ⟩
100 tailDelta (mono x) ≡⟨ refl ⟩ 100 tailDelta (mono x) ≡⟨ refl ⟩
101 mono x ∎ 101 mono x ∎
102 102
103 head-delta-natural-transformation : {l ll : Level} {A : Set l} {B : Set ll} 103 head-delta-natural-transformation : {l : Level} {A B : Set l}
104 -> (f : A -> B) -> (d : Delta A) -> headDelta (delta-fmap f d) ≡ f (headDelta d) 104 -> (f : A -> B) -> (d : Delta A) -> headDelta (delta-fmap f d) ≡ f (headDelta d)
105 head-delta-natural-transformation f (mono x) = refl 105 head-delta-natural-transformation f (mono x) = refl
106 head-delta-natural-transformation f (delta x d) = refl 106 head-delta-natural-transformation f (delta x d) = refl
107 107
108 n-tail-natural-transformation : {l ll : Level} {A : Set l} {B : Set ll} 108 n-tail-natural-transformation : {l : Level} {A B : Set l}
109 -> (n : Nat) -> (f : A -> B) -> (d : Delta A) -> n-tail n (delta-fmap f d) ≡ delta-fmap f (n-tail n d) 109 -> (n : Nat) -> (f : A -> B) -> (d : Delta A) -> n-tail n (delta-fmap f d) ≡ delta-fmap f (n-tail n d)
110 n-tail-natural-transformation O f d = refl 110 n-tail-natural-transformation O f d = refl
111 n-tail-natural-transformation (S n) f (mono x) = begin 111 n-tail-natural-transformation (S n) f (mono x) = begin
112 n-tail (S n) (delta-fmap f (mono x)) ≡⟨ refl ⟩ 112 n-tail (S n) (delta-fmap f (mono x)) ≡⟨ refl ⟩
113 n-tail (S n) (mono (f x)) ≡⟨ tail-delta-to-mono (S n) (f x) ⟩ 113 n-tail (S n) (mono (f x)) ≡⟨ tail-delta-to-mono (S n) (f x) ⟩