environ
vocabularies HIDDEN, CAT_1, ENS_1, FUNCT_1, GRAPH_1, RELAT_1, SUBSET_1, MCART_1, NATTRA_1, STRUCT_0, XBOOLE_0, PZFMISC1, TARSKI, OPPCAT_1, CAT_2, FUNCT_2, YONEDA_1, MONOID_0, PARTFUN1;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, XFAMILY, SUBSET_1, MCART_1, RELAT_1, FUNCT_1, BINOP_1, FUNCT_2, STRUCT_0, GRAPH_1, CAT_1, CAT_2, OPPCAT_1, ENS_1, CAT_3, NATTRA_1;
definitions TARSKI;
theorems FUNCT_1, FUNCT_2, CAT_1, CAT_2, OPPCAT_1, ENS_1, NATTRA_1, ISOCAT_1, RELAT_1, CAT_3, XTUPLE_0;
schemes FUNCT_2;
registrations XBOOLE_0, FUNCT_1, RELSET_1, ENS_1, STRUCT_0, FUNCT_2, CAT_1, XTUPLE_0;
constructors HIDDEN, DOMAIN_1, NATTRA_1, ENS_1, RELSET_1, CAT_3, XTUPLE_0, XFAMILY;
requirements HIDDEN, SUBSET, BOOLE;
equalities TARSKI, BINOP_1, GRAPH_1, CAT_1, XTUPLE_0;
expansions CAT_1;
definition
let A be
Category;
let f be
Morphism of
A;
existence
ex b1 being natural_transformation of <|(cod f),?>,<|(dom f),?> st
for o being Object of A holds b1 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))]
uniqueness
for b1, b2 being natural_transformation of <|(cod f),?>,<|(dom f),?> st ( for o being Object of A holds b1 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ) & ( for o being Object of A holds b2 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ) holds
b1 = b2
end;
definition
let A be
Category;
existence
ex b1 being Contravariant_Functor of A, Functors (A,(EnsHom A)) st
for f being Morphism of A holds b1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>]
uniqueness
for b1, b2 being Contravariant_Functor of A, Functors (A,(EnsHom A)) st ( for f being Morphism of A holds b1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ) & ( for f being Morphism of A holds b2 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ) holds
b1 = b2
end;