projects
/
coq-categories.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
758bf2a
)
IsomorphicCategories: make the components fields, not methods
author
Adam Megacz
<adam@megacz.com>
Sun, 27 Mar 2011 19:22:28 +0000
(12:22 -0700)
committer
Adam Megacz
<adam@megacz.com>
Sun, 27 Mar 2011 19:22:28 +0000
(12:22 -0700)
src/Functors_ch1_4.v
patch
|
blob
|
history
diff --git
a/src/Functors_ch1_4.v
b/src/Functors_ch1_4.v
index
176563c
..
0d7f401
100644
(file)
--- 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).
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: *)
}.
(* this causes Coq to die: *)