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){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
}.