# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1376537568 -32400
# Node ID 5dc6f3f43507b9b8c50dab83c92def54b9b1b14d
# Parent  2f68a9e0167b630267929f05877b482a82ecaa1b
clean up

diff -r 2f68a9e0167b -r 5dc6f3f43507 monoid-monad.agda
--- a/monoid-monad.agda	Thu Aug 15 12:04:50 2013 +0900
+++ b/monoid-monad.agda	Thu Aug 15 12:32:48 2013 +0900
@@ -23,7 +23,6 @@
     _∙_      : Op₂ Carrier
     ε        : Carrier
     isMonoid : IsMonoid _≡_ _∙_ ε
-  open IsMonoid isMonoid public
 
 postulate Mono : ≡-Monoid c
 open ≡-Monoid
@@ -58,7 +57,7 @@
              (λ x → ε Mono , x) o f
         ∎
 
--- a → (ε,a)
+-- η : a → (ε,a)
 η : NTrans  A A identityFunctor T
 η = record {
        TMap = λ a → λ(x : a) → ( ε Mono , x ) ;
@@ -67,7 +66,7 @@
        }
   }
 
--- (m,(m',a)) → (m*m,a)
+-- μ : (m,(m',a)) → (m*m,a)
 
 muMap : (a : Obj A  ) → FObj T ( FObj T a ) → Σ (Carrier Mono) (λ x → a )
 muMap a ( m , ( m' , x ) ) = ( _∙_ Mono m  m'  ,  x )
@@ -104,7 +103,7 @@
 Lemma-MM36 : ∀{ x y z : Carrier Mono } → ((Mono ∙ (Mono ∙ x) y) z)  ≡ (_∙_ Mono  x (_∙_ Mono y z ) )
 Lemma-MM36  {x} {y} {z} = ( IsMonoid.assoc ( isMonoid Mono ))  x y z
 
--- Functional Extensionarity  (We cannot prove this in Agda / Coq, just assumming )
+-- Functional Extensionarity Axiom (We cannot prove this in Agda / Coq, just assumming )
 postulate Extensionarity : {f g : Carrier Mono → Carrier Mono } → (∀ {x} → (f x ≡ g x))  → ( f ≡ g ) 
 
 postulate Extensionarity3 : {f g : Carrier Mono → Carrier Mono → Carrier Mono → Carrier Mono } →