--- a/universal-mapping.agda	Tue Jul 23 16:49:12 2013 +0900
+++ b/universal-mapping.agda	Tue Jul 23 17:34:46 2013 +0900
@@ -323,7 +323,55 @@
           ε = nat-ε A B um
           adjoint1 :   { b : Obj B } ->
                      A [ A [ ( FMap U ( TMap ε b ))  o ( TMap η ( FObj U b )) ]  ≈ id1 A (FObj U b) ]
-          adjoint1 = {!!}
+          adjoint1 {b} = let open ≈-Reasoning (A) in
+             begin
+               FMap U ( TMap ε b )  o  TMap η ( FObj U b )
+             ≈⟨⟩
+               FMap U ((_* um) ( id1 A (FObj U b)))  o  η' ( FObj U b )
+             ≈⟨ IsUniversalMapping.universalMapping ( isUniversalMapping um )  ⟩
+               id (FObj U b) 
+             ∎
+          lemma-adj1 : (a : Obj A) -> 
+             A [ A [ FMap U ((B [((_* um) ( id1 A (FObj U ( FObj F a )))) o (_* um) (A [  η' (FObj U ( FObj F a )) o ( η' a ) ]) ])) o η' a ] 
+               ≈ (η' a) ]
+          lemma-adj1 a =  let open ≈-Reasoning (A) in
+             begin
+               FMap U ((B [((_* um) ( id1 A (FObj U ( FObj F a )))) o (_* um) (A [  η' (FObj U ( FObj F a )) o ( η' a ) ]) ])) o η' a 
+             ≈⟨ car ( IsFunctor.distr ( isFunctor U))  ⟩
+               (FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o FMap U ((_* um) (A [  η' (FObj U ( FObj F a )) o ( η' a ) ]))) o η' a 
+             ≈⟨ sym assoc ⟩
+               FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o ( FMap U ((_* um) (A [  η' (FObj U ( FObj F a )) o ( η' a ) ])) o η' a )
+             ≈⟨ cdr (IsUniversalMapping.universalMapping ( isUniversalMapping um)) ⟩
+               FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o ( η' (FObj U ( FObj F a )) o ( η' a ) )
+             ≈⟨ assoc ⟩
+               (FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o ( η' (FObj U ( FObj F a )))) o ( η' a )
+             ≈⟨ car (IsUniversalMapping.universalMapping ( isUniversalMapping um)) ⟩
+                id (FObj U ( FObj F a)) o ( η' a )
+             ≈⟨ idL ⟩
+               η' a
+             ∎
+          lemma-adj2 : (a : Obj A) -> A [ A [ FMap U (id1 B (FObj F a)) o η' a ] ≈  η' a ]
+          lemma-adj2 a = let open ≈-Reasoning (A) in
+             begin
+               FMap U (id1 B (FObj F a)) o η' a 
+             ≈⟨  car ( IsFunctor.identity ( isFunctor U))  ⟩
+               id (FObj U (FObj F a)) o η' a 
+             ≈⟨ idL ⟩
+               η' a 
+             ∎
           adjoint2 :   {a : Obj A} ->
                      B [ B [ ( TMap ε ( FObj F a ))  o ( FMap F ( TMap η a )) ]  ≈ id1 B (FObj F a) ]
-          adjoint2 = {!!}
+          adjoint2 {a} = let open ≈-Reasoning (B) in
+             begin
+                TMap ε ( FObj F a )  o  FMap F ( TMap η a )
+             ≈⟨⟩
+                ((_* um) ( id1 A (FObj U ( FObj F a ))))  o  (_* um)  (A [  η' (FObj U ( FObj F a ))   o ( η' a ) ])
+             ≈⟨ sym ( ( IsUniversalMapping.uniquness ( isUniversalMapping um )  (lemma-adj1 a))) ⟩
+                (_* um)( η' a )
+             ≈⟨  IsUniversalMapping.uniquness ( isUniversalMapping um )  (lemma-adj2 a) ⟩
+                id1 B (FObj F a)
+             ∎
+
+
+--  done!
+