# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1374511556 -32400
# Node ID 659b8a21caf7e4f98efe377a6e4017ceb50d2d28
# Parent  a626fdd909c318bc8ac768d85e1c0279d5852aba
uniq-univeralMapping from Adjunction

diff -r a626fdd909c3 -r 659b8a21caf7 universal-mapping.agda
--- a/universal-mapping.agda	Tue Jul 23 01:27:43 2013 +0900
+++ b/universal-mapping.agda	Tue Jul 23 01:45:56 2013 +0900
@@ -95,7 +95,6 @@
               ≈⟨  idL  ⟩
                   f
               ∎
-         open import Relation.Binary.Core
          lemma1 : (a : Obj A) ( b : Obj B ) ( f : Hom A a (FObj U b) ) -> ( g :  Hom B (FObj F a) b) ->
                 A [ A [ FMap U g o  TMap η a ]  ≈ f ] ->
                 B [  (FMap F (A [ FMap U g o TMap η a ] )) ≈ FMap F f ] 
@@ -107,14 +106,22 @@
                   solution f 
               ≈⟨⟩
                   TMap ε b o FMap F f
-              ≈⟨  cdr (sym ( lemma1 a b f g k )) ⟩ 
+              ≈⟨ cdr (sym ( lemma1 a b f g k )) ⟩ 
                   TMap ε b o FMap F ( A [ FMap U g o  TMap η a ] )
-              ≈⟨  {!!}  ⟩ 
+              ≈⟨ cdr (IsFunctor.distr ( isFunctor F ))  ⟩ 
+                  TMap ε b o ( FMap F ( FMap U g)  o FMap F ( TMap η a ) )
+              ≈⟨ assoc  ⟩ 
+                  ( TMap ε b o  FMap F ( FMap U g) ) o FMap F ( TMap η a ) 
+              ≈⟨ sym ( car ( nat B ε ))  ⟩ 
+                  ( g o TMap ε ( FObj F a) )  o FMap F ( TMap η a ) 
+              ≈⟨ sym assoc ⟩ 
+                  g o ( TMap ε ( FObj F a)   o FMap F ( TMap η a ) )
+              ≈⟨ cdr ( IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩ 
+                  g o id (FObj F a)
+              ≈⟨ idR ⟩ 
                   g
               ∎
 
-
-
 --
 --
 --  Universal mapping yields Adjunction