From: Adam Megacz <adam@megacz.com>
Date: Sun, 27 Mar 2011 19:22:28 +0000 (-0700)
Subject: IsomorphicCategories: make the components fields, not methods
X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=commitdiff_plain;h=1ab46a0e579ec1964ae0ab3cadb64f6a77db8d30

IsomorphicCategories: make the components fields, not methods
---

diff --git a/src/Functors_ch1_4.v b/src/Functors_ch1_4.v
index 176563c..0d7f401 100644
--- a/src/Functors_ch1_4.v
+++ b/src/Functors_ch1_4.v
@@ -103,9 +103,13 @@ 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
+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
 }.
 
 (* this causes Coq to die: *)