environ
vocabularies HIDDEN, CAT_1, FUNCT_1, ZFMISC_1, RELAT_1, MCART_1, STRUCT_0, ALGSTR_0, GRAPH_1, PZFMISC1, NATTRA_1, XBOOLE_0, WELLORD1, TARSKI, PARTFUN1, VALUED_1, REWRITE1, ISOCAT_1, MONOID_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_3, STRUCT_0, GRAPH_1, CAT_1, CAT_2, CAT_3, NATTRA_1;
definitions TARSKI, CAT_1, FUNCT_1, NATTRA_1, XBOOLE_0, FUNCT_2;
theorems FUNCT_2, CAT_1, ZFMISC_1, FUNCT_1, FUNCT_3, NATTRA_1, RELAT_1, TARSKI, CAT_3, XTUPLE_0;
schemes FUNCT_2;
registrations RELSET_1, FUNCT_2, STRUCT_0, CAT_1, FUNCT_3;
constructors HIDDEN, NATTRA_1, FUNCOP_1, RELSET_1, CAT_3, FUNCT_4;
requirements HIDDEN, SUBSET, BOOLE;
equalities CAT_1, XBOOLE_0, CAT_2, BINOP_1;
expansions CAT_1, FUNCT_1, NATTRA_1;
theorem
for
A,
B,
C,
D being
Category for
F1,
F2 being
Functor of
A,
B for
G1,
G2 being
Functor of
B,
C for
H1,
H2 being
Functor of
C,
D for
s being
natural_transformation of
F1,
F2 for
t being
natural_transformation of
G1,
G2 for
u being
natural_transformation of
H1,
H2 st
F1 is_naturally_transformable_to F2 &
G1 is_naturally_transformable_to G2 &
H1 is_naturally_transformable_to H2 holds
u (#) (t (#) s) = (u (#) t) (#) s
theorem
for
A,
B,
C being
Category for
F1,
F2,
F3 being
Functor of
A,
B for
G1,
G2,
G3 being
Functor of
B,
C for
s being
natural_transformation of
F1,
F2 for
s9 being
natural_transformation of
F2,
F3 for
t being
natural_transformation of
G1,
G2 for
t9 being
natural_transformation of
G2,
G3 st
F1 is_naturally_transformable_to F2 &
F2 is_naturally_transformable_to F3 &
G1 is_naturally_transformable_to G2 &
G2 is_naturally_transformable_to G3 holds
(t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s)