Mercurial > hg > Members > kono > Proof > category

changeset 81:0404b2ba7db6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Resolution Adjoint proved.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 27 Jul 2013 13:03:02 +0900
parents e945c201364a
children bb95e780c68f
files nat.agda
diffstat 1 files changed, 34 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Sat Jul 27 11:52:10 2013 +0900
+++ b/nat.agda	Sat Jul 27 13:03:02 2013 +0900
@@ -397,8 +397,8 @@
            FMap T f 
      ∎ )
 
--- Lemma11 :  T ≃  (U_T ○ F_T)
---Lemma11 = {!!} -- Lemma11-1
+Lemma11 :  T ≃  (U_T ○ F_T)
+Lemma11 f = Category.Cat.refl (Lemma11-1 f)
 
 nat-η : NTrans A A identityFunctor ( U_T ○ F_T ) 
 nat-η = record { TMap = \x -> TMap η x ; isNTrans = isNTrans1 } where
@@ -487,11 +487,41 @@
        } where
            adjoint1 :   { b : Obj KleisliCategory } →
                      A [ A [ ( FMap U_T ( TMap nat-ε b))  o ( TMap nat-η ( FObj U_T b )) ]  ≈ id1 A (FObj U_T b) ]
-           adjoint1 = {!!}
+           adjoint1 {b} =  let open ≈-Reasoning (A) in
+               begin
+                  ( FMap U_T ( TMap nat-ε b))  o ( TMap nat-η ( FObj U_T b ))
+               ≈⟨⟩
+                  (TMap μ (b)  o FMap T (id1 A (FObj T b )))  o ( TMap η ( FObj T b ))
+               ≈⟨ car ( cdr (IsFunctor.identity (isFunctor T))) ⟩
+                  (TMap μ (b)  o (id1 A (FObj T (FObj T b ))))  o ( TMap η ( FObj T b ))
+               ≈⟨ car idR ⟩
+                  TMap μ (b) o ( TMap η ( FObj T b ))
+               ≈⟨ IsMonad.unity1 (isMonad M) ⟩
+                  id1 A (FObj U_T b)
+               ∎ 
            adjoint2 :   {a : Obj A} →
                      KleisliCategory [ KleisliCategory [ ( TMap nat-ε ( FObj F_T a ))  o ( FMap F_T ( TMap nat-η a )) ]  
                             ≈ id1 KleisliCategory (FObj F_T a) ]
-           adjoint2 = {!!}
+           adjoint2 {a} =  let open ≈-Reasoning (A) in
+               begin
+                  KMap (( TMap nat-ε ( FObj F_T a )) * ( FMap F_T ( TMap nat-η a )) )
+               ≈⟨⟩
+                  TMap μ a o (FMap T (id1 A (FObj T a) ) o ((TMap η (FObj T a)) o (TMap η a)))
+               ≈⟨ cdr ( car ( IsFunctor.identity (isFunctor T))) ⟩
+                  TMap μ a o ((id1 A (FObj T (FObj T a) )) o ((TMap η (FObj T a)) o (TMap η a)))
+               ≈⟨ cdr ( idL ) ⟩
+                  TMap μ a o ((TMap η (FObj T a)) o (TMap η a))
+               ≈⟨ assoc  ⟩
+                  (TMap μ a o (TMap η (FObj T a))) o (TMap η a)
+               ≈⟨ car (IsMonad.unity1 (isMonad M)) ⟩
+                  id1 A (FObj T a) o (TMap η a)
+               ≈⟨ idL ⟩
+                  TMap η a
+               ≈⟨⟩
+                  TMap η (FObj F_T a)
+               ≈⟨⟩
+                  KMap (id1 KleisliCategory (FObj F_T a))
+              ∎