Mercurial > hg > Members > kono > Proof > category

changeset 301:93cf0a6c21fe

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 29 Sep 2013 14:43:47 +0900
parents d6a6dd305da2
children c5b2656dbec6
files comparison-functor.agda em-category.agda monoid-monad.agda
diffstat 3 files changed, 2 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/comparison-functor.agda	Sun Sep 29 14:01:07 2013 +0900
+++ b/comparison-functor.agda	Sun Sep 29 14:43:47 2013 +0900
@@ -37,7 +37,6 @@
 μ_K  = UεF A B U_K F_K ε_K 
 
 M : Monad A (U_K ○ F_K ) η_K μ_K 
--- M =  Adj2Monad A B {U_K} {F_K} {η_K} {ε_K} AdjK
 M =  Adj2Monad A B {U_K} {F_K} {η_K} {ε_K} AdjK
 
 open import kleisli {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } { η_K } { μ_K } { M } 
--- a/em-category.agda	Sun Sep 29 14:01:07 2013 +0900
+++ b/em-category.agda	Sun Sep 29 14:43:47 2013 +0900
@@ -279,7 +279,7 @@
              EMap (f ∙ ( emap-ε a ))
           ∎  )
        isNTrans1 : IsNTrans  Eilenberg-MooreCategory Eilenberg-MooreCategory ( F^T ○ U^T ) identityFunctor (λ a → emap-ε a )
-       isNTrans1 = record { commute = λ {a} {b} {f} →  (IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A)) )  (homomorphism f ) }  -- naturity1 {a} {b} {f}
+       isNTrans1 = record { commute = λ {a} {b} {f} → commute1 {a} {b} {f} }
                                                                                  
 --
 -- μ = U^T ε U^F
--- a/monoid-monad.agda	Sun Sep 29 14:01:07 2013 +0900
+++ b/monoid-monad.agda	Sun Sep 29 14:43:47 2013 +0900
@@ -21,7 +21,7 @@
   field
     Carrier  : Set c
     _∙_      : Op₂ Carrier
-    ε        : Carrier
+    ε        : Carrier   -- id in Monoid
     isMonoid : IsMonoid _≡_ _∙_ ε
 
 postulate M : ≡-Monoid c