Mercurial > hg > Members > kono > Proof > category

changeset 78:b3c023f7c929

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 Sat, 27 Jul 2013 03:52:24 +0900
parents 528c7e27af91
children 84723389e3c9
files nat.agda
diffstat 1 files changed, 33 insertions(+), 23 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Fri Jul 26 22:07:21 2013 +0900
+++ b/nat.agda	Sat Jul 27 03:52:24 2013 +0900
@@ -203,7 +203,7 @@
 
 
 record KHom (a : Obj A)  (b : Obj A)
-     : Set (suc (c₂ ⊔ c₁)) where
+     : Set c₂ where
    field
        KMap :  Hom A a ( FObj T b )
 
@@ -253,7 +253,7 @@
                           (f * (g * h)) ⋍ ((f * g) * h)
          Kassoc {_} {_} {_} {_} {f} {g} {h} =  Lemma9 (KMap f) (KMap g) (KMap h) 
 
-KleisliCategory : Category c₁ (suc (c₂ ⊔ c₁)) ℓ
+KleisliCategory : Category c₁ c₂ ℓ
 KleisliCategory =
   record { Obj = Obj A
          ; Hom = KHom
@@ -376,30 +376,40 @@
              KMap  ( ffmap g * ffmap f )
           ∎
 
-nat-ε : NTrans KleisliCategory KleisliCategory identityFunctor ( F_T ○ U_T )
-nat-ε = record { TMap = \a -> id1 A ( FObj T a ) ; isNTrans = isNTrans } where
-       naturality : ?
-       naturality = ?
-       isNtrans : IsNTrans  KleisliCategory KleisliCategory identityFunctor ( F_T  ○ U_T )
-       isNtrans = record { naturality = naturality }
+
+nat-η : NTrans A A identityFunctor ( U_T ○ F_T ) 
+nat-η = record { TMap = \x -> TMap η x ; isNTrans = isNTrans1 } where
+       isNTrans1 : IsNTrans A A identityFunctor ( U_T ○ F_T ) (\a -> TMap η a)
+       isNTrans1 = {!!}
 
-Lemma11 : {a : Obj A } -> A [ TMap μ a ≈ FMap U_T ( TMap nat-ε ( FObj F_T a ) ) ]
-Lemma11 = ?
+tmap-ε : (a : Obj A) -> KHom ? ?
+tmap-ε a = record { KMap = id1 A (FObj T a) }
+
+nat-ε : NTrans KleisliCategory KleisliCategory  ( F_T ○ U_T ) identityFunctor
+nat-ε = record { TMap = \a -> tmap-ε a; isNTrans = isNTrans1 } where
+       naturality : {a b : Obj A} {f : KHom a b}
+            →  (f * ( tmap-ε a ) ) ⋍   (( tmap-ε b ) * (  FMap (F_T ○ U_T) f ) )
+       naturality = {!!}
+       isNTrans1 : IsNTrans  KleisliCategory KleisliCategory ( F_T ○ U_T ) identityFunctor (\a -> tmap-ε a )
+       isNTrans1 = record { naturality = naturality } 
 
---Lemma12 : T = F_T  ○ U_T
---Lemma12 = ?
+Lemma11 : {x : Obj A } -> A [ TMap μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ]
+Lemma11 = {!!}
+
+Lemma12 : T ≃  (U_T ○ F_T)
+Lemma12 = {!!}
 
-Resoution_T : Adjunction A KleisliCategory U_T F_T η nat-ε 
-Resoution_T = record {
-           isAdjunction = record {
-               adjoint1 = adjoint1 ; 
-               adjoint2 = adjoint2
-           } 
-       } where
-           adjoint1 : ?
-           adjoint1 = ?
-           adjoint2 : ?
-           adjoint2 = ?
+-- Resoution_T : Adjunction A KleisliCategory U_T F_T nat-η nat-ε 
+-- Resoution_T = record {
+--            isAdjunction = record {
+--                adjoint1 = adjoint1 ; 
+--                adjoint2 = adjoint2
+--            } 
+--        } where
+--            adjoint1 : ?
+--            adjoint1 = ?
+--            adjoint2 : ?
+--            adjoint2 = ?