From 448af7a5ce5ab0520c60dd11d43374e6b5d32552 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 9 Apr 2011 03:55:27 +0000 Subject: [PATCH] add functor_comp_assoc --- src/Functors_ch1_4.v | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/Functors_ch1_4.v b/src/Functors_ch1_4.v index 12e4489..52b0403 100644 --- a/src/Functors_ch1_4.v +++ b/src/Functors_ch1_4.v @@ -59,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 := -- 1.7.10.4