Mercurial > hg > Members > kono > Proof > category

changeset 115:17e69b05bc5e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
U^T and F^T problem written
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 01 Aug 2013 09:04:45 +0900
parents 2032c438b6a6
children 0e37b2cf3c73
files em-category.agda
diffstat 1 files changed, 77 insertions(+), 63 deletions(-) [+]
line wrap: on
line diff
--- a/em-category.agda	Thu Aug 01 02:50:28 2013 +0900
+++ b/em-category.agda	Thu Aug 01 09:04:45 2013 +0900
@@ -102,11 +102,25 @@
    ∎
 
 _∙_ :  {a b c : EMObj } -> EMHom b c -> EMHom a b -> EMHom a c
-_∙_ {a} {b} {c} g f = record { homomorphism = Lemma-EM2 a b c g f } 
+_∙_ {a} {b} {c} g f = record { EMap = A [ EMap g  o EMap f ] ; homomorphism = Lemma-EM2 a b c g f } 
 
 _≗_ : {a : EMObj } {b : EMObj } (f g : EMHom a b ) -> Set ℓ 
 _≗_ f g = A [ EMap f ≈ EMap g ]
 
+--
+-- 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} 
+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 } → 
+                          f ≗ g → h ≗ i → (h ∙ f) ≗ (i ∙ g)
+EMo-resp {a} {b} {c} {f} {g} {h} {i} = ( IsCategory.o-resp-≈ (Category.isCategory A) )
+EMassoc :   {a b c d : EMObj} -> {f : EMHom c d } → {g : EMHom b c } → {h : EMHom a b } →
+                          (f ∙ (g ∙ h)) ≗ ((f ∙ g) ∙ h)
+EMassoc {_} {_} {_} {_} {f} {g} {h} =   ( IsCategory.associative (Category.isCategory A) )
+
 isEilenberg-MooreCategory : IsCategory EMObj EMHom _≗_ _∙_  EM-id 
 isEilenberg-MooreCategory  = record  { isEquivalence =  isEquivalence 
                     ; identityL =   IsCategory.identityL (Category.isCategory A)
@@ -123,20 +137,6 @@
              ; sym   = sym
              ; trans = trans-hom
              } 
---
--- 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} 
-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 } → 
-                          f ≗ g → h ≗ i → (h ∙ f) ≗ (i ∙ g)
-EMo-resp {a} {b} {c} {f} {g} {h} {i} = ( IsCategory.o-resp-≈ (Category.isCategory A) )
-EMassoc :   {a b c d : EMObj} -> {f : EMHom c d } → {g : EMHom b c } → {h : EMHom a b } →
-                          (f ∙ (g ∙ h)) ≗ ((f ∙ g) ∙ h)
-EMassoc {_} {_} {_} {_} {f} {g} {h} =   ( IsCategory.associative (Category.isCategory A) )
-
 Eilenberg-MooreCategory : Category (c₁ ⊔ c₂ ⊔ ℓ) (c₁ ⊔ c₂ ⊔ ℓ) ℓ
 Eilenberg-MooreCategory =
   record { Obj = EMObj
@@ -147,52 +147,66 @@
          ; isCategory = isEilenberg-MooreCategory
           }
 
--- --
--- -- Resolution
--- --    T = U_T U_F
--- --      nat-ε
--- --      nat-η
--- --
--- -- 
--- -- 
--- -- U_T : Functor Eilenberg-MooreCategory A
--- -- U_T = record {
--- --         FObj = FObj T
--- --           ; FMap = ufmap
--- --         ; isFunctor = record
--- --         {      ≈-cong   = ≈-cong
--- --              ; identity = identity
--- --              ; distr    = distr1
--- --         }
--- --      } where
--- --         identity : {a : EMObj} →  A [ ufmap (EM-id a) ≈ id1 A (FObj T a) ]
--- --         identity {a} = let open ≈-Reasoning (A) in
--- --           begin
--- --               TMap μ (a)  o FMap T (TMap η a)
--- --           ≈⟨ IsMonad.unity2 (isMonad M) ⟩
--- --              id1 A (FObj T a)
--- --           ∎
--- --         ≈-cong : {a b : EMObj} {f g : EMHom a b} → A [ EMap f ≈ EMap g ] → A [ ufmap f ≈ ufmap g ]
--- --         ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (A) in
--- --           begin
--- --              TMap μ (b)  o FMap T (EMap f)
--- --           ≈⟨ cdr (fcong T f≈g) ⟩
--- --              TMap μ (b)  o FMap T (EMap g)
--- --           ∎
--- --         distr1 :  {a b c : EMObj} {f : EMHom a b} {g : EMHom b c} → A [ ufmap (g ∙ f) ≈ (A [ ufmap g o ufmap f ] )]
--- --         distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in
--- --           begin
--- --              ufmap (g ∙ f)
--- --           ≈⟨⟩
--- --              ufmap g o ufmap f
--- --           ∎
--- -- 
--- -- open MResolution
--- -- 
--- -- Resolution_T : MResolution A Eilenberg-MooreCategory T U_T F_T {nat-η} {nat-ε} {nat-μ} Adj_T 
--- -- Resolution_T = record {
--- --       T=UF   = Lemma11;
--- --       μ=UεF  = Lemma12 
--- --   }
--- -- 
+
+-- Resolution
+--   T = U^T U^F
+--     ε^t
+--     η^T
+
+U^T : Functor Eilenberg-MooreCategory A
+U^T = record {
+            FObj = \a -> obj a
+          ; FMap = \f -> EMap f
+        ; isFunctor = record
+        {      ≈-cong   = \eq -> eq
+             ; identity = refl-hom
+             ; distr    = refl-hom
+        }
+     } where open ≈-Reasoning (A) 
+
+Lemma-EM4 : (a : Obj A ) (phi : Hom A (FObj T a) a) -> A [ A [ phi  o TMap η a ] ≈ id1 A a ]
+Lemma-EM4 = ?
+
+Lemma-EM5 : (a : Obj A ) (phi : Hom A (FObj T a) a) -> A [ A [ phi  o TMap μ a ] ≈ A [ phi o FMap T phi ] ]
+Lemma-EM5 = ?
+
+ftobj : Obj A -> EMObj
+ftobj = \x -> record { a = FObj T x ; phi = TMap μ x; 
+ isAlgebra = record {
+      identity = Lemma-EM4 (FObj T x) ( TMap μ x);
+      eval     = Lemma-EM5 (FObj T x) ( TMap μ x)
+ } }
+
+Lemma-EM6 :  (a b : EMObj ) -> (f : Hom A (obj a) (obj b))  -> 
+      A [ A [ (φ b)  o FMap T f ]  ≈ A [ f  o (φ a) ] ]
+Lemma-EM6 = ?
+
+ftmap : {a b : Obj A} -> (Hom A a b) -> EMHom (ftobj a) (ftobj b)
+ftmap {a} {b} f = record { EMap = FMap T f; homomorphism =  Lemma-EM6 (ftobj a) (ftobj b) (FMap T f) }
+
+F^T : Functor A Eilenberg-MooreCategory
+F^T = record {
+        FObj = ftobj
+        ; FMap = ftmap
+        ; isFunctor = record {
+               ≈-cong   = ≈-cong   
+             ; identity = identity 
+             ; distr    = distr 
+        }
+     } where 
+        ≈-cong   : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → (ftmap f) ≗ (ftmap g)
+        ≈-cong   = ?
+        identity :  {a : Obj A} →  ftmap (id1 A a) ≗ EM-id {ftobj a}
+        identity = ?
+        distr    :  {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → ftmap (A [ g o f ]) ≗ ( ftmap g ∙ ftmap f )
+        distr    = ?
+
+--open MResolution
+--
+--Resolution_T : MResolution A Eilenberg-MooreCategory T U_T F_T {nat-η} {nat-ε} {nat-μ} Adj_T 
+--Resolution_T = record {
+--      T=UF   = Lemma11;
+--      μ=UεF  = Lemma12 
+--  }
+
 -- -- end