Mercurial > hg > Members > kono > Proof > category

changeset 69:84a150c980ce

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
generalized distr and assco1
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 25 Jul 2013 14:46:02 +0900
parents 829e0698f87f
children fb3c48b375b3
files HomReasoning.agda cat-utility.agda nat.agda
diffstat 3 files changed, 49 insertions(+), 40 deletions(-) [+]
line wrap: on
line diff
--- a/HomReasoning.agda	Thu Jul 25 13:56:16 2013 +0900
+++ b/HomReasoning.agda	Thu Jul 25 14:46:02 2013 +0900
@@ -78,20 +78,26 @@
 --             B [ a ≈ b ] → (f : Hom B x y → Hom A x' y' ) →  f a ≈ f b
 --  cong-≈ refl f = refl-hom
 
-  assoc :   {a b c d : Obj A }  {f : Hom A c d}  {g : Hom A b c} {h : Hom A a b}
-                                  →  f o ( g o h )  ≈ ( f o g ) o h
+  assoc : {a b c d : Obj A }  {f : Hom A c d}  {g : Hom A b c} {h : Hom A a b}
+                                  →  A [ A [ f o ( A [ g o h ] ) ] ≈ A [ ( A [ f o g ] ) o h ] ]
   assoc =  IsCategory.associative (Category.isCategory A)
 
-  distr : { c₁′ c₂′ ℓ′ : Level}  {D : Category c₁′ c₂′ ℓ′} (T : Functor D A) →  {a b c : Obj D} {g : Hom D b c} { f : Hom D a b }
-     →   FMap T ( D [ g o f ]  )  ≈  FMap T g o FMap T f 
+  -- slow but working on another cateogry
+  assoc1 : { c₁ c₂ ℓ : Level}  {A : Category c₁ c₂ ℓ}   {a b c d : Obj A }  {f : Hom A c d}  {g : Hom A b c} {h : Hom A a b}
+                                  →  A [ A [ f o ( A [ g o h ] ) ] ≈ A [ ( A [ f o g ] ) o h ] ]
+  assoc1 {_} {_} {_} {A} =  IsCategory.associative (Category.isCategory A)
+
+  distr : { c₁ c₂ ℓ : Level}  {A : Category c₁ c₂ ℓ} 
+         { c₁′ c₂′ ℓ′ : Level}  {D : Category c₁′ c₂′ ℓ′} (T : Functor D A) →  {a b c : Obj D} {g : Hom D b c} { f : Hom D a b }
+     →   A [ FMap T ( D [ g o f ]  )  ≈  A [ FMap T g o FMap T f ] ]
   distr {_} T = IsFunctor.distr ( isFunctor T )
 
   open NTrans 
-  nat : { c₁′ c₂′ ℓ′ : Level}  {D : Category c₁′ c₂′ ℓ′} {a b : Obj D} {f : Hom D a b}  {F G : Functor D A }
+  nat : { c₁ c₂ ℓ : Level}  {A : Category c₁ c₂ ℓ}  { c₁′ c₂′ ℓ′ : Level}  {D : Category c₁′ c₂′ ℓ′} 
+         {a b : Obj D} {f : Hom D a b}  {F G : Functor D A }
       →  (η : NTrans D A F G )
-      →   FMap G f  o  TMap η a   ≈ TMap η b  o  FMap F f
-  nat {_} η  =  IsNTrans.naturality ( isNTrans η  )
-
+      →   A [ A [ FMap G f  o  TMap η a ]  ≈ A [ TMap η b  o  FMap F f ] ]
+  nat η  =  IsNTrans.naturality ( isNTrans η  )
 
   infixr  2 _∎
   infixr 2 _≈⟨_⟩_ _≈⟨⟩_ 
--- a/cat-utility.agda	Thu Jul 25 13:56:16 2013 +0900
+++ b/cat-utility.agda	Thu Jul 25 14:46:02 2013 +0900
@@ -92,7 +92,7 @@
                (FMap F ( FMap H f )) o  ( FMap F (TMap n a))
             ≈⟨ sym (distr F) ⟩
                FMap F ( B [ (FMap H f)  o TMap n a ])
-            ≈⟨ IsFunctor.≈-cong (isFunctor F) ( IsNTrans.naturality ( isNTrans n)  ) ⟩
+            ≈⟨ IsFunctor.≈-cong (isFunctor F) ( nat n ) ⟩
                FMap F ( B [ (TMap n b ) o FMap G f ] )
             ≈⟨ distr F ⟩
                (FMap F (TMap n b )) o  (FMap F (FMap G f))
--- a/nat.agda	Thu Jul 25 13:56:16 2013 +0900
+++ b/nat.agda	Thu Jul 25 14:46:02 2013 +0900
@@ -203,41 +203,44 @@
      join k ( join k h g) f 
   ∎ where open ≈-Reasoning (A) 
 
--- Kleisli-join : {!!}
--- Kleisli-join = {!!}
+KHom : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → ( T : Functor A A )  {a b : Obj A} →  {!!} -> {!!} -> Set c₂
+KHom = {!!}
+
+Kleisli-join : {!!}
+Kleisli-join = {!!}
 
--- Kleisli-id : {!!}
--- Kleisli-id = {!!}
+Kleisli-id : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( T : Functor A A )  {a : Obj A} → Hom A a (FObj T a)
+Kleisli-id A T = {!!}
 
--- Lemma10 : {!!}
--- Lemma10 = {!!}
+Lemma10 : {!!}
+Lemma10 = {!!}
 
--- open import Relation.Binary.Core
+open import Relation.Binary.Core
 
--- isKleisliCategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
---                  { T : Functor A A }
---                  { η : NTrans A A identityFunctor T }
---                  { μ : NTrans A A (T ○ T) T }
---                  ( m : Monad A T η μ )
---                  { k : Kleisli A T η μ m} →
---          IsCategory ( Obj A ) ( Hom A ) ( Category._≈_ A ) ( Kleisli-join ) Kleisli-id
--- isKleisliCategory A {T} {η} m = record  { isEquivalence =  IsCategory.isEquivalence ( Category.isCategory A )
---                     ; identityL =   {!!}
---                     ; identityR =   {!!}
---                     ; o-resp-≈ =    {!!}
---                     ; associative = {!!}
---                     }
---      where
---          KidL : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) { T : Functor A A }
---                  { η : NTrans A A identityFunctor T }
---                  { μ : NTrans A A (T ○ T) T } ( m : Monad A T η μ ) → {!!}
---          KidL = {!!}
---          KidR : {!!}
---          KidR = {!!}
---          Ko-resp : {!!}
---          Ko-resp = {!!}
---          Kassoc : {!!}
---          Kassoc = {!!}
+isKleisliCategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
+                 { T : Functor A A }
+                 { η : NTrans A A identityFunctor T }
+                 { μ : NTrans A A (T ○ T) T }
+                 ( m : Monad A T η μ )
+                 { k : Kleisli A T η μ m} →
+         IsCategory ( Obj A ) ( KHom A T ) ( Category._≈_ A ) ( Kleisli-join ) (Kleisli-id A T)
+isKleisliCategory A {T} {η} m = record  { isEquivalence =  IsCategory.isEquivalence ( Category.isCategory A )
+                    ; identityL =   {!!}
+                    ; identityR =   {!!}
+                    ; o-resp-≈ =    {!!}
+                    ; associative = {!!}
+                    }
+     where
+         KidL : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) { T : Functor A A }
+                 { η : NTrans A A identityFunctor T }
+                 { μ : NTrans A A (T ○ T) T } ( m : Monad A T η μ ) → {!!}
+         KidL = {!!}
+         KidR : {!!}
+         KidR = {!!}
+         Ko-resp : {!!}
+         Ko-resp = {!!}
+         Kassoc : {!!}
+         Kassoc = {!!}
 
 -- Kleisli :
 -- Kleisli = record { Hom =