--- a/free-monoid.agda	Sat Aug 31 12:53:35 2013 +0900
+++ b/free-monoid.agda	Sun Sep 01 13:26:30 2013 +0900
@@ -161,6 +161,7 @@
 
 open UniversalMapping
 
+--   [a,b,c] → f(a) ∙ f(b) ∙ f(c)
 Φ :  {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } →  List a -> Carrier b
 Φ {a} {b} {f} [] = ε b
 Φ {a} {b} {f} ( x :: xs ) = _∙_ b  ( f x ) (Φ {a} {b} {f} xs )
@@ -275,8 +276,16 @@
 fm-ε =  nat-ε A B {U} {Generator} {eta} FreeMonoidUniveralMapping 
 --  TMap fm-ε
 
-adjoint  = UMAdjunction  A B  U Generator eta FreeMonoidUniveralMapping 
+open Adjunction
 
+-- A = Sets {c}
+-- B = Monoids  
+-- U   underline funcotr
+-- F   generator = x :: []
+-- Eta          x :: []
+-- Epsiron      morph = Φ
+
+adj = UMAdjunction  A B  U Generator eta FreeMonoidUniveralMapping