### comparison agda/delta.agda @ 131:d205ff1e406fInfiniteDeltaWithMonad

Cleanup proofs
author Yasutaka Higa Tue, 03 Feb 2015 12:57:13 +0900 e6499a50ccbd 2bf1fa6d2006
comparison
equal inserted replaced
130:ac45d065cbf2 131:d205ff1e406f
1 open import Level
2 open import Relation.Binary.PropositionalEquality
3 open ≡-Reasoning
4
1 open import list 5 open import list
2 open import basic 6 open import basic
3 open import nat 7 open import nat
4 open import laws 8 open import laws
9 9
10 module delta where 10 module delta where
11 11
12 data Delta {l : Level} (A : Set l) : (Nat -> (Set l)) where 12 data Delta {l : Level} (A : Set l) : (Nat -> (Set l)) where
13 mono : A -> Delta A (S O) 13 mono : A -> Delta A (S O)
36 -- Monad (Category) 36 -- Monad (Category)
37 delta-eta : {l : Level} {A : Set l} {n : Nat} -> A -> Delta A (S n) 37 delta-eta : {l : Level} {A : Set l} {n : Nat} -> A -> Delta A (S n)
38 delta-eta {n = O} x = mono x 38 delta-eta {n = O} x = mono x
39 delta-eta {n = (S n)} x = delta x (delta-eta {n = n} x) 39 delta-eta {n = (S n)} x = delta x (delta-eta {n = n} x)
40 40
44 delta-mu : {l : Level} {A : Set l} {n : Nat} -> (Delta (Delta A (S n)) (S n)) -> Delta A (S n) 41 delta-mu : {l : Level} {A : Set l} {n : Nat} -> (Delta (Delta A (S n)) (S n)) -> Delta A (S n)
45 delta-mu (mono x) = x 42 delta-mu (mono x) = x
46 delta-mu (delta x d) = delta (headDelta x) (delta-mu (delta-fmap tailDelta d)) 43 delta-mu (delta x d) = delta (headDelta x) (delta-mu (delta-fmap tailDelta d))
47 44
48 delta-bind : {l : Level} {A B : Set l} {n : Nat} -> (Delta A (S n)) -> (A -> Delta B (S n)) -> Delta B (S n) 45 delta-bind : {l : Level} {A B : Set l} {n : Nat} -> (Delta A (S n)) -> (A -> Delta B (S n)) -> Delta B (S n)
49 delta-bind d f = delta-mu (delta-fmap f d) 46 delta-bind d f = delta-mu (delta-fmap f d)
54 47
55 {- 48 {-