add FullSubcategoryInclusionFunctor

[coq-categories.git] / src / Functors_ch1_4.v

diff --git a/src/Functors_ch1_4.v b/src/Functors_ch1_4.v
index 78f4b59..52b0403 100644 (file)
--- a/src/Functors_ch1_4.v
+++ b/src/Functors_ch1_4.v
@@ -1,6 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
-Require Import General.
+Require Import Notations.
 Require Import Categories_ch1_3.
 
 (******************************************************************************)
@@ -60,7 +59,15 @@ Definition functor_comp
   Defined.
 Notation "f >>>> g" := (@functor_comp _ _ _ _ _ _ _ _ _ _ f _ g)   : category_scope.
 
-
+Lemma functor_comp_assoc `{C':Category}`{D:Category}`{E:Category}`{F:Category}
+  {F1obj}(F1:Functor C' D F1obj)
+  {F2obj}(F2:Functor D E F2obj)
+  {F3obj}(F3:Functor E F F3obj)
+  `(f:a~>b) :
+  ((F1 >>>> F2) >>>> F3) \ f ~~ (F1 >>>> (F2 >>>> F3)) \ f.
+  intros; simpl.
+  reflexivity.
+  Qed.
 
 (* this is like JMEq, but for the particular case of ~~; note it does not require any axioms! *)
 Inductive heq_morphisms `{c:Category}{a b:c}(f:a~>b) : forall {a' b':c}, a'~>b' -> Prop :=
@@ -103,12 +110,14 @@ 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: *)
 (* Definition IsomorphicCategories := Isomorphic (CategoryOfCategories). *)