Mercurial > hg > Members > kono > Proof > category

diff em-category.agda @ 688:a5f2ca67e7c5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix monad/adjunction definition couniversal to limit does not work
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 11 Nov 2017 21:34:58 +0900
parents ba042c2d3ff5
children
line wrap: on
line diff
--- a/em-category.agda	Wed Nov 08 19:57:43 2017 +0900
+++ b/em-category.agda	Sat Nov 11 21:34:58 2017 +0900
@@ -24,7 +24,7 @@
                  { T : Functor A A }
                  { η : NTrans A A identityFunctor T }
                  { μ : NTrans A A (T ○ T) T }
-                 { M : Monad A T η μ } where
+                 { M : IsMonad A T η μ } where
 
 --
 --  Hom in Eilenberg-Moore Category
@@ -104,7 +104,7 @@
 -- cannot use as identityL = EMidL
 --
 EMidL : {C D : EMObj} → {f : EMHom C D} → (EM-id  ∙ f) ≗ f
-EMidL {C} {D} {f} = let open ≈-Reasoning (A) in idL {obj D} 
+EMidL {C} {D} {f} = let open ≈-Reasoning (A) in idL {obj C} 
 EMidR : {C D : EMObj} → {f : EMHom C D} → (f ∙ EM-id)  ≗ f
 EMidR {C} {_} {_} = let open ≈-Reasoning (A) in  idR {obj C}
 EMo-resp :  {a b c : EMObj} → {f g : EMHom a b } → {h i : EMHom  b c } → 
@@ -157,12 +157,11 @@
         }
      } where open ≈-Reasoning (A) 
 
-open Monad
 Lemma-EM4 : (x : Obj A ) → A [ A [ TMap μ x  o TMap η (FObj T x) ] ≈ id1 A (FObj T x) ]
 Lemma-EM4 x = let  open ≈-Reasoning (A) in
     begin
        TMap μ x  o TMap η (FObj T x) 
-    ≈⟨ IsMonad.unity1 (isMonad M) ⟩
+    ≈⟨ IsMonad.unity1 M ⟩
        id1 A (FObj T x)
     ∎
 
@@ -170,7 +169,7 @@
 Lemma-EM5 x =  let  open ≈-Reasoning (A) in
     begin
        ( TMap μ x)  o TMap μ (FObj T x) 
-    ≈⟨ IsMonad.assoc (isMonad M) ⟩
+    ≈⟨ IsMonad.assoc M ⟩
        ( TMap μ x) o FMap T ( TMap μ x)
     ∎
 
@@ -312,8 +311,12 @@
               TMap μ x
           ∎ )
 
-Adj^T : Adjunction A Eilenberg-MooreCategory U^T F^T η^T ε^T
+Adj^T : Adjunction A Eilenberg-MooreCategory 
 Adj^T = record {
+           U =  U^T ;
+           F =  F^T ;
+           η = η^T  ;
+           ε = ε^T ;
            isAdjunction = record {
                adjoint1 = λ {b} → IsAlgebra.identity (isAlgebra b) ; -- adjoint1
                adjoint2 = adjoint2
@@ -339,14 +342,20 @@
                   EMap (( TMap ε^T ( FObj F^T a )) ∙ ( FMap F^T ( TMap η^T a )) )
                ≈⟨⟩
                   TMap μ a  o FMap T ( TMap η a )
-               ≈⟨ IsMonad.unity2 (isMonad M) ⟩
+               ≈⟨ IsMonad.unity2 M ⟩
                   EMap (id1 Eilenberg-MooreCategory (FObj F^T a))
                ∎
 
 open MResolution
 
-Resolution^T : MResolution A Eilenberg-MooreCategory T U^T F^T {η^T} {ε^T} {μ^T} Adj^T 
+Resolution^T : MResolution A Eilenberg-MooreCategory  ( record { T = T ; η = η ; μ = μ; isMonad = M } )
 Resolution^T = record {
+     UR =  U^T ;
+     FR =  F^T ;
+     ηR =  η^T ;
+     εR =  ε^T ;
+     μR =  μ^T  ;
+     Adj = Adjunction.isAdjunction Adj^T ;
      T=UF = Lemma-EM8;
      μ=UεF  = Lemma-EM11
  }