Mercurial > hg > Members > kono > Proof > category

changeset 77:528c7e27af91

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Resolution U_T, F_T
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 26 Jul 2013 22:07:21 +0900
parents 6c6c3dd8ef12
children b3c023f7c929
files nat.agda
diffstat 1 files changed, 55 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Fri Jul 26 20:54:41 2013 +0900
+++ b/nat.agda	Fri Jul 26 22:07:21 2013 +0900
@@ -341,15 +341,67 @@
         ≈-cong f≈g =  (IsCategory.o-resp-≈ (Category.isCategory A)) f≈g ( lemma1  f≈g )
         distr1 :  {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → 
                  ( ffmap (A [ g o f ]) ⋍  ( ffmap g * ffmap f ) )
-        distr1 {_} {_} {_} {f} {g} =  let open ≈-Reasoning (A) in
+        distr1 {a} {b} {c} {f} {g} =  let open ≈-Reasoning (A) in
           begin
              KMap (ffmap (A [ g o f ]))
-          ≈⟨ {!!} ⟩
+          ≈⟨⟩
+             TMap η (c) o (g o f)
+          ≈⟨ assoc ⟩
+             (TMap η (c) o g) o f
+          ≈⟨ car (sym (nat η)) ⟩
+             (FMap T g  o TMap η (b)) o f
+          ≈⟨ sym idL ⟩
+             id1 A (FObj T c)  o ((FMap T g  o TMap η (b)) o f)
+          ≈⟨ sym (car (IsMonad.unity2 (isMonad M)))  ⟩
+             (TMap μ c  o FMap T (TMap η c)) o ((FMap T g  o TMap η (b)) o f)
+          ≈⟨ sym assoc  ⟩
+             TMap μ c  o  ( FMap T (TMap η c) o ((FMap T g  o TMap η (b)) o f) )
+          ≈⟨ cdr (cdr (sym  assoc))  ⟩
+             TMap μ c  o  ( FMap T (TMap η c) o (FMap T g  o (TMap η (b) o f)))
+          ≈⟨ cdr assoc  ⟩
+             TMap μ c  o ( ( FMap T (TMap η c) o FMap T g ) o (TMap η (b) o f) )
+          ≈⟨ sym (cdr ( car ( distr T ))) ⟩
+             TMap μ c  o ( ( FMap T (TMap η c o g))  o (TMap η (b) o f))
+          ≈⟨ assoc ⟩
+             (TMap μ c  o  ( FMap T (TMap η c o g)))  o (TMap η (b) o f)
+          ≈⟨ assoc ⟩
+             ((TMap μ c  o  (FMap T  (TMap η c o g)))  o  TMap η b) o f
+          ≈⟨ sym assoc ⟩
+             (TMap μ c  o  (FMap T  (TMap η c o g)))  o  (TMap η b o f) 
+          ≈⟨ sym assoc ⟩
+             TMap μ c  o ( (FMap T  (TMap η c o g))  o  (TMap η b o f) )
+          ≈⟨⟩
+             join K (TMap η c o g)  (TMap η b o f) 
+          ≈⟨⟩
              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 }
+
+Lemma11 : {a : Obj A } -> A [ TMap μ a ≈ FMap U_T ( TMap nat-ε ( FObj F_T a ) ) ]
+Lemma11 = ?
+
+--Lemma12 : T = F_T  ○ U_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 = ?
+
 
 
 
 
-