From 1ab46a0e579ec1964ae0ab3cadb64f6a77db8d30 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sun, 27 Mar 2011 12:22:28 -0700 Subject: [PATCH] IsomorphicCategories: make the components fields, not methods --- src/Functors_ch1_4.v | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) 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: *) -- 1.7.10.4