-Class IsomorphicCategories `(C:Category)`(D:Category){Fobj}{Gobj}(F:Functor C D Fobj)(G:Functor D C Gobj) :=
-{ ic_forward : F >>>> G ~~~~ functor_id C
-; ic_backward : G >>>> F ~~~~ functor_id D
+Class IsomorphicCategories `(C:Category)`(D:Category) :=
+{ ic_f_obj : C -> D
+; ic_g_obj : D -> C
+; ic_f : Functor C D ic_f_obj
+; ic_g : Functor D C ic_g_obj
+; ic_forward : ic_f >>>> ic_g ~~~~ functor_id C
+; ic_backward : ic_g >>>> ic_f ~~~~ functor_id D