### changeset 126:5902b2a24abf

Prove mu-is-nt for DeltaM with fmap-equiv
author Yasutaka Higa Tue, 03 Feb 2015 11:45:33 +0900 6dcc68ef8f96 d56596e4e784 agda/delta/functor.agda agda/deltaM.agda agda/deltaM/functor.agda agda/deltaM/monad.agda agda/laws.agda 5 files changed, 140 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
```--- a/agda/delta/functor.agda	Mon Feb 02 14:09:30 2015 +0900
+++ b/agda/delta/functor.agda	Tue Feb 03 11:45:33 2015 +0900
@@ -24,9 +24,24 @@
functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d)

+delta-fmap-equiv : {l : Level} {A B : Set l} {n : Nat} {f g : A -> B}
+                   (eq : (x : A) -> f x ≡ g x) -> (d : Delta A (S n)) ->
+                   delta-fmap f d ≡ delta-fmap g d
+delta-fmap-equiv {l} {A} {B} {O} {f} {g} eq (mono x) = begin
+  mono (f x) ≡⟨ cong mono (eq x) ⟩
+  mono (g x)
+  ∎
+delta-fmap-equiv {l} {A} {B} {S n} {f} {g} eq (delta x d) = begin
+  delta (f x) (delta-fmap f d) ≡⟨ cong (\de -> delta de (delta-fmap f d)) (eq x) ⟩
+  delta (g x) (delta-fmap f d) ≡⟨ cong (\de -> delta (g x) de) (delta-fmap-equiv eq d) ⟩
+  delta (g x) (delta-fmap g d)
+  ∎
+
+

delta-is-functor : {l : Level} {n : Nat} -> Functor {l} (\A -> Delta A (S n))
-delta-is-functor = record {  fmap = delta-fmap ;
-                             preserve-id = functor-law-1;
-                             covariant  = \f g -> functor-law-2 g f
-                             }
+delta-is-functor = record { fmap       = delta-fmap
+                          ;preserve-id = functor-law-1
+                          ; covariant  = \f g -> functor-law-2 g f
+                          ; fmap-equiv = delta-fmap-equiv
+                          }```
```--- a/agda/deltaM.agda	Mon Feb 02 14:09:30 2015 +0900
+++ b/agda/deltaM.agda	Tue Feb 03 11:45:33 2015 +0900
@@ -57,7 +57,7 @@
deltaM-fmap : {l : Level} {A B : Set l} {n : Nat}
{T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
(A -> B) -> DeltaM M A (S n) -> DeltaM M B (S n)
-deltaM-fmap {l} {A} {B} {n} {M} {functorM} f (deltaM d) = deltaM (fmap delta-is-functor (fmap functorM f) d)
+deltaM-fmap {l} {A} {B} {n} {M} {functorM} f d = deltaM (fmap delta-is-functor (fmap functorM f) (unDeltaM d))

```
```--- a/agda/deltaM/functor.agda	Mon Feb 02 14:09:30 2015 +0900
+++ b/agda/deltaM/functor.agda	Tue Feb 03 11:45:33 2015 +0900
@@ -75,6 +75,25 @@
(deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d))
∎

+deltaM-fmap-equiv : {l : Level} {A B : Set l} {n : Nat}
+                    {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
+                    {f g : A -> B}
+                    (eq : (x : A) -> f x ≡ g x) -> (d : DeltaM M A (S n)) ->
+                    deltaM-fmap f d ≡ deltaM-fmap g d
+deltaM-fmap-equiv {l} {A} {B}   {O} {T} {F} {M} {f} {g} eq (deltaM (mono x))    = begin
+  deltaM-fmap f (deltaM (mono x)) ≡⟨ refl ⟩
+  deltaM (mono (fmap F f x))      ≡⟨ cong (\de -> deltaM (mono de)) (fmap-equiv F eq x) ⟩
+  deltaM (mono (fmap F g x))      ≡⟨ refl ⟩
+  deltaM-fmap g (deltaM (mono x))
+  ∎
+deltaM-fmap-equiv {l} {A} {B} {S n} {T} {F} {M} {f} {g} eq (deltaM (delta x d)) = begin
+  deltaM-fmap f (deltaM (delta x d)) ≡⟨ refl ⟩
+  deltaM (delta (fmap F f x) (delta-fmap (fmap F f) d)) ≡⟨ cong (\de -> deltaM (delta de (delta-fmap (fmap F f) d))) (fmap-equiv F eq x) ⟩
+  deltaM (delta (fmap F g x) (delta-fmap (fmap F f) d)) ≡⟨ cong (\de -> deltaM (delta (fmap F g x) de)) (delta-fmap-equiv (fmap-equiv F eq) d) ⟩
+  deltaM (delta (fmap F g x) (delta-fmap (fmap F g) d)) ≡⟨ refl ⟩
+  deltaM-fmap g (deltaM (delta x d))
+  ∎
+

deltaM-is-functor : {l : Level} {n : Nat}
@@ -83,6 +102,7 @@
deltaM-is-functor {F = F} = record { fmap         = deltaM-fmap
; preserve-id  = deltaM-preserve-id {F = F}
; covariant    = (\f g -> deltaM-covariant {F = F} g f)
+                                   ; fmap-equiv   = deltaM-fmap-equiv
}

```
```--- a/agda/deltaM/monad.agda	Mon Feb 02 14:09:30 2015 +0900
+++ b/agda/deltaM/monad.agda	Tue Feb 03 11:45:33 2015 +0900
@@ -25,6 +25,19 @@
deconstruct-id {n = O}   (deltaM x) = refl
deconstruct-id {n = S n} (deltaM x) = refl

+headDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat}
+                    {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
+                    (f : A -> B) -> (x : (DeltaM M A (S n))) ->
+                    ((fmap F f) ∙ headDeltaM) x ≡ (headDeltaM ∙ (deltaM-fmap f)) x
+headDeltaM-with-f {n = O} f   (deltaM (mono x))    = refl
+headDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl
+
+tailDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat}
+                    {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
+                    (f : A -> B) -> (d : (DeltaM M A (S (S n)))) ->
+                    (tailDeltaM ∙ (deltaM-fmap f)) d ≡ ((deltaM-fmap f) ∙ tailDeltaM) d
+tailDeltaM-with-f {n = O} f (deltaM (delta x d))   = refl
+tailDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl

fmap-headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat}
@@ -91,12 +104,26 @@

-postulate deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat}
+deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat}
{T : Set l -> Set l} {F : Functor T} {M : Monad T F}
(f : A -> B) -> (d : DeltaM M (DeltaM M A (S n)) (S n)) ->
deltaM-fmap f (deltaM-mu d) ≡ deltaM-mu (deltaM-fmap (deltaM-fmap f) d)
+deltaM-mu-is-nt {l} {A} {B} {O} {T} {F} {M}  f (deltaM (mono x))      =
{-
deltaM-mu-is-nt {l} {A} {B} {O} {T} {F} {M}  f (deltaM (mono x))      = begin
+  deltaM-fmap f (deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩
+  deltaM-fmap f (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono x))))))) ≡⟨ refl ⟩
+  deltaM-fmap f (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) x)))) ≡⟨ refl ⟩
+  deltaM (mono (fmap F f (mu M (fmap F (headDeltaM {M = M}) x)))) ≡⟨ {!!} ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x)))) ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F (deltaM-fmap f) x))))))) ≡⟨ refl ⟩
+  deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x))) ≡⟨ refl ⟩
+  deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x))) ≡⟨ refl ⟩
+  deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (mono x)))
+  ∎
+-}
+
+  begin
deltaM-fmap f (deltaM-mu (deltaM (mono x)))
≡⟨ refl ⟩
deltaM-fmap f (deltaM (mono (mu M (fmap F headDeltaM x))))
@@ -104,26 +131,83 @@
deltaM (mono (fmap F f (mu M (fmap F headDeltaM x))))
≡⟨ cong (\de -> deltaM (mono de)) (sym (mu-is-nt M f (fmap F headDeltaM x))) ⟩
deltaM (mono (mu M (fmap F (fmap F f) (fmap F headDeltaM x))))
-  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F headDeltaM (fmap F f) x)) ⟩
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F headDeltaM (fmap F f) x)) ⟩
deltaM (mono (mu M (fmap F ((fmap F f) ∙ headDeltaM) x)))
-  ≡⟨ {!!} ⟩
-  deltaM (mono (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)))
-  ≡⟨ {!!} ⟩
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (fmap-equiv F (headDeltaM-with-f f) x) ⟩
deltaM (mono (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)))
≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F (deltaM-fmap f) (headDeltaM) x) ⟩
-  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x))))
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x))))
≡⟨ refl ⟩
-  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F (deltaM-fmap f) x)))))))
-  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F (deltaM-fmap f) x)))))))
+  ≡⟨ refl ⟩
deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x)))
≡⟨ refl ⟩
deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (mono x)))
∎
-deltaM-mu-is-nt {n = S n} f (deltaM (delta x d)) = {!!}

--}
+deltaM-mu-is-nt {l} {A} {B} {S n} {T} {F} {M} f (deltaM (delta x d)) = begin
+  deltaM-fmap f (deltaM-mu (deltaM (delta x d))) ≡⟨ refl ⟩
+  deltaM-fmap f (deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta x d)))))
+                               (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta x d))))))))
+  ≡⟨ refl ⟩
+  deltaM-fmap f (deltaM (delta (mu M (fmap F (headDeltaM {M = M}) x))
+                               (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (fmap F f (mu M (fmap F (headDeltaM {M = M}) x)))
+                (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ cong (\de -> deltaM (delta de
+                  (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))
+           (sym (mu-is-nt M f (fmap F headDeltaM x)))  ⟩
+  deltaM (delta (mu M (fmap F (fmap F f) (fmap F (headDeltaM {M = M}) x)))
+                (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de) (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))
+           (sym (covariant F headDeltaM (fmap F f) x)) ⟩
+  deltaM (delta (mu M (fmap F ((fmap F f) ∙ (headDeltaM {M = M})) x))
+                (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de) (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))))
+           (fmap-equiv F (headDeltaM-with-f f) x)  ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (unDeltaM {M = M} (deltaM-fmap f (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM de)))
+           (deltaM-mu-is-nt {l} {A} {B} {n} {T} {F} {M} f (deltaM-fmap tailDeltaM (deltaM d))) ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (deltaM-fmap {n = n} f) (deltaM-fmap {n = n} (tailDeltaM {n = n}) (deltaM d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de))))
+           (sym (deltaM-covariant (deltaM-fmap f) tailDeltaM (deltaM d))) ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap {n = n} ((deltaM-fmap {n = n} f) ∙ (tailDeltaM {n = n})) (deltaM d)))))
+
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de))))
+               (sym (deltaM-fmap-equiv (tailDeltaM-with-f f) (deltaM d))) ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (tailDeltaM ∙ (deltaM-fmap f)) (deltaM d)))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de))))
+           (deltaM-covariant tailDeltaM (deltaM-fmap f) (deltaM d)) ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-fmap (deltaM-fmap f) (deltaM d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
+                (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d))))))
+  ≡⟨ cong (\de -> deltaM (delta (mu M de) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d)))))))
+           (covariant F (deltaM-fmap f) headDeltaM x) ⟩
+  deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x)))
+                      (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d))))))
+  ≡⟨ refl ⟩
+  deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d))))))
+                      (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d))))))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d)))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (delta x d)))
+  ∎

+
+
+{-
deltaM-right-unity-law : {l : Level} {A : Set l} {n : Nat}
{T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
(d : DeltaM M A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d
@@ -154,10 +238,10 @@
≡⟨ refl ⟩
deltaM (delta (mu M (eta M x))
(unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))
-  ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))))
+  ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))))
(sym (right-unity-law M x)) ⟩
deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))
-  ≡⟨ refl ⟩
+  ≡⟨ refl ⟩
deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-fmap (fmap F tailDeltaM) (delta-eta (eta M (deltaM (delta x d)))))))))
≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM de)))))
(sym (delta-eta-is-nt (fmap F tailDeltaM)  (eta M (deltaM (delta x d))))) ⟩
@@ -177,7 +261,7 @@

-{-
+

postulate deltaM-left-unity-law : {l : Level} {A : Set l}```
```--- a/agda/laws.agda	Mon Feb 02 14:09:30 2015 +0900
+++ b/agda/laws.agda	Tue Feb 03 11:45:33 2015 +0900
@@ -7,10 +7,12 @@
record Functor {l : Level} (F : Set l -> Set l) : Set (suc l) where
field
fmap : {A B : Set l} -> (A -> B) -> (F A) -> (F B)
-  field
+  field -- laws
preserve-id : {A : Set l} (x : F A) → fmap id x ≡ id x
covariant   : {A B C : Set l} (f : A -> B) -> (g : B -> C) -> (x : F A)
-> fmap (g ∙ f) x ≡ ((fmap g) ∙ (fmap f)) x
+  field -- proof assistant
+    fmap-equiv : {A B : Set l} {f g : A -> B} -> ((x : A) -> f x ≡ g x) -> (fx : F A) -> fmap f fx ≡ fmap g fx
open Functor

record NaturalTransformation {l : Level} (F G : Set l -> Set l)```