# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1376207777 -32400
# Node ID 3f3870e867f2bb40af4861b392d51ffe877dbe18
# Parent  de1c3443f10d8e46e6a039df2dacb0cda2b9eeeb
on going...

diff -r de1c3443f10d -r 3f3870e867f2 monoid-monad.agda
--- a/monoid-monad.agda	Sun Aug 11 16:35:15 2013 +0900
+++ b/monoid-monad.agda	Sun Aug 11 16:56:17 2013 +0900
@@ -67,4 +67,27 @@
          ; isCategory = isT1Category
          }
 
+tobj : ( a : T1 M A ) -> T1 M A
+tobj (T1a a)  =  T1a a
+tobj (T1t a t)  =  T1t a t
 
+tfmap : {a b : T1 M A } ( f : T1Hom a b ) -> T1Hom (tobj a) (tobj b)
+tfmap f = ? -- record { T1Map = T1Map f }
+
+T : Functor T1Category T1Category
+T = record {
+        FObj = \a -> tobj a
+        ; FMap = tfmap
+        ; isFunctor = record
+        { ≈-cong   = ≈-cong
+             ; identity = identity
+             ; distr    = distr1
+        }
+    } where
+        ≈-cong   : {a b : T1 M A} {f g : T1Hom a b} → f ⋍ g → tfmap f ⋍ tfmap g
+        ≈-cong   = ?
+        identity : {a : T1 M A} →  ((tfmap (T1-id {a} )) ⋍ (T1-id { tobj a })) 
+        identity = ?
+        distr1    :  {a b c : T1 M A} {f : T1Hom a b} {g : T1Hom b c} → 
+                 ( tfmap ( g ∙ f) ⋍  ( tfmap g ∙ tfmap f ) )
+        distr1    = ?