projects
/
coq-categories.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
469c709
)
add functor_comp_assoc
author
Adam Megacz
<megacz@cs.berkeley.edu>
Sat, 9 Apr 2011 03:55:27 +0000
(
03:55
+0000)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Sat, 9 Apr 2011 03:55:27 +0000
(
03:55
+0000)
src/Functors_ch1_4.v
patch
|
blob
|
history
diff --git
a/src/Functors_ch1_4.v
b/src/Functors_ch1_4.v
index
12e4489
..
52b0403
100644
(file)
--- 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.
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 :=
(* 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 :=