# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1424843390 -32400
# Node ID 575de2e3838563002d997ba7a429b20139264e04
# Parent  f241d521bf652a1df9dcd7a75cc5d81332bbe48e
Fix names left/right unity law

diff -r f241d521bf65 -r 575de2e38385 agda/delta/monad.agda
--- a/agda/delta/monad.agda	Wed Feb 25 14:36:02 2015 +0900
+++ b/agda/delta/monad.agda	Wed Feb 25 14:49:50 2015 +0900
@@ -95,9 +95,9 @@
   ∎
 
 
-delta-right-unity-law : {l : Level} {A : Set l} {n : Nat} (d : Delta A (S n)) -> (delta-mu ∙ delta-eta) d ≡ id d
-delta-right-unity-law (mono x)    = refl
-delta-right-unity-law (delta x d) = begin
+delta-left-unity-law : {l : Level} {A : Set l} {n : Nat} (d : Delta A (S n)) -> (delta-mu ∙ delta-eta) d ≡ id d
+delta-left-unity-law (mono x)    = refl
+delta-left-unity-law (delta x d) = begin
   (delta-mu ∙ delta-eta) (delta x d)
   ≡⟨ refl ⟩
   delta-mu (delta-eta (delta x d))
@@ -111,16 +111,16 @@
   delta x (delta-mu (delta-eta (tailDelta (delta x d))))
   ≡⟨ refl ⟩
   delta x (delta-mu (delta-eta d))
-  ≡⟨ cong (\de -> delta x de) (delta-right-unity-law d) ⟩
+  ≡⟨ cong (\de -> delta x de) (delta-left-unity-law d) ⟩
   delta x d
   ≡⟨ refl ⟩
   id (delta x d)  ∎
 
 
-delta-left-unity-law  : {l : Level} {A : Set l} {n : Nat} -> (d : Delta A (S n)) ->
+delta-right-unity-law  : {l : Level} {A : Set l} {n : Nat} -> (d : Delta A (S n)) ->
                                              (delta-mu  ∙ (delta-fmap delta-eta)) d ≡ id d
-delta-left-unity-law (mono x)    = refl
-delta-left-unity-law {n = (S n)} (delta x d) = begin
+delta-right-unity-law (mono x)    = refl
+delta-right-unity-law {n = (S n)} (delta x d) = begin
   (delta-mu ∙ delta-fmap delta-eta) (delta x d)            ≡⟨ refl ⟩
   delta-mu ( delta-fmap delta-eta (delta x d))             ≡⟨ refl ⟩
   delta-mu (delta (delta-eta x) (delta-fmap delta-eta d))  ≡⟨ refl ⟩
@@ -128,7 +128,7 @@
   delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d)))
   ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (delta-covariant tailDelta delta-eta d)) ⟩
   delta x (delta-mu (delta-fmap (tailDelta ∙ delta-eta {n = S n}) d))  ≡⟨ refl ⟩
-  delta x (delta-mu (delta-fmap (delta-eta {n = n}) d))  ≡⟨ cong (\de -> delta x de) (delta-left-unity-law d) ⟩
+  delta x (delta-mu (delta-fmap (delta-eta {n = n}) d))  ≡⟨ cong (\de -> delta x de) (delta-right-unity-law d) ⟩
   delta x d ≡⟨ refl ⟩
   id (delta x d)  ∎
 
@@ -140,8 +140,8 @@
                           eta-is-nt = delta-eta-is-nt;
                           mu-is-nt = delta-mu-is-nt;
                           association-law = delta-association-law;
-                          left-unity-law  = delta-left-unity-law ;
-                          right-unity-law = \x -> (sym (delta-right-unity-law x)) }
+                          right-unity-law  = delta-right-unity-law ;
+                          left-unity-law = \x -> (sym (delta-left-unity-law x)) }
 
 
 
diff -r f241d521bf65 -r 575de2e38385 agda/deltaM/monad.agda
--- a/agda/deltaM/monad.agda	Wed Feb 25 14:36:02 2015 +0900
+++ b/agda/deltaM/monad.agda	Wed Feb 25 14:49:50 2015 +0900
@@ -177,19 +177,19 @@
 
 
 
-deltaM-right-unity-law : {l : Level} {A : Set l} {n : Nat}
+deltaM-left-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
-deltaM-right-unity-law {l} {A} {O} {M} {fm} {mm} (deltaM (mono x)) = begin
+deltaM-left-unity-law {l} {A} {O} {M} {fm} {mm} (deltaM (mono x)) = begin
   deltaM-mu (deltaM-eta (deltaM (mono x)))             ≡⟨ refl ⟩
   deltaM-mu (deltaM (mono (eta mm (deltaM (mono x))))) ≡⟨ refl ⟩
   deltaM (mono (mu mm (fmap fm (headDeltaM {M = mm})(eta mm (deltaM (mono x))))))
   ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (eta-is-nt mm headDeltaM (deltaM (mono x)) )) ⟩
   deltaM (mono (mu mm (eta mm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) (deltaM (mono x)))))) ≡⟨ refl ⟩
-  deltaM (mono (mu mm (eta mm x))) ≡⟨ cong (\de -> deltaM (mono de)) (sym (right-unity-law mm x)) ⟩
+  deltaM (mono (mu mm (eta mm x))) ≡⟨ cong (\de -> deltaM (mono de)) (sym (left-unity-law mm x)) ⟩
   deltaM (mono x)
   ∎
-deltaM-right-unity-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin
+deltaM-left-unity-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin
   deltaM-mu (deltaM-eta (deltaM (delta x d)))
   ≡⟨ refl ⟩
   deltaM-mu (deltaM (delta (eta M (deltaM (delta x d))) (delta-eta (eta M (deltaM (delta x d))))))
@@ -208,7 +208,7 @@
   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))))))))))
-           (sym (right-unity-law M x)) ⟩
+           (sym (left-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 ⟩
   deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-fmap (fmap F tailDeltaM) (delta-eta (eta M (deltaM (delta x d)))))))))
@@ -222,7 +222,7 @@
   deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-eta (eta M (deltaM d)))))))
   ≡⟨ refl ⟩
   deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-eta (deltaM d)))))
-  ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} de))) (deltaM-right-unity-law (deltaM d)) ⟩
+  ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} de))) (deltaM-left-unity-law (deltaM d)) ⟩
   deltaM (delta x (unDeltaM {M = M} (deltaM d)))
   ≡⟨ refl ⟩
   deltaM (delta x d)
@@ -233,10 +233,10 @@
 
 
 
-deltaM-left-unity-law : {l : Level} {A : Set l} {n : Nat}
+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-fmap deltaM-eta)) d ≡ id d
-deltaM-left-unity-law {l} {A}   {O} {T} {F} {M} (deltaM (mono x)) = begin
+deltaM-right-unity-law {l} {A}   {O} {T} {F} {M} (deltaM (mono x)) = begin
   deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩
   deltaM-mu (deltaM (mono (fmap F deltaM-eta x)))      ≡⟨ refl ⟩
   deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F deltaM-eta x)))))))      ≡⟨ refl ⟩
@@ -245,10 +245,10 @@
   deltaM (mono (mu M (fmap F ((headDeltaM {n = O} {M = M}) ∙ deltaM-eta) x)))
   ≡⟨ refl ⟩
   deltaM (mono (mu M (fmap F (eta M) x)))
-  ≡⟨ cong (\de -> deltaM (mono de)) (left-unity-law M x) ⟩
+  ≡⟨ cong (\de -> deltaM (mono de)) (right-unity-law M x) ⟩
   deltaM (mono x)
   ∎
-deltaM-left-unity-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin
+deltaM-right-unity-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin
   deltaM-mu (deltaM-fmap deltaM-eta (deltaM (delta x d)))
   ≡⟨ refl ⟩
   deltaM-mu (deltaM (delta (fmap F deltaM-eta x) (delta-fmap (fmap F deltaM-eta) d)))
@@ -266,7 +266,7 @@
   deltaM (delta (mu M (fmap F (eta M) x))
                 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d))))))
   ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d)))))))
-           (left-unity-law M x) ⟩
+           (right-unity-law M x) ⟩
   deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d))))))
   ≡⟨ refl ⟩
   deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (tailDeltaM {n = n})(deltaM-fmap (deltaM-eta {n = S n})(deltaM d))))))
@@ -274,7 +274,7 @@
   deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((tailDeltaM {n = n}) ∙ (deltaM-eta {n = S n})) (deltaM d)))))
   ≡⟨ refl ⟩
   deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap deltaM-eta (deltaM d)))))
-  ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} de))) (deltaM-left-unity-law (deltaM d)) ⟩
+  ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} de))) (deltaM-right-unity-law (deltaM d)) ⟩
   deltaM (delta x (unDeltaM {M = M} (deltaM d)))
   ≡⟨ refl ⟩
   deltaM (delta x d)
@@ -438,6 +438,6 @@
                        ; eta-is-nt = deltaM-eta-is-nt
                        ; mu-is-nt = (\f x -> (sym (deltaM-mu-is-nt f x)))
                        ; association-law = deltaM-association-law
-                       ; left-unity-law  = deltaM-left-unity-law
-                       ; right-unity-law = (\x -> (sym (deltaM-right-unity-law x)))
+                       ; right-unity-law  = deltaM-right-unity-law
+                       ; left-unity-law = (\x -> (sym (deltaM-left-unity-law x)))
                        }
diff -r f241d521bf65 -r 575de2e38385 agda/laws.agda
--- a/agda/laws.agda	Wed Feb 25 14:36:02 2015 +0900
+++ b/agda/laws.agda	Wed Feb 25 14:49:50 2015 +0900
@@ -40,8 +40,8 @@
     mu-is-nt  : {A B : Set l} -> (f : A -> B) -> (x : T (T A)) -> mu (fmap F (fmap F f) x) ≡ fmap F f (mu x)
   field -- category laws
     association-law : {A : Set l} -> (x : (T (T (T A)))) -> (mu ∙ (fmap F mu))  x ≡ (mu ∙ mu) x
-    left-unity-law  : {A : Set l} -> (x : T A)           -> (mu ∙ (fmap F eta)) x ≡ id x
-    right-unity-law : {A : Set l} -> (x : T A)           -> id x ≡ (mu ∙ eta) x
+    right-unity-law  : {A : Set l} -> (x : T A)           -> (mu ∙ (fmap F eta)) x ≡ id x
+    left-unity-law : {A : Set l} -> (x : T A)           -> id x ≡ (mu ∙ eta) x
 
 
 open Monad