--- a/cat-utility.agda	Sun Nov 12 00:53:32 2017 +0900
+++ b/cat-utility.agda	Sun Nov 12 01:29:47 2017 +0900
@@ -27,11 +27,11 @@
 
         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) ) )
                          : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
             infixr 11 _*
             field
+               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
                isUniversalMapping : IsUniversalMapping A B U F η _*
 
@@ -49,11 +49,11 @@
 
         record coUniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                          ( F : Functor A B )
-                         ( U : Obj B → Obj A )
-                         ( ε : (b : Obj B) → Hom B ( FObj F (U b) ) b )
                          : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
             infixr 11 _*'
             field
+               U : Obj B → Obj A 
+               ε : (b : Obj B) → Hom B ( FObj F (U b) ) b 
                _*' :  { b : Obj B}{ a : Obj A} → ( Hom B (FObj F a) b ) →  Hom A a (U b )
                iscoUniversalMapping : coIsUniversalMapping A B F U ε _*'