Mercurial > hg > Members > kono > Proof > category

changeset 4:05087d3aeac0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 06 Jul 2013 08:50:32 +0900
parents dce706edd66b
children 16572013c362
files category.ind nat.agda
diffstat 2 files changed, 40 insertions(+), 29 deletions(-) [+]
line wrap: on
line diff
--- a/category.ind	Sat Jul 06 07:27:57 2013 +0900
+++ b/category.ind	Sat Jul 06 08:50:32 2013 +0900
@@ -952,7 +952,7 @@
 
 Object of $A$.
 
-Arrow $f: T -> T(A)$. In $f: b -> c, g: c -> d$,
+Arrow $f: a -> T(a)$ in $A$. In $A_T$, $f: b -> c, g: c -> d$,
 
 $  g * f = μ(d)T(g)f $
 
@@ -1085,11 +1085,11 @@
 $ f: a ->  (m,f(a)) $
 
 \begin{eqnarray*}
-g * f (b) & = & μ(T(g))f(b) = μ(T(g))(m,f(b)) \\ & = & μ(m,(m',gf(b))) = (mm',gf(b))   \\
-(g * f) * h(a) & = & μT(μ(T(g)f))h(a)  = μT(μ)(TT(g))T(f)(m,h(a))   \\
-\mbox{}    & = & μT(μ)(TT(g))(m,(m',fh(a))) \\ & = & μT(μ)(m,(m',(m'',gfh(a)))) =  (mm'm'',gfh(a))  \\
-g * (f * h)(a) & = & (μ(T(g)))μT(f)h(a)  = (μ(T(g)))μT(f)(m,h(a))  \\
-\mbox{}   & =  & (μ(T(g)))μ(m,(m',fh(a)) \\ &  = & μ(T(g))(mm',fh(a)) = (mm'm'',gfh(a))  \\
+g * f (b) & = & μ(d)T(g)f(b) = μ(d)T(g)(m,f(b)) \\ & = & μ(m,(m',gf(b))) = (mm',gf(b))   \\
+(g * f) * h(a) & = & μ(d)T(μ(d)T(g)f)h(a)  = μ(d)T(μ(d))(TT(g))T(f)(m,h(a))   \\
+\mbox{}    & = & μ(d)T(μ(d))(TT(g))(m,(m',fh(a))) \\ & = & μ(d)T(μ(d)(m,(m',(m'',gfh(a)))) =  (mm'm'',gfh(a))  \\
+g * (f * h)(a) & = & (μ(d)(T(g)))μ(c)T(f)h(a)  = (μ(d)(T(g)))μ(c)T(f)(m,h(a))  \\
+\mbox{}   & =  & (μ(d)(T(g)))μ(c)(m,(m',fh(a))) \\ &  = & μ(d)T(g)(mm',fh(a)) = (mm'm'',gfh(a))  \\
 \end{eqnarray*}
 
 
@@ -1294,26 +1294,26 @@
 -- naturality of $μ$
 
 --begin-comment:
-           μ_a
+           μ(a)
    TT(a) ---------> T(a)
       |              |
  TT(f)|              |T(f)
       |              |
-      v    μ_b       v
+      v    μ(b)       v
    TT(b) ---------> T(b)
 --end-comment:
 
 \begin{tikzcd}
-TT(a) \arrow{r}{μ_a} \arrow{d}{TT(f)} & T(a) \arrow{d}{T(f)} \\
-TT(b) \arrow{r}{μ_b} & T(b)
+TT(a) \arrow{r}{μ(a)} \arrow{d}{TT(f)} & T(a) \arrow{d}{T(f)} \\
+TT(b) \arrow{r}{μ(b)} & T(b)
 \end{tikzcd}
 
 
-$  μ_bTT(f)TT(a) = T(f)μ_aTT(a)$
+$  μ(b)TT(f)TT(a) = T(f)μ(a)TT(a)$
 
-$  μ_bTT(f)TT(a) = μ_b((m,(m',f(a))) = (m*m',f(a))$
+$  μ(b)TT(f)TT(a) = μ(b)((m,(m',f(a))) = (m*m',f(a))$
 
-$  T(f)μ_a(TT(a)) = T(f)(m*m',a) = (m*m',f(a))$
+$  T(f)μ(a)(TT(a)) = T(f)(m*m',a) = (m*m',f(a))$
 
 --μ○μ
 
@@ -1326,19 +1326,18 @@
 $μ_T(a) TTT(a) = μ_T(a) (m,(m',(m'',a))) = (m*m',(m'',a)) $
 
 --begin-comment:
-           μ_a
- TTTT(a) ---------> TTT(a)
-      |              |
- TT(μ)|              |T(μ)
-      |              |
-      v    μ_b       v
-  TTT(a) ---------> TT(a)
+               μ(TTT(a))
+      TTTT(a) ----------> TTT(a)
+           |               |
+ TT(μ(T(a))|               |T(μ(T(a)))
+           |               |
+           v   μ(TT(a))    v
+       TTT(a) -----------> TT(a)
 --end-comment:
 
-
 \begin{tikzcd}
-TTTT(a) \arrow{r}{μ_a} \arrow{d}{TT(μ)} & TTT(a) \arrow{d}{T(μ)} \\
-TTT(a) \arrow{r}{μ_b} & TT(a)
+TTTT(a) \arrow{r}{μ(TTT(a))} \arrow{d}[swap]{TT(μ)} & TTT(a) \arrow{d}{T(μ)} & \mbox{} \\
+TTT(a) \arrow{r}{μ(TT(a))} & TT(a) & \mbox{} \\
 \end{tikzcd}
 
 
--- a/nat.agda	Sat Jul 06 07:27:57 2013 +0900
+++ b/nat.agda	Sat Jul 06 08:50:32 2013 +0900
@@ -137,15 +137,27 @@
 -- f ○ η(a) = f
 
 
-record Kleisli  { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }
+record Kleisli  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )
+                 ( T : Functor A A )
+                 ( η : NTrans A A identityFunctor T )
+                 ( μ : NTrans A A (T ○ T) T )
+                 ( M : Monad A T η μ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
+     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 [ Trans μ c  o A [ FMap T g  o f ] ]
+
+open Kleisli
+Lemma7 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                  { T : Functor A A }
                  { η : NTrans A A identityFunctor T }
                  { μ : NTrans A A (T ○ T) T }
-                 { M : Monad A T η μ } : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
-     infix 9 _*_
-     _*_ : { a b c : Obj A } ->
-                      ( Hom A b ( FObj T c )) -> (  Hom A a ( FObj T b)) -> Hom A a ( FObj T c )
-     g * f = A [ Trans μ ({!!} (Category.cod A g))  o A [ FMap T g  o f ] ]
+                 { a b : Obj A } 
+                 { f : Hom A a ( FObj T b) } 
+                 { M : Monad A T η μ } 
+                 ( K : Kleisli A T η μ M) 
+                      -> A  [ join ? ? ?  ≈ f ]
+Lemma7 = \m -> {!!}
+