--- a/cat-utility.agda	Sun Nov 26 21:57:41 2017 +0900
+++ b/cat-utility.agda	Mon Nov 27 14:42:49 2017 +0900
@@ -13,6 +13,16 @@
         id1 A a =  (Id {_} {_} {_} {A} a)
         -- We cannot make A implicit
 
+        record Iso  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ)
+                 (x y : Obj C )
+                : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
+           field
+                 ≅→ :  Hom C x y
+                 ≅← :  Hom C y x
+                 iso→  :  C [ C [ ≅← o ≅→  ] ≈  id1 C x ]
+                 iso←  :  C [ C [ ≅→ o ≅←  ] ≈  id1 C y ]
+
+
         record IsUniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                          ( U : Functor B A )
                          ( F : Obj A → Obj B )