Mercurial > hg > Members > kono > Proof > category

changeset 101:0f7086b6a1a6

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 15:17:15 +0900
parents 59dec035602c
children 09af60198ce5
files cat-utility.agda em-category.agda
diffstat 2 files changed, 74 insertions(+), 57 deletions(-) [+]
line wrap: on
line diff
--- a/cat-utility.agda	Tue Jul 30 17:58:20 2013 +0900
+++ b/cat-utility.agda	Wed Jul 31 15:17:15 2013 +0900
@@ -19,10 +19,10 @@
                          ( _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b )
                          : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
            field
-               universalMapping :   {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → 
-                             A [ A [ FMap U ( f * ) o  η a' ]  ≈ f ]
-               uniquness :   {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g :  Hom B (F a') b' } → 
-                             A [ A [ FMap U g o  η a' ]  ≈ f ] → B [ f * ≈ g ]
+               universalMapping :   {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → 
+                             A [ A [ FMap U ( f * ) o  η a ]  ≈ f ]
+               uniquness :   {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → { g :  Hom B (F a) b } → 
+                             A [ A [ FMap U g o  η a ]  ≈ f ] → B [ f * ≈ g ]
 
         record UniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
                          ( U : Functor B A )
--- a/em-category.agda	Tue Jul 30 17:58:20 2013 +0900
+++ b/em-category.agda	Wed Jul 31 15:17:15 2013 +0900
@@ -29,52 +29,91 @@
 --
 --  Hom in Eilenberg-Moore Category
 --
-
+open Functor
+open NTrans
 record IsEMAlgebra { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } 
-     (a : Obj A)  (φ  : FObj T a -> a ) : Set c₁
-  field
-     identity : A [ A [ φ  o TMap η a ] ≈ id1 A a ]
-     eval     : A [ A [ φ  o TMap μ a ] ≈ A [ φ o FMap T φ ]
+     (a : Obj A)  (φ  : Hom A (FObj T a) a ) : Set c₁ where
+   field
+       identity : A [ A [ φ  o TMap η a ] ≈ id1 A a ]
+       eval     : A [ A [ φ  o TMap μ a ] ≈ A [ φ o FMap T φ ] ]
 open IsEMAlgebra
 
 record EMAlgebra { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } 
-     (a : Obj A)  (φ  : FObj T a -> a ) : Set  c₂
+     (a : Obj A)  (φ  : FObj T a -> a ) : Set  c₂ where
   field
      isEMAlbgebra : IsEMAlgebra {c₁} {c₂} {ℓ} {A} {T} a φ 
 open EMAlgebra
      
 data EMObj { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A }
-     {a : Obj A}  {φ  : FObj T a -> a } {EMAlgebra a φ} : Set ( c₁ ⊔ c₂ )
-            emObj : (IsEMAlgebra a φ) -> EMObj {_} {_} {_} {_} {_} {a} {φ}
+     {a : Obj A}  {φ  : FObj T a -> a } {EMAlgebra a φ} : Set ( c₁ ⊔ c₂ ) where
+            emObj : \a φ -> (IsEMAlgebra a φ) -> EMObj { c₁} {c₂} {ℓ} {A} {T} {a} {φ}
+
+emobj : EMObj -> Obj A
+emobj (emObj x φ isAlgebra) = x
 
 record IsEMHom { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } 
+              {x y : Obj A} {φ  : FObj T x -> x } {φ'  : FObj T y -> y }
               (a : EMObj {c₁} {c₂} {ℓ} {A} {T} x φ  ) 
-              (b : EMObj {c₁} {c₂} {ℓ} {A} {T} y φ' ) : Set c₂ where
+              (b : EMObj {c₁} {c₂} {ℓ} {A} {T} y φ' ) 
+              (α : Hom A a b) : Set c₂ where
    field
-       homomorphism : A [ φ'  o FMap T α ]  ≈ A [ α  o φ ] ]
+       homomorphism : A [ A [ φ'  o FMap T α ]  ≈ A [ α  o φ ] ]
 open IsEMHom
 
 record EMHom { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } 
+              {x y : Obj A }
               (a : EMObj {c₁} {c₂} {ℓ} {A} {T} x) 
-              (b : EMObj {c₁} {c₂} {ℓ} {A} {T} y) : Set c₂ where
+              (b : EMObj {c₁} {c₂} {ℓ} {A} {T} y) 
+              {α : Hom A a b} : Set c₂ where
    field
        EMap :  Hom A x y
-       isEMHom : IsEMHom {c₁} {c₂} {ℓ} {A} {T} a b
+       isEMHom : IsEMHom {c₁} {c₂} {ℓ} {A} {T} a b α
 open EMHom
 
-EM-id : {x : Obj A} a : EMObj  EMObj {_} {_} {_} {_} {_} {a}) -> EMHom a a 
-EM-id {x = x} _ = record { EMap = id1 A x ; isEMHom = Lemma-EM1 x }
+Lemma-EM1 : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A }
+              {x : Obj A}
+              {φ : FObj T x -> x }
+              (a : EMObj {c₁} {c₂} {ℓ} {A} {T} x φ)
+               -> A [ A [ φ  o FMap T (id1 A x) ]  ≈ A [ (id1 A x) o φ ] ]
+Lemma-EM1 (emObj x φ isAlgebra ) = let open ≈-Reasoning (A) in
+   begin
+       φ o FMap T (id1 A x)
+   ≈⟨ cdr ( IsFunctor.identity (isFunctor T) ) ⟩
+       φ o (id1 A (FObj T x))
+   ≈⟨ idR ⟩
+       φ 
+   ≈⟨ sym idL ⟩
+       (id1 A x)  o φ
+   ∎
+
+EM-id : {a : EMObj } -> EMHom a a 
+EM-id  {a = a} = record { EMap = id1 A (emobj a) ; 
+     isEMHom = record { homomorphism = Lemma-EM1 a } }
 
 open import Relation.Binary.Core
 
+Lemma-EM2 : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A }
+              (a b : EMObj)
+              {x : Obj A}
+              {φ  : FObj T x -> x } 
+              (c : EMObj {c₁} {c₂} {ℓ} {A} {T} x φ)
+              (g : EMHom b c)
+              (f : EMHom a b) -> A [ A [ φ  o FMap T (A [ (EMap g)  o  (EMap f) ] ) ]  
+                      ≈ A [ (A [ (EMap g)  o  (EMap f) ])  o φ ] ]
+Lemma-EM2 _ _ (emObj c φ isAlgebra ) g f = let open ≈-Reasoning (A) in
+   begin
+        φ  o FMap T (A [ (EMap g)  o  (EMap f) ] )
+   ≈⟨ ? ⟩
+        ( (EMap g)  o  (EMap f) )  o φ
+   ∎
 _≗_ : { a : EMObj } { b : EMObj } (f g  : EMHom a b ) -> Set ℓ 
-_≗_ {a} {b} f g = A [ EMap f ≈ EMap g ]
+_≗_ f g = A [ EMap f ≈ EMap g ]
 
 _∙_ : { a b : EMObj A } → { c : EMObj A } →
-                      ( EMHom b c) → (  EMHom a b) → EMHom a c 
-_∙_ {a} {b} {c} g f = record { EMap = A [ (EMap g)  o  (EMap f) ; isEMHom = Lemma-EM2 a b c g f }
+                      ( EMHom b c) → (EMHom a b) → EMHom a c 
+_∙_ {a} {b} {c} g f = record { EMap = A [ (EMap g)  o  (EMap f) ] ; isEMHom = Lemma-EM2 a b c g f }
 
-isEilenberg-MooreCategory : IsCategory ( Obj A ) EMHom _⋍_ _*_ EM-id 
+isEilenberg-MooreCategory : IsCategory ( Obj A ) EMHom _≗_ _∙_ EM-id 
 isEilenberg-MooreCategory  = record  { isEquivalence =  isEquivalence 
                     ; identityL =   KidL
                     ; identityR =   KidR
@@ -84,29 +123,29 @@
      where
          open ≈-Reasoning (A) 
          isEquivalence :  { a b : Obj A } ->
-               IsEquivalence {_} {_} {EMHom a b} _⋍_
+               IsEquivalence {_} {_} {EMHom a b} _≗_
          isEquivalence {C} {D} =      -- this is the same function as A's equivalence but has different types
            record { refl  = refl-hom
              ; sym   = sym
              ; trans = trans-hom
              } 
-         KidL : {C D : Obj A} -> {f : EMHom C D} → (EM-id * f) ⋍ f
-         KidL {_} {_} {f} =  Lemma7 (EMap f) 
-         KidR : {C D : Obj A} -> {f : EMHom C D} → (f * EM-id) ⋍ f
-         KidR {_} {_} {f} =  Lemma8 (EMap f) 
+         KidL : {C D : Obj A} -> {f : EMHom C D} → (EM-id ∙ f) ≗ f
+         KidL {_} {_} {f} =  ? -- Lemma7 (EMap f) 
+         KidR : {C D : Obj A} -> {f : EMHom C D} → (f ∙ EM-id) ≗ f
+         KidR {_} {_} {f} =  ? -- Lemma8 (EMap f) 
          Ko-resp :  {a b c : Obj A} -> {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
+                          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 : Obj A} -> {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) 
+                          (f ∙ (g ∙ h)) ≗ ((f ∙ g) ∙ h)
+         Kassoc {_} {_} {_} {_} {f} {g} {h} =  ? -- Lemma9 (EMap f) (EMap g) (EMap h) 
 
 Eilenberg-MooreCategory : Category c₁ c₂ ℓ
 Eilenberg-MooreCategory =
   record { Obj = Obj A
          ; Hom = EMHom
-         ; _o_ = _*_
-         ; _≈_ = _⋍_
+         ; _o_ = _∙_
+         ; _≈_ = _≗_
          ; Id  = EM-id
          ; isCategory = isEilenberg-MooreCategory
          }
@@ -143,32 +182,10 @@
 --           ≈⟨ cdr (fcong T f≈g) ⟩
 --              TMap μ (b)  o FMap T (EMap g)
 --           ∎
---         distr1 :  {a b c : Obj A} {f : EMHom a b} {g : EMHom b c} → A [ ufmap (g * f) ≈ (A [ ufmap g o ufmap f ] )]
+--         distr1 :  {a b c : Obj A} {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 {a} {c} ( record { EMap = TMap μ (c) o (FMap T (EMap g)  o (EMap f)) } )
---           ≈⟨⟩
---              TMap μ (c)  o  FMap T ( TMap μ (c) o (FMap T (EMap g)  o (EMap f)))
---           ≈⟨ cdr ( distr T) ⟩
---              TMap μ (c)  o (( FMap T ( TMap μ (c)) o FMap T  (FMap T (EMap g)  o (EMap f))))
---           ≈⟨ assoc ⟩
---              (TMap μ (c)  o ( FMap T ( TMap μ (c)))) o FMap T  (FMap T (EMap g)  o (EMap f))
---           ≈⟨ car (sym (IsMonad.assoc (isMonad M))) ⟩
---              (TMap μ (c)  o ( TMap μ (FObj T c))) o FMap T  (FMap T (EMap g)  o (EMap f))
---           ≈⟨ sym assoc ⟩
---              TMap μ (c)  o (( TMap μ (FObj T c)) o FMap T  (FMap T (EMap g)  o (EMap f)))
---           ≈⟨ cdr (cdr (distr T)) ⟩
---              TMap μ (c)  o (( TMap μ (FObj T c)) o (FMap T  (FMap T (EMap g))  o FMap T (EMap f)))
---           ≈⟨ cdr (assoc) ⟩
---              TMap μ (c)  o ((( TMap μ (FObj T c)) o (FMap T  (FMap T (EMap g))))  o FMap T (EMap f))
---           ≈⟨ sym (cdr (car (nat μ ))) ⟩
---              TMap μ (c)  o ((FMap T (EMap g )  o  TMap μ (b))  o FMap T (EMap f ))
---           ≈⟨ cdr (sym assoc) ⟩
---              TMap μ (c)  o (FMap T (EMap g )  o  ( TMap μ (b)  o FMap T (EMap f )))
---           ≈⟨ assoc ⟩
---              ( TMap μ (c)  o FMap T (EMap g ) )  o  ( TMap μ (b)  o FMap T (EMap f ) )
+--              ufmap (g ∙ f)
 --           ≈⟨⟩
 --              ufmap g o ufmap f
 --           ∎