# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1374675381 -32400
# Node ID 45118051b829d1e9f83b41ead2aa2a2fb15780e9
# Parent  a6e31588e2a6c9e3ab46b30051521c7b9f982802
unity1

diff -r a6e31588e2a6 -r 45118051b829 nat.agda
--- a/nat.agda	Wed Jul 24 22:45:57 2013 +0900
+++ b/nat.agda	Wed Jul 24 23:16:21 2013 +0900
@@ -261,7 +261,7 @@
 lemma11 :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ'}
                  ( U : Functor B A ) ( F : Functor A B ) -> NTrans A A ( U ○  ((F  ○  U) ○  F )) ( U ○  (identityFunctor ○ F) ) 
                          -> NTrans A A  (( U ○  F ) ○ ( U ○  F )) ( U ○  F )
-lemma11 U F n = record { isNTrans = record { naturality = IsNTrans.naturality ( isNTrans n ) }}
+lemma11 U F n = record { TMap = \a -> TMap n a; isNTrans = record { naturality = IsNTrans.naturality ( isNTrans n ) }}
 
 UεF :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                  ( U : Functor B A )
@@ -279,8 +279,29 @@
       Adjunction A B U F η ε  → Monad A (U ○  F) η (UεF A B U F ε)
 Adj2Monad A B {U} {F} {η} {ε} adj = record {
          isMonad = record {
-                    assoc = {!!};
-                    unity1 = {!!};
-                    unity2 = {!!}
+                    assoc = assoc1;
+                    unity1 = unity1;
+                    unity2 = unity2
               }
-      } 
+      }  where
+           T : Functor A A
+           T = U  ○ F
+           μ : NTrans A A ( T ○ T ) T
+           μ = UεF A B U F ε
+           assoc1 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
+           assoc1 = {!!}
+           unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
+           unity1 = {!!}
+           unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
+           unity2 {a} = let open ≈-Reasoning (A) in
+             begin
+                TMap μ a o (FMap T (TMap η a ))
+             ≈⟨⟩
+                (FMap U (TMap ε ( FObj F a ))) o (FMap U ( FMap F (TMap η a )))
+             ≈⟨ sym (IsFunctor.distr ( isFunctor U )) ⟩
+                FMap U ( B [  (TMap ε ( FObj F a )) o ( FMap F (TMap η a )) ])
+             ≈⟨ (IsFunctor.≈-cong (isFunctor U)) (IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩
+                FMap U ( id1 B (FObj F a) )
+             ≈⟨ IsFunctor.identity ( isFunctor U ) ⟩
+                id (FObj T a)
+             ∎