Mercurial > hg > Members > kono > Proof > category

changeset 75:8e665152c306

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Comparison Functor
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 26 Jul 2013 19:52:19 +0900
parents 49e6eb3ef9c0
children 6c6c3dd8ef12
files HomReasoning.agda nat.agda
diffstat 2 files changed, 97 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/HomReasoning.agda	Fri Jul 26 16:18:32 2013 +0900
+++ b/HomReasoning.agda	Fri Jul 26 19:52:19 2013 +0900
@@ -74,9 +74,18 @@
   sym   =  IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A))
 
 -- How to prove this?
+  ≡-≈ : {a b : Obj A } { x y : Hom A a b } →  (x≈y : x ≡ y ) → x ≈ y
+  ≡-≈  refl = refl-hom
+
+--  ≈-≡ : {a b : Obj A } { x y : Hom A a b } →  (x≈y : x ≈ y ) → x ≡ y
+--  ≈-≡  x≈y = irr x≈y
+  ≡-cong : { c₁′ c₂′ ℓ′ : Level}  {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A }  →
+             a ≡ b  → (f : Hom B x y → Hom A x' y' ) →  f a  ≈  f b
+  ≡-cong refl f =  ≡-≈ refl
+
 --  cong-≈ :  { c₁′ c₂′ ℓ′ : Level}  {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A }  → 
 --             B [ a ≈ b ] → (f : Hom B x y → Hom A x' y' ) →  f a ≈ f b
---  cong-≈ refl f = refl-hom
+--  cong-≈ eq f = {!!}
 
   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 ] ]
@@ -90,7 +99,14 @@
   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 )
+  distr T = IsFunctor.distr ( isFunctor T )
+
+  resp : {a b c : Obj A} {f g : Hom A a b} {h i : Hom A b c} → f ≈ g → h ≈ i → (h o f) ≈ (i o g)
+  resp = IsCategory.o-resp-≈ (Category.isCategory A)
+
+  fcong :  { c₁ c₂ ℓ : Level}  {C : Category c₁ c₂ ℓ}
+         { c₁′ c₂′ ℓ′ : Level}  {D : Category c₁′ c₂′ ℓ′} {a b : Obj C} {f g : Hom C a b} → (T : Functor C D) → C [ f ≈ g ] → D [ FMap T f ≈ FMap T g ]
+  fcong T = IsFunctor.≈-cong (isFunctor T) 
 
   open NTrans 
   nat : { c₁ c₂ ℓ : Level}  {A : Category c₁ c₂ ℓ}  { c₁′ c₂′ ℓ′ : Level}  {D : Category c₁′ c₂′ ℓ′} 
--- a/nat.agda	Fri Jul 26 16:18:32 2013 +0900
+++ b/nat.agda	Fri Jul 26 19:52:19 2013 +0900
@@ -253,4 +253,83 @@
                           (f * (g * h)) ⋍ ((f * g) * h)
          Kassoc {_} {_} {_} {_} {f} {g} {h} =  Lemma9 (KMap f) (KMap g) (KMap h) 
 
+KleisliCategory : Category c₁ (suc (c₂ ⊔ c₁)) ℓ
+KleisliCategory =
+  record { Obj = Obj A
+         ; Hom = KHom
+         ; _o_ = _*_
+         ; _≈_ = _⋍_
+         ; Id  = K-id
+         ; isCategory = isKleisliCategory
+         }
 
+U_T : Functor KleisliCategory A
+U_T = record {
+        FObj = FObj T
+          ; FMap = ufmap
+        ; isFunctor = record
+        {      ≈-cong   = ≈-cong
+             ; identity = identity
+             ; distr    = distr
+        }
+     } where
+        ufmap : {a b : Obj A} (f : KHom a b ) -> Hom A (FObj T a) (FObj T b)
+        ufmap {a} {b} f =  A [ TMap μ (b)  o FMap T (KMap f) ]
+        identity : {a : Obj A} →  A [ ufmap (K-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 : Obj A} {f g : KHom a b} → A [ KMap f ≈ KMap g ] → A [ ufmap f ≈ ufmap g ]
+        ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (A) in
+          begin
+             TMap μ (b)  o FMap T (KMap f)
+          ≈⟨ cdr (fcong T f≈g) ⟩
+             TMap μ (b)  o FMap T (KMap g)
+          ∎
+        distr :  {a b c : Obj A} {f : KHom a b} {g : KHom b c} → A [ ufmap (g * f) ≈ (A [ ufmap g o ufmap f ] )]
+        distr {_} {_} {c} {f} {g} = let open ≈-Reasoning (A) in
+          begin
+             ufmap (g * f)
+--          ≈⟨⟩
+--             TMap μ (FObj T c)  o FMap T ( (TMap μ (c) o FMap T (KMap g))  o (KMap f))
+          ≈⟨ {!!} ⟩
+             ufmap g o ufmap f
+          ∎
+
+
+ffmap :  {a b : Obj A} (f : Hom A a b) -> KHom a b
+ffmap f = record { KMap = A [ TMap η (Category.cod A f) o f ] }
+
+F_T : Functor A KleisliCategory
+F_T = record {
+        FObj = \a -> a
+        ; FMap = ffmap
+        ; isFunctor = record
+        { ≈-cong   = ≈-cong
+             ; identity = identity
+             ; distr    = distr
+        }
+     } where
+        identity : {a : Obj A} →  A [ A [ TMap η a o id1 A a ] ≈ TMap η a  ]
+        identity {a} = IsCategory.identityR ( Category.isCategory A)
+        lemma1 : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ TMap η b  ≈  TMap η b ]
+        lemma1 f≈g = IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))
+        ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ A [ TMap η (Category.cod A f) o f ] ≈ A [ TMap η (Category.cod A g) o g ] ]
+        ≈-cong f≈g =  (IsCategory.o-resp-≈ (Category.isCategory A)) f≈g ( lemma1  f≈g )
+        distr :  {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → 
+                 ( ffmap (A [ g o f ]) ⋍  ( ffmap g * ffmap f ) )
+        distr {_} {_} {_} {f} {g} =  let open ≈-Reasoning (A) in
+          begin
+             KMap (ffmap (A [ g o f ]))
+          ≈⟨ {!!} ⟩
+             KMap  ( ffmap g * ffmap f )
+          ∎
+
+
+
+
+
+