# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1374565752 -32400
# Node ID 5d2a33bb12910ded068598dcd9c02325369e5195
# Parent  b4530a8079181bbc1725c25a84ed209c3bc03eb4
cleanup

diff -r b4530a807918 -r 5d2a33bb1291 universal-mapping.agda
--- a/universal-mapping.agda	Tue Jul 23 16:36:31 2013 +0900
+++ b/universal-mapping.agda	Tue Jul 23 16:49:12 2013 +0900
@@ -63,12 +63,12 @@
 open UniversalMapping
 
 Lemma1 : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
-                 ( U : Functor B A )
-                 ( F : Functor A B )
-                 ( η : NTrans A A identityFunctor ( U ○  F ) )
-                 ( ε : NTrans B B  ( F ○  U ) identityFunctor ) ->
+                 { U : Functor B A }
+                 { F : Functor A B }
+                 { η : NTrans A A identityFunctor ( U ○  F ) }
+                 { ε : NTrans B B  ( F ○  U ) identityFunctor } ->
       Adjunction A B U F η ε  -> UniversalMapping A B U (FObj F) (TMap η) 
-Lemma1 A B U F η ε adj = record {
+Lemma1 A B {U} {F} {η} {ε} adj = record {
          _* = solution  ;
          isUniversalMapping = record {
                     universalMapping  = universalMapping;
@@ -136,12 +136,12 @@
 -- F is an functor
 --
 
-FunctorF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
-                 ( U : Functor B A )
-                 ( F : Obj A -> Obj B )
-                 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) ->
+FunctorF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
+                 { U : Functor B A }
+                 { F : Obj A -> Obj B }
+                 { η : (a : Obj A) -> Hom A a ( FObj U (F a) ) } ->
        UniversalMapping A B U F η   -> Functor A B
-FunctorF A B U F η um = record {
+FunctorF A B {U} {F} {η} um = record {
               FObj = F;
               FMap = myFMap ;
               isFunctor = myIsFunctor
@@ -209,16 +209,16 @@
 -- naturality of η
 --
 nat-η : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
-                 ( U : Functor B A )
-                 ( F : Obj A -> Obj B )
-                 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) ->
+                 { U : Functor B A }
+                 { F : Obj A -> Obj B }
+                 { η : (a : Obj A) -> Hom A a ( FObj U (F a) ) } ->
        (um : UniversalMapping A B U F η )  -> 
-           NTrans  A A identityFunctor ( U ○ FunctorF A B U F η um )
-nat-η A B U F η um = record {
+           NTrans  A A identityFunctor ( U ○ FunctorF A B um )
+nat-η A B {U} {F} {η} um = record {
              TMap = η ; isNTrans = myIsNTrans
        } where
     F' : Functor A B
-    F' = FunctorF A B U F η um
+    F' = FunctorF A B um
     naturality :  {a b : Obj A} {f : Hom A a b}
       → A [ A [ (FMap U (FMap F' f))  o  ( η a ) ]  ≈ A [ (η b ) o f ] ]
     naturality {a} {b} {f} =   let open ≈-Reasoning (A) in
@@ -233,16 +233,16 @@
     myIsNTrans = record { naturality = naturality }
 
 nat-ε : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
-                 ( U : Functor B A )
-                 ( F : Obj A -> Obj B )
-                 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) ->
+                 { U : Functor B A }
+                 { F : Obj A -> Obj B }
+                 { η : (a : Obj A) -> Hom A a ( FObj U (F a) ) } ->
        (um : UniversalMapping A B U F η )  -> 
-           NTrans B B ( FunctorF A B U F η um ○ U) identityFunctor 
-nat-ε A B U F η um = record {
+           NTrans B B ( FunctorF A B um ○ U) identityFunctor 
+nat-ε A B {U} {F} {η} um = record {
              TMap = ε ; isNTrans = myIsNTrans
        } where
     F' : Functor A B
-    F' = FunctorF A B U F η um
+    F' = FunctorF A B um
     ε : ( b : Obj B ) -> Hom B ( FObj F' ( FObj U b) ) b
     ε b = (_* um) ( id1 A (FObj U b))
     lemma-nat1 :  (a b : Obj B) (f : Hom B a b ) -> 
@@ -308,7 +308,7 @@
                  ( F' : Obj A -> Obj B )
                  ( η' : (a : Obj A) -> Hom A a ( FObj U (F' a) ) ) ->
        (um : UniversalMapping A B U F' η' )  -> 
-              Adjunction A B U (FunctorF A B U F' η' um) (nat-η A B U F' η' um) (nat-ε A B U F' η' um)
+              Adjunction A B U (FunctorF A B um) (nat-η A B um) (nat-ε A B  um)
 UMAdjunction A B U F' η' um = record {
            isAdjunction = record {
                adjoint1 = adjoint1 ; 
@@ -316,14 +316,14 @@
            } 
        } where
           F : Functor A B
-          F = FunctorF A B U F' η' um
+          F = FunctorF A B um
           η : NTrans A A identityFunctor ( U ○  F ) 
-          η = nat-η A B U F' η' um
+          η = nat-η A B um
           ε : NTrans B B  ( F ○  U ) identityFunctor 
-          ε = nat-ε A B U F' η' um
+          ε = 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 = {!!}
           adjoint2 :   {a : Obj A} ->
                      B [ B [ ( TMap ε ( FObj F a ))  o ( FMap F ( TMap η a )) ]  ≈ id1 B (FObj F a) ]
-          adjoint2 = ?
+          adjoint2 = {!!}