Mercurial > hg > Members > atton > delta_monad

annotate agda/deltaM/monad.agda @ 124:48b44bd85056

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix proof natural transformation for deltaM-eta
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 02 Feb 2015 13:12:49 +0900
parents 53cb21845dea
children 6dcc68ef8f96
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
98
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Relation.Binary.PropositionalEquality
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open ≡-Reasoning
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import basic
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import delta
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import delta.functor
111
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
8 open import delta.monad
98
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import deltaM
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import deltaM.functor
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
11 open import nat
98
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import laws
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 module deltaM.monad where
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 open Functor
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 open NaturalTransformation
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 open Monad
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
20 -- sub proofs
114
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
21
117
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
22 deconstruct-id : {l : Level} {A : Set l} {n : Nat}
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
23 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
24 (d : DeltaM M A (S n)) -> deltaM (unDeltaM d) ≡ d
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
25 deconstruct-id {n = O} (deltaM x) = refl
117
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
26 deconstruct-id {n = S n} (deltaM x) = refl
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
27
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
28
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
29 headDeltaM-with-appendDeltaM : {l : Level} {A : Set l} {n m : Nat}
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
30 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
31 (d : DeltaM M A (S n)) -> (ds : DeltaM M A (S m)) ->
117
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
32 headDeltaM (appendDeltaM d ds) ≡ headDeltaM d
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
33 headDeltaM-with-appendDeltaM {l} {A} {O} {O} (deltaM (mono _)) (deltaM _) = refl
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
34 headDeltaM-with-appendDeltaM {l} {A} {O} {S m} (deltaM (mono _)) (deltaM _) = refl
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
35 headDeltaM-with-appendDeltaM {l} {A} {S n} {O} (deltaM (delta _ _)) (deltaM _) = refl
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
36 headDeltaM-with-appendDeltaM {l} {A} {S n} {S m} (deltaM (delta _ _)) (deltaM _) = refl
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
37
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
38
117
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
39
114
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
40 fmap-headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat}
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
41 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
42 (x : T A) -> (fmap F ((headDeltaM {n = n} {M = M}) ∙ deltaM-eta) x) ≡ fmap F (eta M) x
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
43 fmap-headDeltaM-with-deltaM-eta {n = O} x = refl
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
44 fmap-headDeltaM-with-deltaM-eta {n = S n} x = refl
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
45
114
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
46
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
47
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
48 fmap-tailDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat}
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
49 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
50 (d : DeltaM M A (S n)) ->
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
51 deltaM-fmap ((tailDeltaM {n = n} {M = M} ) ∙ deltaM-eta) d ≡ deltaM-fmap (deltaM-eta) d
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
52 fmap-tailDeltaM-with-deltaM-eta {n = O} d = refl
114
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
53 fmap-tailDeltaM-with-deltaM-eta {n = S n} d = refl
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
54
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
55
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
56
118
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
57 fmap-headDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat}
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
58 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
59 (x : T (DeltaM M (DeltaM M A (S n)) (S n))) ->
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
60 fmap F (headDeltaM ∙ deltaM-mu) x ≡ fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x
118
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
61 fmap-headDeltaM-with-deltaM-mu {n = O} x = refl
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
62 fmap-headDeltaM-with-deltaM-mu {n = S n} x = refl
114
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
63
118
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
64
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
65 fmap-tailDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat}
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
66 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
67 (d : DeltaM M (DeltaM M (DeltaM M A (S (S n))) (S (S n))) (S n)) ->
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
68 deltaM-fmap (tailDeltaM ∙ deltaM-mu) d ≡ deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) d
118
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
69 fmap-tailDeltaM-with-deltaM-mu {n = O} (deltaM (mono x)) = refl
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
70 fmap-tailDeltaM-with-deltaM-mu {n = S n} (deltaM d) = refl
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
71
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
72
117
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
73
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
74
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
75
114
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
76 -- main proofs
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
77
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
78 deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat}
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
79 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
114
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
80 (f : A -> B) -> (x : A) ->
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
81 ((deltaM-eta {l} {B} {n} {T} {F} {M} )∙ f) x ≡ deltaM-fmap f (deltaM-eta x)
114
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
82 deltaM-eta-is-nt {l} {A} {B} {O} {M} {fm} {mm} f x = begin
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
83 deltaM-eta {n = O} (f x) ≡⟨ refl ⟩
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
84 deltaM (mono (eta mm (f x))) ≡⟨ cong (\de -> deltaM (mono de)) (eta-is-nt mm f x) ⟩
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
85 deltaM (mono (fmap fm f (eta mm x))) ≡⟨ refl ⟩
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
86 deltaM-fmap f (deltaM-eta {n = O} x) ∎
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
87 deltaM-eta-is-nt {l} {A} {B} {S n} {M} {fm} {mm} f x = begin
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
88 deltaM-eta {n = S n} (f x)
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
89 ≡⟨ refl ⟩
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
90 deltaM (delta-eta {n = S n} (eta mm (f x)))
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
91 ≡⟨ refl ⟩
114
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
92 deltaM (delta (eta mm (f x)) (delta-eta (eta mm (f x))))
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
93 ≡⟨ cong (\de -> deltaM (delta de (delta-eta de))) (eta-is-nt mm f x) ⟩
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
94 deltaM (delta (fmap fm f (eta mm x)) (delta-eta (fmap fm f (eta mm x))))
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
95 ≡⟨ cong (\de -> deltaM (delta (fmap fm f (eta mm x)) de)) (eta-is-nt delta-is-monad (fmap fm f) (eta mm x)) ⟩
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
96 deltaM (delta (fmap fm f (eta mm x)) (delta-fmap (fmap fm f) (delta-eta (eta mm x))))
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
97 ≡⟨ refl ⟩
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
98 deltaM-fmap f (deltaM-eta {n = S n} x)
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
99 ∎
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
100
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
101
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
102 {-
102
9c62373bd474 Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
103
118
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
104 postulate deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat}
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
105 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
106 (f : A -> B) ->
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
107 (d : DeltaM T {F} {M} (DeltaM T A (S n)) (S n)) ->
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
108 deltaM-fmap f (deltaM-mu d) ≡ deltaM-mu (deltaM-fmap (deltaM-fmap f) d)
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
109
112
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
110 postulate deltaM-right-unity-law : {l : Level} {A : Set l}
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
111 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} {n : Nat}
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
112 (d : DeltaM M {functorM} {monadM} A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
113 {-
111
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
114 deltaM-right-unity-law {l} {A} {M} {fm} {mm} {O} (deltaM (mono x)) = begin
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
115 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
116 deltaM-mu (deltaM (mono (eta mm (deltaM (mono x))))) ≡⟨ refl ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
117 deltaM (mono (mu mm (fmap fm (headDeltaM {M = M})(eta mm (deltaM (mono x))))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
118 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (eta-is-nt mm headDeltaM (deltaM (mono x)) )) ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
119 deltaM (mono (mu mm (eta mm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) (deltaM (mono x)))))) ≡⟨ refl ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
120 deltaM (mono (mu mm (eta mm x))) ≡⟨ cong (\de -> deltaM (mono de)) (sym (right-unity-law mm x)) ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
121 deltaM (mono x)
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
122 ∎
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
123 deltaM-right-unity-law {l} {A} {M} {fm} {mm} {S n} (deltaM (delta x d)) = begin
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
124 deltaM-mu (deltaM-eta (deltaM (delta x d)))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
125 ≡⟨ refl ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
126 deltaM-mu (deltaM (delta (eta mm (deltaM (delta x d))) (delta-eta (eta mm (deltaM (delta x d))))))
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
127 ≡⟨ refl ⟩
112
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
128 appendDeltaM (deltaM (mono (mu mm (fmap fm (headDeltaM {monadM = mm}) (eta mm (deltaM (delta x d)))))))
111
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
129 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d)))))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
130 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm de)))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
131 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
132 (sym (eta-is-nt mm headDeltaM (deltaM (delta x d)))) ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
133 appendDeltaM (deltaM (mono (mu mm (eta mm ((headDeltaM {monadM = mm}) (deltaM (delta x d)))))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
134 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d)))))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
135 ≡⟨ refl ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
136 appendDeltaM (deltaM (mono (mu mm (eta mm x))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
137 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d)))))))
112
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
138 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono de)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))))
111
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
139 (sym (right-unity-law mm x)) ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
140 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d)))))))
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 102
diff changeset
141 ≡⟨ refl ⟩
111
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
142 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-eta (eta mm (deltaM (delta x d)))))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
143 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM de))) (sym (eta-is-nt delta-is-monad (fmap fm tailDeltaM) (eta mm (deltaM (delta x d))))) ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
144 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-eta (fmap fm tailDeltaM (eta mm (deltaM (delta x d)))))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
145 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-eta de)))) (sym (eta-is-nt mm tailDeltaM (deltaM (delta x d)))) ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
146 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-eta (eta mm (tailDeltaM (deltaM (delta x d)))))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
147 ≡⟨ refl ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
148 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-eta (eta mm (deltaM d)))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
149 ≡⟨ refl ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
150 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-eta (deltaM d)))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
151 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) de) (deltaM-right-unity-law (deltaM d)) ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
152 appendDeltaM (deltaM (mono x)) (deltaM d)
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
153 ≡⟨ refl ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
154 deltaM (delta x d)
102
9c62373bd474 Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
155 ∎
112
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
156 -}
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
157
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
158
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
159
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
160
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
161
114
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
162 postulate deltaM-left-unity-law : {l : Level} {A : Set l}
112
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
163 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM}
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
164 {n : Nat}
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
165 (d : DeltaM M {functorM} {monadM} A (S n)) ->
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
166 (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d
114
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
167 {-
112
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
168 deltaM-left-unity-law {l} {A} {M} {fm} {mm} {O} (deltaM (mono x)) = begin
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
169 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x)))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
170 ≡⟨ refl ⟩
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
171 deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-eta) (mono x)))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
172 ≡⟨ refl ⟩
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
173 deltaM-mu (deltaM (mono (fmap fm deltaM-eta x)))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
174 ≡⟨ refl ⟩
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
175 deltaM (mono (mu mm (fmap fm (headDeltaM {l} {A} {O} {M}) (fmap fm deltaM-eta x))))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
176 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (covariant fm deltaM-eta headDeltaM x)) ⟩
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
177 deltaM (mono (mu mm (fmap fm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) ∙ deltaM-eta) x)))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
178 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (fmap-headDeltaM-with-deltaM-eta {l} {A} {O} {M} {fm} {mm} x) ⟩
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
179 deltaM (mono (mu mm (fmap fm (eta mm) x)))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
180 ≡⟨ cong (\de -> deltaM (mono de)) (left-unity-law mm x) ⟩
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
181 deltaM (mono x)
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
182 ∎
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
183 deltaM-left-unity-law {l} {A} {M} {fm} {mm} {S n} (deltaM (delta x d)) = begin
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
184 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (delta x d)))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
185 ≡⟨ refl ⟩
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
186 deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-eta) (delta x d)))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
187 ≡⟨ refl ⟩
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
188 deltaM-mu (deltaM (delta (fmap fm deltaM-eta x) (delta-fmap (fmap fm deltaM-eta) d)))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
189 ≡⟨ refl ⟩
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
190 appendDeltaM (deltaM (mono (mu mm (fmap fm (headDeltaM {l} {A} {S n} {M} {fm} {mm}) (fmap fm deltaM-eta x)))))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
191 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d))))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
192 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm de)))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
193 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d)))))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
194 (sym (covariant fm deltaM-eta headDeltaM x)) ⟩
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
195 appendDeltaM (deltaM (mono (mu mm (fmap fm ((headDeltaM {l} {A} {S n} {M} {fm} {mm}) ∙ deltaM-eta) x))))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
196 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d))))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
197 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm de)))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
198 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d)))))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
199 (fmap-headDeltaM-with-deltaM-eta {l} {A} {S n} {M} {fm} {mm} x) ⟩
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
200 appendDeltaM (deltaM (mono (mu mm (fmap fm (eta mm) x))))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
201 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d))))
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
202
112
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
203 ≡⟨ cong (\de -> (appendDeltaM (deltaM (mono de)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d))))))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
204 (left-unity-law mm x) ⟩
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
205 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d))))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
206 ≡⟨ refl ⟩
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
207 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap (tailDeltaM {n = n})(deltaM-fmap deltaM-eta (deltaM d))))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
208 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) (deltaM-mu de)) (sym (covariant deltaM-is-functor deltaM-eta tailDeltaM (deltaM d))) ⟩
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
209 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap ((tailDeltaM {n = n}) ∙ deltaM-eta) (deltaM d)))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
210 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) (deltaM-mu de)) (fmap-tailDeltaM-with-deltaM-eta (deltaM d)) ⟩
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
211 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap deltaM-eta (deltaM d)))
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
212 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) de) (deltaM-left-unity-law (deltaM d)) ⟩
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
213 appendDeltaM (deltaM (mono x)) (deltaM d)
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
214 ≡⟨ refl ⟩
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
215 deltaM (delta x d)
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
216 ∎
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
217
114
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
218 -}
117
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
219 postulate nya : {l : Level} {A : Set l}
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
220 (M : Set l -> Set l) (fm : Functor M) (mm : Monad M fm)
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
221 (d : DeltaM M {fm} {mm} (DeltaM M {fm} {mm} (DeltaM M {fm} {mm} A (S O)) (S O)) (S O)) ->
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
222 deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d)
114
08403eb8db8b Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 112
diff changeset
223
112
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
224
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
225
115
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
226
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
227
115
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
228
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
229
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
230 deltaM-association-law : {l : Level} {A : Set l} {n : Nat}
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
231 (M : Set l -> Set l) (fm : Functor M) (mm : Monad M fm)
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
232 (d : DeltaM M {fm} {mm} (DeltaM M {fm} {mm} (DeltaM M {fm} {mm} A (S n)) (S n)) (S n)) ->
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
233 deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d)
117
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
234 deltaM-association-law {l} {A} {O} M fm mm (deltaM (mono x)) = nya {l} {A} M fm mm (deltaM (mono x))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
235 {-
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
236 begin
115
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
237 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩
116
f02c5ad4a327 Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
238 deltaM-mu (deltaM (mono (fmap fm deltaM-mu x))) ≡⟨ refl ⟩
f02c5ad4a327 Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
239 deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM {A = DeltaM M A (S O)} {monadM = mm} (deltaM (mono (fmap fm deltaM-mu x))))))) ≡⟨ refl ⟩
f02c5ad4a327 Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
240 deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))) ≡⟨ refl ⟩
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
241 deltaM (mono (mu mm (fmap fm (headDeltaM {A = A} {monadM = mm}) (fmap fm
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
242 (\d -> (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d)))))) x))))
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
243 ≡⟨ cong (\de -> deltaM (mono (mu mm de)))
116
f02c5ad4a327 Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
244 (sym (covariant fm (\d -> (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d)))))) headDeltaM x)) ⟩
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
245 deltaM (mono (mu mm (fmap fm ((headDeltaM {A = A} {monadM = mm}) ∙
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
246 (\d -> (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d))))))) x)))
116
f02c5ad4a327 Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
247 ≡⟨ refl ⟩
f02c5ad4a327 Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
248 deltaM (mono (mu mm (fmap fm (\d -> (headDeltaM {A = A} {monadM = mm} (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d))))))) x)))
115
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
249 ≡⟨ refl ⟩
116
f02c5ad4a327 Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
250 deltaM (mono (mu mm (fmap fm (\d -> (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d)))) x)))
f02c5ad4a327 Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
251 ≡⟨ refl ⟩
f02c5ad4a327 Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
252 deltaM (mono (mu mm (fmap fm ((mu mm) ∙ (((fmap fm headDeltaM)) ∙ ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm})))) x)))
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
253 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (covariant fm ((fmap fm headDeltaM) ∙ (headDeltaM)) (mu mm) x )⟩
116
f02c5ad4a327 Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
254 deltaM (mono (mu mm (((fmap fm (mu mm)) ∙ (fmap fm ((fmap fm headDeltaM) ∙ (headDeltaM {l} {DeltaM M A (S O)} {monadM = mm})))) x)))
f02c5ad4a327 Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
255 ≡⟨ refl ⟩
f02c5ad4a327 Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
256 deltaM (mono (mu mm (fmap fm (mu mm) ((fmap fm ((fmap fm headDeltaM) ∙ (headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}))) x))))
f02c5ad4a327 Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
257 ≡⟨ cong (\de -> deltaM (mono (mu mm (fmap fm (mu mm) de)))) (covariant fm headDeltaM (fmap fm headDeltaM) x) ⟩
f02c5ad4a327 Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
258 deltaM (mono (mu mm (fmap fm (mu mm) (((fmap fm (fmap fm headDeltaM)) ∙ (fmap fm (headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}))) x))))
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
259 ≡⟨ refl ⟩
116
f02c5ad4a327 Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
260 deltaM (mono (mu mm (fmap fm (mu mm) (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x)))))
f02c5ad4a327 Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
261 ≡⟨ cong (\de -> deltaM (mono de)) (association-law mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))) ⟩
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
262 deltaM (mono (mu mm (mu mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x)))))
115
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
263 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (mu-is-nt mm headDeltaM (fmap fm headDeltaM x)) ⟩
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
264 deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))) ≡⟨ refl ⟩
116
f02c5ad4a327 Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
265 deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM {A = DeltaM M A (S O)} {monadM = mm} (deltaM (mono (mu mm (fmap fm headDeltaM x)))))))) ≡⟨ refl ⟩
115
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
266 deltaM-mu (deltaM (mono (mu mm (fmap fm headDeltaM x)))) ≡⟨ refl ⟩
116
f02c5ad4a327 Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
267 deltaM-mu (deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM {A = DeltaM M (DeltaM M A (S O)) (S O)} {monadM = mm} (deltaM (mono x))))))) ≡⟨ refl ⟩
f02c5ad4a327 Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 115
diff changeset
268 deltaM-mu (deltaM-mu (deltaM (mono x))) ∎
117
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
269 -}
118
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
270 deltaM-association-law {l} {A} {S n} M fm mm (deltaM (delta x d)) = begin
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
271 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d)))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
272 ≡⟨ refl ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
273 deltaM-mu (deltaM (delta (fmap fm deltaM-mu x) (delta-fmap (fmap fm deltaM-mu) d)))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
274 ≡⟨ refl ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
275 deltaM (delta (mu mm (fmap fm (headDeltaM {A = A} {monadM = mm}) (headDeltaM {A = DeltaM M A (S (S n))} {monadM = mm} (deltaM (delta (fmap fm deltaM-mu x) (delta-fmap (fmap fm deltaM-mu) d))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
276 (unDeltaM {A = A} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta (fmap fm deltaM-mu x) (delta-fmap (fmap fm deltaM-mu) d))))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
277
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
278 ≡⟨ refl ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
279 deltaM (delta (mu mm (fmap fm (headDeltaM {A = A} {monadM = mm}) (fmap fm deltaM-mu x)))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
280 (unDeltaM {A = A} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
281 ≡⟨ cong (\de -> deltaM (delta (mu mm de) (unDeltaM {A = A} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d)))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
282 (sym (covariant fm deltaM-mu headDeltaM x)) ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
283 deltaM (delta (mu mm (fmap fm ((headDeltaM {A = A} {monadM = mm}) ∙ deltaM-mu) x))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
284 (unDeltaM {A = A} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
285 ≡⟨ cong (\de -> deltaM (delta (mu mm de)
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
286 (unDeltaM {A = A} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d)))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
287 (fmap-headDeltaM-with-deltaM-mu {A = A} {monadM = mm} x) ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
288 deltaM (delta (mu mm (fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
289 (unDeltaM {A = A} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
290 ≡⟨ refl ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
291 deltaM (delta (mu mm (fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
292 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-fmap deltaM-mu (deltaM d))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
293 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
294 (unDeltaM {monadM = mm} (deltaM-mu de))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
295 (sym (deltaM-covariant fm tailDeltaM deltaM-mu (deltaM d))) ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
296 deltaM (delta (mu mm (fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
297 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap (tailDeltaM ∙ deltaM-mu) (deltaM d)))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
298 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
299 (unDeltaM {monadM = mm} (deltaM-mu de))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
300 (fmap-tailDeltaM-with-deltaM-mu (deltaM d)) ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
301 deltaM (delta (mu mm (fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
302 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
303 ≡⟨ cong (\de -> deltaM (delta (mu mm de)
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
304 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
305 (covariant fm headDeltaM ((mu mm) ∙ (fmap fm headDeltaM)) x) ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
306 deltaM (delta (mu mm (((fmap fm ((mu mm) ∙ (fmap fm headDeltaM))) ∙ (fmap fm headDeltaM)) x))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
307 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
308 ≡⟨ refl ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
309 deltaM (delta (mu mm (((fmap fm ((mu mm) ∙ (fmap fm headDeltaM))) (fmap fm headDeltaM x))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
310 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
311 ≡⟨ cong (\de -> deltaM (delta (mu mm de)
118
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
312 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
313 (covariant fm (fmap fm headDeltaM) (mu mm) (fmap fm headDeltaM x)) ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
314
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
315 deltaM (delta (mu mm ((((fmap fm (mu mm)) ∙ (fmap fm (fmap fm headDeltaM))) (fmap fm headDeltaM x))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
316 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
317 ≡⟨ refl ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
318 deltaM (delta (mu mm (fmap fm (mu mm) (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
319 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
320 ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
321 (association-law mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))) ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
322 deltaM (delta (mu mm (mu mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
323 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
324 ≡⟨ cong (\de -> deltaM (delta (mu mm de) (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
325 (mu-is-nt mm headDeltaM (fmap fm headDeltaM x)) ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
326 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
327 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap ((deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ tailDeltaM) (deltaM d)))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
328 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x)))) (unDeltaM {monadM = mm} (deltaM-mu de))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
329 (deltaM-covariant fm (deltaM-mu ∙ (deltaM-fmap tailDeltaM)) tailDeltaM (deltaM d)) ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
330 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
331 (unDeltaM {monadM = mm} (deltaM-mu (((deltaM-fmap (deltaM-mu ∙ (deltaM-fmap tailDeltaM)) ∙ (deltaM-fmap tailDeltaM)) (deltaM d))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
332 ≡⟨ refl ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
333 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
334 (unDeltaM {monadM = mm} (deltaM-mu (((deltaM-fmap (deltaM-mu ∙ (deltaM-fmap tailDeltaM)) (deltaM-fmap tailDeltaM (deltaM d))))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
335 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x)))) (unDeltaM {monadM = mm} (deltaM-mu de))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
336 (deltaM-covariant fm deltaM-mu (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d))) ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
337 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
338 (unDeltaM {monadM = mm} (deltaM-mu (((deltaM-fmap deltaM-mu) ∙ (deltaM-fmap (deltaM-fmap tailDeltaM))) (deltaM-fmap tailDeltaM (deltaM d))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
339 ≡⟨ refl ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
340 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
341 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap deltaM-mu (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
342 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x)))) (unDeltaM {monadM = mm} de)))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
343 (deltaM-association-law M fm mm (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))) ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
344 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
345 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-mu (deltaM-fmap (deltaM-fmap tailDeltaM) (deltaM-fmap tailDeltaM (deltaM d)))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
346
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
347 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
348 (unDeltaM {monadM = mm} (deltaM-mu de))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
349 (sym (deltaM-mu-is-nt tailDeltaM (deltaM-fmap tailDeltaM (deltaM d)))) ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
350 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
351 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
352 ≡⟨ cong (\de -> deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
353 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM de)))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
354 (sym (deconstruct-id (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))) ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
355 deltaM (delta (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
356 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM
118
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
357 (deltaM (unDeltaM {A = DeltaM M A (S (S n))} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
358
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
359
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
360 ≡⟨ refl ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
361 deltaM (delta (mu mm (fmap fm headDeltaM (headDeltaM {monadM = mm} ((deltaM (delta (mu mm (fmap fm headDeltaM x))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
362 (unDeltaM {A = DeltaM M A (S (S n))} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
363 (unDeltaM {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM ((deltaM (delta (mu mm (fmap fm headDeltaM x))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
364 (unDeltaM {A = DeltaM M A (S (S n))} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
365
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
366
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
367 ≡⟨ refl ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
368 deltaM-mu (deltaM (delta (mu mm (fmap fm headDeltaM x))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
369 (unDeltaM {A = DeltaM M A (S (S n))} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
370 ≡⟨ refl ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
371 deltaM-mu (deltaM (delta (mu mm (fmap fm headDeltaM (headDeltaM {monadM = mm} (deltaM (delta x d)))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
372 (unDeltaM {A = DeltaM M A (S (S n))} {monadM = mm} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta x d))))))))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
373 ≡⟨ refl ⟩
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
374 deltaM-mu (deltaM-mu (deltaM (delta x d)))
53cb21845dea Prove association-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 117
diff changeset
375 ∎
117
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
376 {-
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
377 deltaM-association-law {l} {A} {S n} M fm mm (deltaM (delta x d)) = begin
115
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
378 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d))) ≡⟨ refl ⟩
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
379 deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-mu) (delta x d))) ≡⟨ refl ⟩
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
380 deltaM-mu (deltaM (delta (fmap fm deltaM-mu x) (delta-fmap (fmap fm deltaM-mu) d))) ≡⟨ refl ⟩
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
381 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))))
117
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
382 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d)))) ≡⟨ refl ⟩
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
383 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
384 (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d))))
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
385 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x))))) de)
117
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
386 (sym (deconstruct-id (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d)))))) ⟩
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
387
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
388 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
389 (deltaM (deconstruct {A = A} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d))))))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
390 ≡⟨ refl ⟩
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
391 deltaM (deltaAppend (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x))))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
392 (deconstruct {A = A} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d))))))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
393 ≡⟨ refl ⟩
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
394 deltaM (delta (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
395 (deconstruct {A = A} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d))))))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
396 ≡⟨ {!!} ⟩
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
397 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
398 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d)))))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
399 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))))
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
400 (deltaM-mu (deltaM-fmap tailDeltaM de)))
117
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
401 (sym (deconstruct-id (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))) ⟩
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
402 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
403 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d)))))))
115
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
404
117
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
405 ≡⟨ refl ⟩
115
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
406 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))))
117
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
407 (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM ( (deltaM (delta (mu mm (fmap fm headDeltaM x))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
408 (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))))))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
409 ≡⟨ refl ⟩
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
410 appendDeltaM (deltaM (mono (mu mm (fmap fm (headDeltaM {monadM = mm}) (headDeltaM {monadM = mm} ((deltaM (delta (mu mm (fmap fm headDeltaM x))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
411 (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))))))))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
412 (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM ( (deltaM (delta (mu mm (fmap fm headDeltaM x))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
413 (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))))))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
414 ≡⟨ refl ⟩
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
415 deltaM-mu (deltaM (delta (mu mm (fmap fm headDeltaM x))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
416 (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
417 ≡⟨ refl ⟩
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
418 deltaM-mu (deltaM (deltaAppend (mono (mu mm (fmap fm headDeltaM x)))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
419 (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
420 ≡⟨ refl ⟩
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
421 deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x))))
117
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
422 (deltaM (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
423 ≡⟨ cong (\de -> deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x)))) de))
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
424 (deconstruct-id (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d)))) ⟩
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
425 deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x))))
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
426 (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))
117
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
427 ≡⟨ refl ⟩
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
428 deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x))))
115
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
429 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))≡⟨ refl ⟩
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
430 deltaM-mu (deltaM-mu (deltaM (delta x d)))
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
431 ∎
117
6f86b55bf8b4 Temporary commit : Proving association-law ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
432 -}
115
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
433
e6bcc7467335 Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 114
diff changeset
434
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
435
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
436 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat}
112
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
437 {M : Set l -> Set l}
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
438 (functorM : Functor M)
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
439 (monadM : Monad M functorM) ->
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
440 Monad {l} (\A -> DeltaM M {functorM} {monadM} A (S n)) (deltaM-is-functor {l} {n})
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
441 deltaM-is-monad {l} {A} {n} {M} functorM monadM =
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
442 record { mu = deltaM-mu
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
443 ; eta = deltaM-eta
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
444 ; eta-is-nt = deltaM-eta-is-nt
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
445 ; mu-is-nt = (\f x -> (sym (deltaM-mu-is-nt f x)))
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
446 ; association-law = (deltaM-association-law M functorM monadM)
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
447 ; left-unity-law = deltaM-left-unity-law
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
448 ; right-unity-law = (\x -> (sym (deltaM-right-unity-law x)))
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
449 }
102
9c62373bd474 Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
450
9c62373bd474 Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
451
124
48b44bd85056 Fix proof natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
452 -}