Mercurial > hg > Members > kono > Proof > category

changeset 135:3f3870e867f2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 11 Aug 2013 16:56:17 +0900
parents de1c3443f10d
children a9f5cfbbc0fa
files monoid-monad.agda
diffstat 1 files changed, 23 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- 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    = ?