environ
vocabularies HIDDEN, XBOOLE_0, FUNCT_1, SUBSET_1, MCART_1, ZFMISC_1, TARSKI, PBOOLE, RELAT_1, FUNCT_2, FUNCOP_1, MEMBER_1, STRUCT_0, ALTCAT_1, RELAT_2, MSUALG_6, CAT_1, ALTCAT_2, FUNCT_3, MSUALG_3, ENS_1, WELLORD1, FUNCTOR0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, MCART_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, FUNCT_3, FUNCT_4, STRUCT_0, MSUALG_3, ALTCAT_1, ALTCAT_2;
definitions TARSKI, MSUALG_3, FUNCT_1, FUNCT_2, XBOOLE_0, PBOOLE;
theorems ALTCAT_2, FUNCT_4, FUNCOP_1, ZFMISC_1, ALTCAT_1, FUNCT_2, FUNCT_1, PBOOLE, FUNCT_3, RELAT_1, MCART_1, DOMAIN_1, MSUALG_3, RELSET_1, XBOOLE_0, XBOOLE_1, PARTFUN1, XTUPLE_0;
schemes ALTCAT_2;
registrations SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, PBOOLE, STRUCT_0, ALTCAT_1, ALTCAT_2, PARTFUN1, RELSET_1, FUNCT_3, XTUPLE_0, FUNCT_4;
constructors HIDDEN, FUNCT_3, MSUALG_3, ALTCAT_2, RELSET_1, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities XBOOLE_0, BINOP_1;
expansions MSUALG_3, FUNCT_1, FUNCT_2, XBOOLE_0;
scheme
ValOnPair{
F1()
-> non
empty set ,
F2()
-> Function,
F3()
-> Element of
F1(),
F4()
-> Element of
F1(),
F5(
object ,
object )
-> set ,
P1[
object ,
object ] } :
F2()
. (
F3(),
F4())
= F5(
F3(),
F4())
provided
A1:
F2()
= { [[o,o9],F5(o,o9)] where o, o9 is Element of F1() : P1[o,o9] }
and A2:
P1[
F3(),
F4()]
definition
let I1 be
set ;
let I2 be non
empty set ;
let f be
Function of
I1,
I2;
let A be
ManySortedSet of
[:I1,I1:];
let B be
ManySortedSet of
[:I2,I2:];
let F be
MSUnTrans of
[:f,f:],
A,
B;
~redefine func ~ F -> MSUnTrans of
[:f,f:],
~ A,
~ B;
coherence
~ F is MSUnTrans of [:f,f:], ~ A, ~ B
end;
definition
let C1,
C2 be non
empty AltGraph ;
let F be
Covariant FunctorStr over
C1,
C2;
let o1,
o2 be
Object of
C1;
Morph-Mapredefine func Morph-Map (
F,
o1,
o2)
-> Function of
<^o1,o2^>,
<^(F . o1),(F . o2)^>;
coherence
Morph-Map (F,o1,o2) is Function of <^o1,o2^>,<^(F . o1),(F . o2)^>
end;
definition
let C1,
C2 be non
empty AltGraph ;
let F be
Contravariant FunctorStr over
C1,
C2;
let o1,
o2 be
Object of
C1;
Morph-Mapredefine func Morph-Map (
F,
o1,
o2)
-> Function of
<^o1,o2^>,
<^(F . o2),(F . o1)^>;
coherence
Morph-Map (F,o1,o2) is Function of <^o1,o2^>,<^(F . o2),(F . o1)^>
end;
definition
let C1,
C2 be non
empty AltGraph ;
let o be
Object of
C2;
assume A1:
<^o,o^> <> {}
;
let m be
Morphism of
o,
o;
existence
ex b1 being strict FunctorStr over C1,C2 st
( the ObjectMap of b1 = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b1 = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is Object of C1 : verum } )
uniqueness
for b1, b2 being strict FunctorStr over C1,C2 st the ObjectMap of b1 = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b1 = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is Object of C1 : verum } & the ObjectMap of b2 = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b2 = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is Object of C1 : verum } holds
b1 = b2
;
end;
::
deftheorem Def17 defines
--> FUNCTOR0:def 17 :
for C1, C2 being non empty AltGraph
for o being Object of C2 st <^o,o^> <> {} holds
for m being Morphism of o,o
for b5 being strict FunctorStr over C1,C2 holds
( b5 = C1 --> m iff ( the ObjectMap of b5 = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b5 = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is Object of C1 : verum } ) );
definition
let C1,
C2 be non
empty AltCatStr ;
let F be
FunctorStr over
C1,
C2;
attr F is
comp-preserving means
for
o1,
o2,
o3 being
Object of
C1 st
<^o1,o2^> <> {} &
<^o2,o3^> <> {} holds
for
f being
Morphism of
o1,
o2 for
g being
Morphism of
o2,
o3 ex
f9 being
Morphism of
(F . o1),
(F . o2) ex
g9 being
Morphism of
(F . o2),
(F . o3) st
(
f9 = (Morph-Map (F,o1,o2)) . f &
g9 = (Morph-Map (F,o2,o3)) . g &
(Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 );
end;
::
deftheorem defines
comp-preserving FUNCTOR0:def 21 :
for C1, C2 being non empty AltCatStr
for F being FunctorStr over C1,C2 holds
( F is comp-preserving iff for o1, o2, o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of (F . o1),(F . o2) ex g9 being Morphism of (F . o2),(F . o3) st
( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 ) );
definition
let C1,
C2 be non
empty AltCatStr ;
let F be
FunctorStr over
C1,
C2;
attr F is
comp-reversing means
for
o1,
o2,
o3 being
Object of
C1 st
<^o1,o2^> <> {} &
<^o2,o3^> <> {} holds
for
f being
Morphism of
o1,
o2 for
g being
Morphism of
o2,
o3 ex
f9 being
Morphism of
(F . o2),
(F . o1) ex
g9 being
Morphism of
(F . o3),
(F . o2) st
(
f9 = (Morph-Map (F,o1,o2)) . f &
g9 = (Morph-Map (F,o2,o3)) . g &
(Morph-Map (F,o1,o3)) . (g * f) = f9 * g9 );
end;
::
deftheorem defines
comp-reversing FUNCTOR0:def 22 :
for C1, C2 being non empty AltCatStr
for F being FunctorStr over C1,C2 holds
( F is comp-reversing iff for o1, o2, o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of (F . o2),(F . o1) ex g9 being Morphism of (F . o3),(F . o2) st
( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = f9 * g9 ) );