Mercurial > hg > Members > kono > Proof > category

changeset 108:e763efd30868

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 31 Jul 2013 21:02:32 +0900
parents da14b7f03ff8
children ca1de7cbdf6a
files em-category.agda nat.agda
diffstat 2 files changed, 100 insertions(+), 96 deletions(-) [+]
line wrap: on
line diff
--- a/em-category.agda	Wed Jul 31 20:07:09 2013 +0900
+++ b/em-category.agda	Wed Jul 31 21:02:32 2013 +0900
@@ -31,33 +31,24 @@
 --
 open Functor
 open NTrans
-record IsEMAlgebra (a : Obj A) (φ : Hom A (FObj T a) a ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
+record IsEMObj (a : Obj A) (φ : Hom A (FObj T a) a ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
    field
        identity : A [ A [ φ  o TMap η a ] ≈ id1 A a ]
        eval     : A [ A [ φ  o TMap μ a ] ≈ A [ φ o FMap T φ ] ]
-open IsEMAlgebra
+open IsEMObj
 
-record EMAlgebra (a : Obj A)  (φ : Hom A (FObj T a) a ) : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
+record EMObj {a : Obj A}  {φ : Hom A (FObj T a) a } : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
    obj : Obj A
    obj = a
    phi : Hom A (FObj T a) a
    phi = φ
    field
-     isEMAlbgebra : IsEMAlgebra a φ 
-open EMAlgebra
-     
-data EMObj {a : Obj A}  {φ : Hom A (FObj T a) a }  : Set ( c₁ ⊔ c₂  ⊔ ℓ) where
-            emObj  : (EMAlgebra a φ) -> EMObj {a} {φ}
-
-emobj : {a : Obj A} -> {φ : Hom A (FObj T a) a } -> EMObj {a} {φ} -> Obj A
-emobj (emObj isAlgebra) = obj isAlgebra
-
-emphi : {a : Obj A} -> {φ : Hom A (FObj T a) a } -> EMObj {a} {φ} -> Hom A (FObj T a) a
-emphi (emObj isAlgebra) = phi isAlgebra 
+     isEMObj : IsEMObj a φ 
+open EMObj
 
 record IsEMHom {x y : Obj A} {φ  : Hom A (FObj T x) x } {φ'  : Hom A (FObj T y) y }
-              (a : EMObj {x} {φ}  ) 
-              (b : EMObj {y} {φ'} ) 
+              (a : EMObj {x} {φ}) 
+              (b : EMObj {y} {φ'}) 
               (α : Hom A x y) : Set ℓ where
    field
        homomorphism : A [ A [ φ'  o FMap T α ]  ≈ A [ α  o φ ] ]
@@ -81,7 +72,7 @@
 
 Lemma-EM1 : {x : Obj A} {φ : Hom A (FObj T x) x} (a : EMObj {x} {φ})
                -> A [ A [ φ  o FMap T (id1 A x) ]  ≈ A [ (id1 A x) o φ ] ]
-Lemma-EM1 {x} {φ} (emObj isAlgebra ) = let open ≈-Reasoning (A) in
+Lemma-EM1 {x} {φ} a = let open ≈-Reasoning (A) in
    begin
        φ o FMap T (id1 A x)
    ≈⟨ cdr ( IsFunctor.identity (isFunctor T) ) ⟩
@@ -93,7 +84,7 @@
    ∎
 
 EM-id : {x : Obj A} {φ : Hom A (FObj T x) x} {a : EMObj {x} {φ} } -> EMHom a a 
-EM-id {x} {φ} {a = a} = record { 
+EM-id {x} {φ} {a} = record { 
      isEMHom = record { homomorphism = Lemma-EM1 {x} {φ} a } } 
 
 open import Relation.Binary.Core
@@ -128,19 +119,33 @@
    ≈⟨ assoc ⟩
         ( (EMap g)  o  (EMap f) )  o φ
    ∎
-_≗_ : { a : EMObj } { b : EMObj } (f g  : EMHom a b ) -> Set ℓ 
-_≗_ f g = A [ EMap f ≈ EMap g ]
-
-_∙_ : { a b c : EMObj } → 
-                      ( EMHom b c) → (EMHom a b) → EMHom a c 
-_∙_ {a} {b} {c} g f = record { isEMHom = record { homomorphism = Lemma-EM2 a b c g f } }
 
-isEilenberg-MooreCategory : IsCategory EMObj EMHom _≗_ _∙_ EM-id 
+_∙_ : {x y z : Obj A}
+            {φ   : Hom A  (FObj T x) x}
+            {φ'  : Hom A  (FObj T y) y}
+            {φ'' : Hom A  (FObj T z) z}
+            {α  : Hom A x y}
+            {α' : Hom A y z}
+            {a : EMObj {x} {φ}   } 
+            {b : EMObj {y} {φ'}  } 
+            {c : EMObj {z} {φ''} } 
+            (g : EMHom {y} {z} {φ'} {φ''} {α'} b c ) ->
+            (f : EMHom {x} {y} {φ} {φ'} {α} a b) ->
+                (EMHom {x} {z} {φ} {φ''} {A [ α' o  α ] } a c)
+_∙_ {_} {_} {_} {_} {_} {_} {_} {_} {a} {b} {c} g f = record { isEMHom = record { homomorphism = Lemma-EM2 a b c g f } }
+
+_≗_ :  {x y : Obj A} {φ   : Hom A  (FObj T x) x} {φ'  : Hom A  (FObj T y) y} {α α' : Hom A x y} 
+            {a : EMObj {x} {φ} } {b : EMObj {y} {φ'}}
+            (f : EMHom {x} {y} {φ} {φ'} {α}  a b )
+            (g : EMHom {x} {y} {φ} {φ'} {α'} a b ) -> Set ℓ 
+_≗_ {_} {_} {_} {_} {α} {α'} f g = A [ α ≈ α' ]
+
+-- isEilenberg-MooreCategory : IsCategory EMObj EMHom _≗_ _∙_  EM-id 
 isEilenberg-MooreCategory  = record  { isEquivalence =  isEquivalence 
-                    ; identityL =   KidL
-                    ; identityR =   KidR
-                    ; o-resp-≈ =    Ko-resp
-                    ; associative = Kassoc
+                    ; identityL =   EMidL
+                    ; identityR =   EMidR
+                    ; o-resp-≈ =    EMo-resp
+                    ; associative = EMassoc
                     }
      where
          open ≈-Reasoning (A) 
@@ -151,73 +156,73 @@
              ; sym   = sym
              ; trans = trans-hom
              } 
-         KidL : {C D : EMObj} -> {f : EMHom C D} → (EM-id ∙ f) ≗ f
-         KidL {_} {_} {f} =  {!!} -- Lemma7 (EMap f) 
-         KidR : {C D : EMObj} -> {f : EMHom C D} → (f ∙ EM-id) ≗ f
-         KidR {_} {_} {f} =  {!!} -- Lemma8 (EMap f) 
-         Ko-resp :  {a b c : EMObj} -> {f g : EMHom a b } → {h i : EMHom  b c } → 
+         EMidL : {C D : EMObj} -> {f : EMHom C D} → (EM-id ∙ f) ≗ f
+         EMidL {_} {_} {f} =  {!!} -- Lemma7 (EMap f) 
+         EMidR : {C D : EMObj} -> {f : EMHom C D} → (f ∙ EM-id) ≗ f
+         EMidR {_} {_} {f} =  {!!} -- Lemma8 (EMap f) 
+         EMo-resp :  {a b c : EMObj} -> {f g : EMHom a b } → {h i : EMHom  b c } → 
                           f ≗ g → h ≗ i → (h ∙ f) ≗ (i ∙ g)
-         Ko-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = {!!} -- Lemma10 {a} {b} {c} (EMap f) (EMap g) (EMap h) (EMap i) eq-fg eq-hi
-         Kassoc :   {a b c d : EMObj} -> {f : EMHom c d } → {g : EMHom b c } → {h : EMHom a b } →
+         EMo-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = {!!} -- Lemma10 {a} {b} {c} (EMap f) (EMap g) (EMap h) (EMap i) eq-fg eq-hi
+         EMassoc :   {a b c d : EMObj} -> {f : EMHom c d } → {g : EMHom b c } → {h : EMHom a b } →
                           (f ∙ (g ∙ h)) ≗ ((f ∙ g) ∙ h)
-         Kassoc {_} {_} {_} {_} {f} {g} {h} =  {!!} -- Lemma9 (EMap f) (EMap g) (EMap h) 
+         EMassoc {_} {_} {_} {_} {f} {g} {h} =  {!!} -- Lemma9 (EMap f) (EMap g) (EMap h) 
 
-Eilenberg-MooreCategory : Category (c₁ ⊔ c₂ ⊔ ℓ) (c₁ ⊔ c₂ ⊔ ℓ) ℓ
-Eilenberg-MooreCategory =
-  record { Obj = EMObj
-         ; Hom = EMHom
-         ; _o_ = _∙_
-         ; _≈_ = _≗_
-         ; Id  = EM-id
-         ; isCategory = isEilenberg-MooreCategory
-         }
+-- Eilenberg-MooreCategory : Category (c₁ ⊔ c₂ ⊔ ℓ) (c₁ ⊔ c₂ ⊔ ℓ) ℓ
+-- Eilenberg-MooreCategory =
+--   record { Obj = EMObj
+--          ; Hom = EMHom
+--          ; _o_ = _∙_
+--          ; _≈_ = _≗_
+--          ; Id  = EM-id
+--          ; 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
+-- --      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 
+-- --   }
+-- -- 
 -- -- end
--- a/nat.agda	Wed Jul 31 20:07:09 2013 +0900
+++ b/nat.agda	Wed Jul 31 21:02:32 2013 +0900
@@ -227,8 +227,7 @@
 _⋍_ : { a : Obj A } { b : Obj A } (f g  : KHom a b ) -> Set ℓ 
 _⋍_ {a} {b} f g = A [ KMap f ≈ KMap g ]
 
-_*_ : { a b : Obj A } → { c : Obj A } →
-                      ( KHom b c) → (  KHom a b) → KHom a c 
+_*_ : { a b c : Obj A } → ( KHom b c) → (  KHom a b) → KHom a c 
 _*_ {a} {b} {c} g f = record { KMap = join K {a} {b} {c} (KMap g) (KMap f) }
 
 isKleisliCategory : IsCategory ( Obj A ) KHom _⋍_ _*_ K-id