Mercurial > hg > Members > kono > Proof > category

changeset 122:f8fbd5ecec97

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
no yellow on em-category
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 02 Aug 2013 08:21:32 +0900
parents 324511654f23
children 44c58c27d12d
files comparison-em.agda em-category.agda
diffstat 2 files changed, 17 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/comparison-em.agda	Thu Aug 01 18:14:42 2013 +0900
+++ b/comparison-em.agda	Fri Aug 02 08:21:32 2013 +0900
@@ -24,9 +24,9 @@
       { U^K : Functor B A } { F^K : Functor A B }
       { η^K : NTrans A A identityFunctor ( U^K ○ F^K ) }
       { ε^K : NTrans B B ( F^K ○ U^K ) identityFunctor } 
-      { μ^K' : NTrans A A (( U^K ○ F^K ) ○ ( U^K ○ F^K )) ( U^K ○ F^K ) }
+      { μ^K : NTrans A A (( U^K ○ F^K ) ○ ( U^K ○ F^K )) ( U^K ○ F^K ) }
       ( Adj^K : Adjunction A B U^K F^K η^K ε^K )
-      ( RK : MResolution A B T U^K F^K {η^K} {ε^K} {μ^K'} AdjK )
+      ( RK : MResolution A B T U^K F^K {η^K} {ε^K} {μ^K} Adj^K )
 where
 
 open import adj-monad
@@ -36,17 +36,13 @@
 M : Monad A (U^K ○ F^K ) η^K μ^K 
 M =  Adj2Monad A B {U^K} {F^K} {η^K} {ε^K} Adj^K
 
-K : Eilenberg-MooreCategory A (U^K ○ F^K ) η^K μ^K M 
-K = record {}
-
-open import nat {c₁} {c₂} {ℓ} {A} { U^K ○ F^K } { η^K } { μ^K } { M } { K }
+open import em-category {c₁} {c₂} {ℓ} {A} { U^K ○ F^K } { η^K } { μ^K } { M } 
 
 open Functor
 open NTrans
-open Eilenberg-MooreCategory
-open EMHom
 open Adjunction
 open MResolution
+open Eilenberg-Moore-Hom
 
 emkobj : Obj B -> EMObj
 emkobj b = record { 
@@ -58,7 +54,7 @@
       eval1 = ?
 
 emkmap : {a b : Obj B} (f : Hom B a b) -> EMHom (emkobj a) (emkobj b)
-emkmap {a} {b} f = record { EMap = FMap U f ; homomorphism = homomorphism1 
+emkmap {a} {b} f = record { EMap = FMap U^K f ; homomorphism = homomorphism1 
   } where
       homomorphism1 : ?
       homomorphism1 = ?
@@ -73,24 +69,24 @@
              ; distr    = distr1
         }
      }  where
-         identity : {a : Obj A} →  B [ emkmap (K-id {a}) ≈ id1 B (FObj F^K a) ]
+         identity : {a : Obj A} →  B [ emkmap (EM-id {a}) ≈ id1 B (FObj F^K a) ]
          identity {a} = let open ≈-Reasoning (B) in
            begin
-               emkmap (K-id {a})
+               emkmap (EM-id {a})
            ≈⟨ ? ⟩
               id1 B (FObj F^K a)
            ∎
-         ≈-cong : {a b : Obj A} -> {f g : EMHom a b} → A [ KMap f ≈ KMap g ] → B [ emkmap f ≈ emkmap g ]
+         ≈-cong : {a b : Obj A} -> {f g : EMHom a b} → A [ EMap f ≈ EMap g ] → B [ emkmap f ≈ emkmap g ]
          ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in
            begin
                emkmap f
            ≈⟨ ? ⟩
                emkmap g
            ∎
-         distr1 :  {a b c : Obj A} {f : EMHom a b} {g : EMHom b c} → B [ emkmap (g * f) ≈ (B [ emkmap g o emkmap f ] )]
+         distr1 :  {a b c : Obj A} {f : EMHom a b} {g : EMHom b c} → B [ emkmap (g ∙ f) ≈ (B [ emkmap g o emkmap f ] )]
          distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (B) in
            begin
-              emkmap (g * f)
+              emkmap (g ∙ f)
            ≈⟨ ? ⟩
               emkmap g o emkmap f
            ∎
--- a/em-category.agda	Thu Aug 01 18:14:42 2013 +0900
+++ b/em-category.agda	Fri Aug 02 08:21:32 2013 +0900
@@ -279,8 +279,7 @@
              EMap (f ∙ ( emap-ε a ))
           ∎  )
        isNTrans1 : IsNTrans  Eilenberg-MooreCategory Eilenberg-MooreCategory ( F^T ○ U^T ) identityFunctor (\a -> emap-ε a )
-       isNTrans1 = record { naturality = naturality1 }
-
+       isNTrans1 = record { naturality = \{a} {b} {f} ->  (IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A)) )  (homomorphism f ) }  -- naturity1 {a} {b} {f}
                                                                                  
 --
 -- μ = U^T ε U^F
@@ -329,19 +328,21 @@
 Adj^T : Adjunction A Eilenberg-MooreCategory U^T F^T η^T ε^T
 Adj^T = record {
            isAdjunction = record {
-               adjoint1 = adjoint1 ;
+               adjoint1 = \{b} -> IsAlgebra.identity (isAlgebra b) ; -- adjoint1
                adjoint2 = adjoint2
            }
        } where
-           adjoint1 :   { b : Obj Eilenberg-MooreCategory } →
+           adjoint1 :   { b : EMObj } →
                      A [ A [ ( FMap U^T ( TMap ε^T b))  o ( TMap η^T ( FObj U^T b )) ]  ≈ id1 A (FObj U^T b) ]
            adjoint1 {b} =  let open ≈-Reasoning (A) in
                begin
                   ( FMap U^T ( TMap ε^T b))  o ( TMap η^T ( FObj U^T b ))
                ≈⟨⟩ 
                    φ b  o TMap η (obj b)
-               ≈⟨ IsAlgebra.identity (isAlgebra b ) ⟩
-                  id1 A (FObj U^T b)
+               ≈⟨ IsAlgebra.identity (isAlgebra b) ⟩
+                   id1 A (a b)
+               ≈⟨⟩ 
+                   id1 A (FObj U^T b)
                ∎
            adjoint2 :   {a : Obj A} →
                      Eilenberg-MooreCategory [ Eilenberg-MooreCategory [ ( TMap ε^T ( FObj F^T a ))  o ( FMap F^T ( TMap η^T a )) ]