Mercurial > hg > Members > kono > Proof > category

changeset 68:829e0698f87f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
join implicit parameter
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 25 Jul 2013 13:56:16 +0900
parents e75436075bf0
children 84a150c980ce
files cat-utility.agda nat.agda
diffstat 2 files changed, 11 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/cat-utility.agda	Thu Jul 25 13:08:49 2013 +0900
+++ b/cat-utility.agda	Thu Jul 25 13:56:16 2013 +0900
@@ -118,7 +118,7 @@
      monad : Monad A T η μ 
      monad = M
      -- g ○ f = μ(c) T(g) f
-     join : { a b : Obj A } → ( c : Obj A ) →
+     join : { a b : Obj A } → { c : Obj A } →
                       ( Hom A b ( FObj T c )) → (  Hom A a ( FObj T b)) → Hom A a ( FObj T c )
-     join c g f = A [ TMap μ c  o A [ FMap T g  o f ] ]
+     join {_} {_} {c} g f = A [ TMap μ c  o A [ FMap T g o f ] ]
 
--- a/nat.agda	Thu Jul 25 13:08:49 2013 +0900
+++ b/nat.agda	Thu Jul 25 13:56:16 2013 +0900
@@ -93,13 +93,13 @@
                  ( f : Hom A a ( FObj T b) )
                  ( m : Monad A T η μ )
                  { k : Kleisli A T η μ m}
-                      → A  [ join k b (TMap η b) f  ≈ f ]
+                      → A  [ join k (TMap η b) f  ≈ f ]
 Lemma7 c {T} η b f m {k} = 
   let open ≈-Reasoning (c) 
       μ = mu ( monad k )
   in 
      begin  
-         join k b (TMap η b) f 
+         join k (TMap η b) f 
      ≈⟨ refl-hom ⟩
          c [ TMap μ b  o c [ FMap T ((TMap η b)) o f ] ]  
      ≈⟨ IsCategory.associative (Category.isCategory c) ⟩
@@ -119,10 +119,10 @@
                  ( f : Hom A a ( FObj T b) )
                  ( m : Monad A T η μ )
                  ( k : Kleisli A T η μ m) 
-                      → A  [ join k b f (TMap η a)  ≈ f ]
+                      → A  [ join k f (TMap η a)  ≈ f ]
 Lemma8 c T η a b f m k = 
   begin
-     join k b f (TMap η a) 
+     join k f (TMap η a) 
   ≈⟨ refl-hom ⟩
      c [ TMap μ b  o c [  FMap T f o (TMap η a) ] ]  
   ≈⟨ cdr  ( nat η ) ⟩
@@ -148,12 +148,12 @@
                  ( h : Hom A c ( FObj T d) )
                  ( m : Monad A T η μ )
                  { k : Kleisli A T η μ m}
-                      → A  [ join k d h (join k c g f)  ≈ join k d ( join k d h g) f ]
+                      → A  [ join k h (join k g f)  ≈ join k ( join k h g) f ]
 Lemma9 A {T} {η} {μ} {a} {b} {c} {d} f g h m {k} = 
   begin 
-     join k d h (join k c g f)  
+     join k h (join k g f)  
    ≈⟨⟩
-     join k d h (                  ( TMap μ c o ( FMap T g o f ) ) )
+     join k h (                  ( TMap μ c o ( FMap T g o f ) ) )
    ≈⟨ refl-hom ⟩
      ( TMap μ d  o ( FMap T h  o  ( TMap μ c o ( FMap T g  o f ) ) ) )
    ≈⟨ cdr ( cdr ( assoc )) ⟩
@@ -198,9 +198,9 @@
    ≈⟨ cdr ( car ( sym ( distr T )))   ⟩
      ( TMap μ d  o ( FMap T ( ( ( TMap μ d )   o ( FMap T h  o g ) ) ) o f ) )
    ≈⟨ refl-hom ⟩
-     join k d ( ( TMap μ d  o ( FMap T h  o g ) ) ) f
+     join k ( ( TMap μ d  o ( FMap T h  o g ) ) ) f
    ≈⟨ refl-hom ⟩
-     join k d ( join k d h g) f 
+     join k ( join k h g) f 
   ∎ where open ≈-Reasoning (A) 
 
 -- Kleisli-join : {!!}