X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FFunctors_ch1_4.v;h=176563c2b1a55c111893fbaaecd1d8afff25278d;hp=78f4b59bc65cef57fc3f4bc85462bf4cb6a30342;hb=107e8eb4dc6e893c3dd93535c5343eba204659a8;hpb=06467b1762fe54767eb1d64e7b7f1798eea8cc27

diff --git a/src/Functors_ch1_4.v b/src/Functors_ch1_4.v
index 78f4b59..176563c 100644
--- a/src/Functors_ch1_4.v
+++ b/src/Functors_ch1_4.v
@@ -103,12 +103,10 @@ Definition EqualFunctors `{C1:Category}`{C2:Category}{F1obj}(F1:Functor C1 C2 F1
   forall a b (f f':a~~{C1}~~>b), f~~f' -> heq_morphisms (F1 \ f) (F2 \ f').
 Notation "f ~~~~ g" := (EqualFunctors f g) (at level 45).
 
-(*
 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
 }.
-*)
 
 (* this causes Coq to die: *)
 (* Definition IsomorphicCategories := Isomorphic (CategoryOfCategories). *)