Mercurial > hg > Members > kono > Proof > category

changeset 150:5dc6f3f43507

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 15 Aug 2013 12:32:48 +0900
parents 2f68a9e0167b
children 3bd5109c83f3
files monoid-monad.agda
diffstat 1 files changed, 3 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- 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 } →