--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/universal-mapping.agda	Mon Jul 22 14:30:27 2013 +0900
@@ -0,0 +1,29 @@
+module universal-mapping where
+
+open import Category -- https://github.com/konn/category-agda
+open import Level
+open import Category.HomReasoning
+
+open Functor
+record IsUniversalMapping  {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) ) )
+                 ( _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) ->  Hom B (F a ) b )
+                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
+   field
+       universalMapping :   {a' : Obj A} { b' : Obj B } -> ( f : Hom A a' (FObj U b') ) -> 
+                     A [ A [ FMap U ( f * ) o η a' ]  ≈ f ]
+
+
+record UniversalMapping  {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) ) )
+                 ( _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) ->  Hom B (F a ) b )
+                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
+    field
+       isUniversalMapping : IsUniversalMapping A B U F η _*
+
+
+