--- a/universal-mapping.agda	Mon Jul 22 14:30:27 2013 +0900
+++ b/universal-mapping.agda	Mon Jul 22 14:45:58 2013 +0900
@@ -25,5 +25,30 @@
     field
        isUniversalMapping : IsUniversalMapping A B U F η _*
 
+open NTrans
+open import Category.Cat
+
+record IsAdjunction  {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 )
+                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
+   field
+       adjoint1 :   {a' : Obj A} { b' : Obj B } -> ( f : Hom A a' (FObj U b') ) -> 
+                     A [ A [ ( FMap U ( TMap ε b' ))  o ( TMap η ( FObj U b' )) ]  ≈ Id {_} {_} {_} {A} (FObj U b') ]
+       adjoint2 :   {a' : Obj A} { b' : Obj B } -> ( f : Hom A a' (FObj U b') ) -> 
+                     B [ B [ ( TMap ε ( FObj F a' ))  o ( FMap F ( TMap η a' )) ]  ≈ Id {_} {_} {_} {B} (FObj F a') ]
 
 
+record Adjunction {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 )
+                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
+    field
+       isAdjection : IsAdjunction A B U F η ε
+
+
+