:: Functors for Alternative Categories
:: by Andrzej Trybulec
::
:: Copyright (c) 1996-2021 Association of Mizar Users

scheme :: FUNCTOR0:sch 1
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()]
proof end;

theorem Th1: :: FUNCTOR0:1
for A being set holds {} is Function of A,{} by FUNCT_2:130;

theorem Th2: :: FUNCTOR0:2
for I being set
for M being ManySortedSet of I holds M * (id I) = M
proof end;

registration
let f be empty Function;
cluster ~ f -> empty ;
coherence
~ f is empty
;
let g be Function;
cluster [:f,g:] -> empty ;
coherence
[:f,g:] is empty
proof end;
cluster [:g,f:] -> empty ;
coherence
[:g,f:] is empty
proof end;
end;

theorem Th3: :: FUNCTOR0:3
for A being set
for f being Function holds f .: (id A) = (~ f) .: (id A)
proof end;

theorem Th4: :: FUNCTOR0:4
for X, Y being set
for f being Function of X,Y holds
( f is onto iff [:f,f:] is onto )
proof end;

registration
let f be Function-yielding Function;
coherence ;
end;

theorem Th5: :: FUNCTOR0:5
for A, B being set
for a being object holds ~ ([:A,B:] --> a) = [:B,A:] --> a
proof end;

theorem Th6: :: FUNCTOR0:6
for f, g being Function st f is one-to-one & g is one-to-one holds
[:f,g:] " = [:(f "),(g "):]
proof end;

theorem Th7: :: FUNCTOR0:7
for f being Function st [:f,f:] is one-to-one holds
f is one-to-one
proof end;

theorem Th8: :: FUNCTOR0:8
for f being Function st f is one-to-one holds
~ f is one-to-one
proof end;

theorem Th9: :: FUNCTOR0:9
for f, g being Function st ~ [:f,g:] is one-to-one holds
[:g,f:] is one-to-one
proof end;

theorem Th10: :: FUNCTOR0:10
for f, g being Function st f is one-to-one & g is one-to-one holds
(~ [:f,g:]) " = ~ ([:g,f:] ")
proof end;

theorem Th11: :: FUNCTOR0:11
for A, B being set
for f being Function of A,B st f is onto holds
id B c= [:f,f:] .: (id A)
proof end;

theorem Th12: :: FUNCTOR0:12
for F, G being Function-yielding Function
for f being Function holds (G ** F) * f = (G * f) ** (F * f)
proof end;

theorem Th13: :: FUNCTOR0:13
for A, B, C being set
for f being Function of [:A,B:],C st ~ f is onto holds
f is onto
proof end;

theorem Th14: :: FUNCTOR0:14
for A being set
for B being non empty set
for f being Function of A,B holds [:f,f:] .: (id A) c= id B
proof end;

definition
let A, B be set ;
mode bifunction of A,B is Function of [:A,A:],[:B,B:];
end;

definition
let A, B be set ;
let f be bifunction of A,B;
attr f is Covariant means :Def1: :: FUNCTOR0:def 1
ex g being Function of A,B st f = [:g,g:];
attr f is Contravariant means :Def2: :: FUNCTOR0:def 2
ex g being Function of A,B st f = ~ [:g,g:];
end;

:: deftheorem Def1 defines Covariant FUNCTOR0:def 1 :
for A, B being set
for f being bifunction of A,B holds
( f is Covariant iff ex g being Function of A,B st f = [:g,g:] );

:: deftheorem Def2 defines Contravariant FUNCTOR0:def 2 :
for A, B being set
for f being bifunction of A,B holds
( f is Contravariant iff ex g being Function of A,B st f = ~ [:g,g:] );

theorem Th15: :: FUNCTOR0:15
for A being set
for B being non empty set
for b being Element of B
for f being bifunction of A,B st f = [:A,A:] --> [b,b] holds
( f is Covariant & f is Contravariant )
proof end;

registration
let A, B be set ;
existence
ex b1 being bifunction of A,B st
( b1 is Covariant & b1 is Contravariant )
proof end;
end;

theorem :: FUNCTOR0:16
for A, B being non empty set
for f being Covariant Contravariant bifunction of A,B ex b being Element of B st f = [:A,A:] --> [b,b]
proof end;

definition
let I1, I2 be set ;
let f be Function of I1,I2;
let A be ManySortedSet of I1;
let B be ManySortedSet of I2;
mode MSUnTrans of f,A,B -> ManySortedSet of I1 means :Def3: :: FUNCTOR0:def 3
ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st
( f = f9 & B = B9 & it is ManySortedFunction of A,B9 * f9 ) if I2 <> {}
otherwise it = EmptyMS I1;
existence
( ( I2 <> {} implies ex b1 being ManySortedSet of I1 ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st
( f = f9 & B = B9 & b1 is ManySortedFunction of A,B9 * f9 ) ) & ( not I2 <> {} implies ex b1 being ManySortedSet of I1 st b1 = EmptyMS I1 ) )
proof end;
consistency
for b1 being ManySortedSet of I1 holds verum
;
end;

:: deftheorem Def3 defines MSUnTrans FUNCTOR0:def 3 :
for I1, I2 being set
for f being Function of I1,I2
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for b6 being ManySortedSet of I1 holds
( ( I2 <> {} implies ( b6 is MSUnTrans of f,A,B iff ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st
( f = f9 & B = B9 & b6 is ManySortedFunction of A,B9 * f9 ) ) ) & ( not I2 <> {} implies ( b6 is MSUnTrans of f,A,B iff b6 = EmptyMS I1 ) ) );

definition
let I1 be set ;
let I2 be non empty set ;
let f be Function of I1,I2;
let A be ManySortedSet of I1;
let B be ManySortedSet of I2;
redefine mode MSUnTrans of f,A,B means :Def4: :: FUNCTOR0:def 4
it is ManySortedFunction of A,B * f;
compatibility
for b1 being ManySortedSet of I1 holds
( b1 is MSUnTrans of f,A,B iff b1 is ManySortedFunction of A,B * f )
proof end;
end;

:: deftheorem Def4 defines MSUnTrans FUNCTOR0:def 4 :
for I1 being set
for I2 being non empty set
for f being Function of I1,I2
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for b6 being ManySortedSet of I1 holds
( b6 is MSUnTrans of f,A,B iff b6 is ManySortedFunction of A,B * f );

registration
let I1, I2 be set ;
let f be Function of I1,I2;
let A be ManySortedSet of I1;
let B be ManySortedSet of I2;
cluster -> Function-yielding for MSUnTrans of f,A,B;
coherence
for b1 being MSUnTrans of f,A,B holds b1 is Function-yielding
proof end;
end;

theorem Th17: :: FUNCTOR0:17
for I1 being set
for I2, I3 being non empty set
for f being Function of I1,I2
for g being Function of I2,I3
for B being ManySortedSet of I2
for C being ManySortedSet of I3
for G being MSUnTrans of g,B,C holds G * f is MSUnTrans of g * f,B * f,C
proof end;

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;
:: original: ~
redefine func ~ F -> MSUnTrans of [:f,f:], ~ A, ~ B;
coherence
~ F is MSUnTrans of [:f,f:], ~ A, ~ B
proof end;
end;

theorem Th18: :: FUNCTOR0:18
for I1, I2 being non empty set
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for o being Element of I2 st B . o <> {} holds
for m being Element of B . o
for f being Function of I1,I2 st f = I1 --> o holds
{ [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B
proof end;

theorem Th19: :: FUNCTOR0:19
for I1 being set
for I2, I3 being non empty set
for f being Function of I1,I2
for g being Function of I2,I3
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for C being ManySortedSet of I3
for F being MSUnTrans of f,A,B
for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) holds
G ** F is MSUnTrans of g * f,A,C
proof end;

definition
let C1, C2 be 1-sorted ;
attr c3 is strict ;
struct BimapStr over C1,C2 -> ;
aggr BimapStr(# ObjectMap #) -> BimapStr over C1,C2;
sel ObjectMap c3 -> bifunction of the carrier of C1, the carrier of C2;
end;

definition
let C1, C2 be non empty AltGraph ;
let F be BimapStr over C1,C2;
let o be Object of C1;
func F . o -> Object of C2 equals :: FUNCTOR0:def 5
( the ObjectMap of F . (o,o)) 1 ;
coherence
( the ObjectMap of F . (o,o)) 1 is Object of C2
by MCART_1:10;
end;

:: deftheorem defines . FUNCTOR0:def 5 :
for C1, C2 being non empty AltGraph
for F being BimapStr over C1,C2
for o being Object of C1 holds F . o = ( the ObjectMap of F . (o,o)) `1 ;

definition
let A, B be 1-sorted ;
let F be BimapStr over A,B;
attr F is one-to-one means :: FUNCTOR0:def 6
the ObjectMap of F is one-to-one ;
attr F is onto means :: FUNCTOR0:def 7
the ObjectMap of F is onto ;
attr F is reflexive means :: FUNCTOR0:def 8
the ObjectMap of F .: (id the carrier of A) c= id the carrier of B;
attr F is coreflexive means :: FUNCTOR0:def 9
id the carrier of B c= the ObjectMap of F .: (id the carrier of A);
end;

:: deftheorem defines one-to-one FUNCTOR0:def 6 :
for A, B being 1-sorted
for F being BimapStr over A,B holds
( F is one-to-one iff the ObjectMap of F is one-to-one );

:: deftheorem defines onto FUNCTOR0:def 7 :
for A, B being 1-sorted
for F being BimapStr over A,B holds
( F is onto iff the ObjectMap of F is onto );

:: deftheorem defines reflexive FUNCTOR0:def 8 :
for A, B being 1-sorted
for F being BimapStr over A,B holds
( F is reflexive iff the ObjectMap of F .: (id the carrier of A) c= id the carrier of B );

:: deftheorem defines coreflexive FUNCTOR0:def 9 :
for A, B being 1-sorted
for F being BimapStr over A,B holds
( F is coreflexive iff id the carrier of B c= the ObjectMap of F .: (id the carrier of A) );

definition
let A, B be non empty AltGraph ;
let F be BimapStr over A,B;
redefine attr F is reflexive means :Def10: :: FUNCTOR0:def 10
for o being Object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)];
compatibility
( F is reflexive iff for o being Object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)] )
proof end;
end;

:: deftheorem Def10 defines reflexive FUNCTOR0:def 10 :
for A, B being non empty AltGraph
for F being BimapStr over A,B holds
( F is reflexive iff for o being Object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)] );

theorem Th20: :: FUNCTOR0:20
for A, B being non empty reflexive AltGraph
for F being BimapStr over A,B st F is coreflexive holds
for o being Object of B ex o9 being Object of A st F . o9 = o
proof end;

definition
let C1, C2 be non empty AltGraph ;
let F be BimapStr over C1,C2;
attr F is feasible means :Def11: :: FUNCTOR0:def 11
for o1, o2 being Object of C1 st <^o1,o2^> <> {} holds
the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {} ;
end;

:: deftheorem Def11 defines feasible FUNCTOR0:def 11 :
for C1, C2 being non empty AltGraph
for F being BimapStr over C1,C2 holds
( F is feasible iff for o1, o2 being Object of C1 st <^o1,o2^> <> {} holds
the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {} );

definition
let C1, C2 be AltGraph ;
attr c3 is strict ;
struct FunctorStr over C1,C2 -> BimapStr over C1,C2;
aggr FunctorStr(# ObjectMap, MorphMap #) -> FunctorStr over C1,C2;
sel MorphMap c3 -> MSUnTrans of the ObjectMap of c3, the Arrows of C1, the Arrows of C2;
end;

definition
let C1, C2 be 1-sorted ;
let IT be BimapStr over C1,C2;
attr IT is Covariant means :Def12: :: FUNCTOR0:def 12
the ObjectMap of IT is Covariant ;
attr IT is Contravariant means :Def13: :: FUNCTOR0:def 13
the ObjectMap of IT is Contravariant ;
end;

:: deftheorem Def12 defines Covariant FUNCTOR0:def 12 :
for C1, C2 being 1-sorted
for IT being BimapStr over C1,C2 holds
( IT is Covariant iff the ObjectMap of IT is Covariant );

:: deftheorem Def13 defines Contravariant FUNCTOR0:def 13 :
for C1, C2 being 1-sorted
for IT being BimapStr over C1,C2 holds
( IT is Contravariant iff the ObjectMap of IT is Contravariant );

registration
let C1, C2 be AltGraph ;
cluster Covariant for FunctorStr over C1,C2;
existence
ex b1 being FunctorStr over C1,C2 st b1 is Covariant
proof end;
cluster Contravariant for FunctorStr over C1,C2;
existence
ex b1 being FunctorStr over C1,C2 st b1 is Contravariant
proof end;
end;

definition
let C1, C2 be AltGraph ;
let F be FunctorStr over C1,C2;
let o1, o2 be Object of C1;
func Morph-Map (F,o1,o2) -> set equals :: FUNCTOR0:def 14
the MorphMap of F . (o1,o2);
correctness
coherence
the MorphMap of F . (o1,o2) is set
;
;
end;

:: deftheorem defines Morph-Map FUNCTOR0:def 14 :
for C1, C2 being AltGraph
for F being FunctorStr over C1,C2
for o1, o2 being Object of C1 holds Morph-Map (F,o1,o2) = the MorphMap of F . (o1,o2);

registration
let C1, C2 be AltGraph ;
let F be FunctorStr over C1,C2;
let o1, o2 be Object of C1;
cluster Morph-Map (F,o1,o2) -> Relation-like Function-like ;
coherence
( Morph-Map (F,o1,o2) is Relation-like & Morph-Map (F,o1,o2) is Function-like )
;
end;

definition
let C1, C2 be non empty AltGraph ;
let F be Covariant FunctorStr over C1,C2;
let o1, o2 be Object of C1;
:: original: Morph-Map
redefine 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)^>
proof end;
end;

definition
let C1, C2 be non empty AltGraph ;
let F be Covariant FunctorStr over C1,C2;
let o1, o2 be Object of C1;
assume that
A1: <^o1,o2^> <> {} and
A2: <^(F . o1),(F . o2)^> <> {} ;
let m be Morphism of o1,o2;
func F . m -> Morphism of (F . o1),(F . o2) equals :Def15: :: FUNCTOR0:def 15
(Morph-Map (F,o1,o2)) . m;
coherence
(Morph-Map (F,o1,o2)) . m is Morphism of (F . o1),(F . o2)
proof end;
end;

:: deftheorem Def15 defines . FUNCTOR0:def 15 :
for C1, C2 being non empty AltGraph
for F being Covariant FunctorStr over C1,C2
for o1, o2 being Object of C1 st <^o1,o2^> <> {} & <^(F . o1),(F . o2)^> <> {} holds
for m being Morphism of o1,o2 holds F . m = (Morph-Map (F,o1,o2)) . m;

definition
let C1, C2 be non empty AltGraph ;
let F be Contravariant FunctorStr over C1,C2;
let o1, o2 be Object of C1;
:: original: Morph-Map
redefine 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)^>
proof end;
end;

definition
let C1, C2 be non empty AltGraph ;
let F be Contravariant FunctorStr over C1,C2;
let o1, o2 be Object of C1;
assume that
A1: <^o1,o2^> <> {} and
A2: <^(F . o2),(F . o1)^> <> {} ;
let m be Morphism of o1,o2;
func F . m -> Morphism of (F . o2),(F . o1) equals :Def16: :: FUNCTOR0:def 16
(Morph-Map (F,o1,o2)) . m;
coherence
(Morph-Map (F,o1,o2)) . m is Morphism of (F . o2),(F . o1)
proof end;
end;

:: deftheorem Def16 defines . FUNCTOR0:def 16 :
for C1, C2 being non empty AltGraph
for F being Contravariant FunctorStr over C1,C2
for o1, o2 being Object of C1 st <^o1,o2^> <> {} & <^(F . o2),(F . o1)^> <> {} holds
for m being Morphism of o1,o2 holds F . m = (Morph-Map (F,o1,o2)) . m;

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;
func C1 --> m -> strict FunctorStr over C1,C2 means :Def17: :: FUNCTOR0:def 17
( the ObjectMap of it = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of it = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is Object of C1 : verum } );
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 } )
proof end;
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 } ) );

theorem Th21: :: FUNCTOR0:21
for C1, C2 being non empty AltGraph
for o2 being Object of C2 st <^o2,o2^> <> {} holds
for m being Morphism of o2,o2
for o1 being Object of C1 holds (C1 --> m) . o1 = o2
proof end;

registration
let C1 be non empty AltGraph ;
let C2 be non empty reflexive AltGraph ;
let o be Object of C2;
let m be Morphism of o,o;
coherence
( C1 --> m is Covariant & C1 --> m is Contravariant & C1 --> m is feasible )
proof end;
end;

registration
let C1 be non empty AltGraph ;
let C2 be non empty reflexive AltGraph ;
cluster feasible Covariant Contravariant for FunctorStr over C1,C2;
existence
ex b1 being FunctorStr over C1,C2 st
( b1 is feasible & b1 is Covariant & b1 is Contravariant )
proof end;
end;

theorem Th22: :: FUNCTOR0:22
for C1, C2 being non empty AltGraph
for F being Covariant FunctorStr over C1,C2
for o1, o2 being Object of C1 holds the ObjectMap of F . (o1,o2) = [(F . o1),(F . o2)]
proof end;

definition
let C1, C2 be non empty AltGraph ;
let F be Covariant FunctorStr over C1,C2;
redefine attr F is feasible means :Def18: :: FUNCTOR0:def 18
for o1, o2 being Object of C1 st <^o1,o2^> <> {} holds
<^(F . o1),(F . o2)^> <> {} ;
compatibility
( F is feasible iff for o1, o2 being Object of C1 st <^o1,o2^> <> {} holds
<^(F . o1),(F . o2)^> <> {} )
proof end;
end;

:: deftheorem Def18 defines feasible FUNCTOR0:def 18 :
for C1, C2 being non empty AltGraph
for F being Covariant FunctorStr over C1,C2 holds
( F is feasible iff for o1, o2 being Object of C1 st <^o1,o2^> <> {} holds
<^(F . o1),(F . o2)^> <> {} );

theorem Th23: :: FUNCTOR0:23
for C1, C2 being non empty AltGraph
for F being Contravariant FunctorStr over C1,C2
for o1, o2 being Object of C1 holds the ObjectMap of F . (o1,o2) = [(F . o2),(F . o1)]
proof end;

definition
let C1, C2 be non empty AltGraph ;
let F be Contravariant FunctorStr over C1,C2;
redefine attr F is feasible means :Def19: :: FUNCTOR0:def 19
for o1, o2 being Object of C1 st <^o1,o2^> <> {} holds
<^(F . o2),(F . o1)^> <> {} ;
compatibility
( F is feasible iff for o1, o2 being Object of C1 st <^o1,o2^> <> {} holds
<^(F . o2),(F . o1)^> <> {} )
proof end;
end;

:: deftheorem Def19 defines feasible FUNCTOR0:def 19 :
for C1, C2 being non empty AltGraph
for F being Contravariant FunctorStr over C1,C2 holds
( F is feasible iff for o1, o2 being Object of C1 st <^o1,o2^> <> {} holds
<^(F . o2),(F . o1)^> <> {} );

registration
let C1, C2 be AltGraph ;
let F be FunctorStr over C1,C2;
cluster the MorphMap of F -> Function-yielding ;
coherence
the MorphMap of F is Function-yielding
;
end;

registration
existence
ex b1 being AltCatStr st
( not b1 is empty & b1 is reflexive )
proof end;
end;

:: Wlasnosci funktorow, Semadeni-Wiweger str. 32
definition
let C1, C2 be non empty with_units AltCatStr ;
let F be FunctorStr over C1,C2;
attr F is id-preserving means :Def20: :: FUNCTOR0:def 20
for o being Object of C1 holds (Morph-Map (F,o,o)) . (idm o) = idm (F . o);
end;

:: deftheorem Def20 defines id-preserving FUNCTOR0:def 20 :
for C1, C2 being non empty with_units AltCatStr
for F being FunctorStr over C1,C2 holds
( F is id-preserving iff for o being Object of C1 holds (Morph-Map (F,o,o)) . (idm o) = idm (F . o) );

theorem Th24: :: FUNCTOR0:24
for C1, C2 being non empty AltGraph
for o2 being Object of C2 st <^o2,o2^> <> {} holds
for m being Morphism of o2,o2
for o, o9 being Object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
(Morph-Map ((C1 --> m),o,o9)) . f = m
proof end;

registration
cluster non empty with_units -> non empty reflexive for AltCatStr ;
coherence
for b1 being non empty AltCatStr st b1 is with_units holds
b1 is reflexive
;
end;

registration
let C1, C2 be non empty with_units AltCatStr ;
let o2 be Object of C2;
cluster C1 --> (idm o2) -> strict id-preserving ;
coherence
C1 --> (idm o2) is id-preserving
proof end;
end;

registration
let C1 be non empty AltGraph ;
let C2 be non empty reflexive AltGraph ;
let o2 be Object of C2;
let m be Morphism of o2,o2;
coherence
C1 --> m is reflexive
proof end;
end;

registration
let C1 be non empty AltGraph ;
let C2 be non empty reflexive AltGraph ;
cluster reflexive feasible for FunctorStr over C1,C2;
existence
ex b1 being FunctorStr over C1,C2 st
( b1 is feasible & b1 is reflexive )
proof end;
end;

registration
let C1, C2 be non empty with_units AltCatStr ;
existence
ex b1 being FunctorStr over C1,C2 st
( b1 is id-preserving & b1 is feasible & b1 is reflexive & b1 is strict )
proof end;
end;

definition
let C1, C2 be non empty AltCatStr ;
let F be FunctorStr over C1,C2;
attr F is comp-preserving means :: FUNCTOR0:def 21
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 :: FUNCTOR0:def 22
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 ) );

definition
let C1 be non empty transitive AltCatStr ;
let C2 be non empty reflexive AltCatStr ;
let F be feasible Covariant FunctorStr over C1,C2;
redefine attr F is comp-preserving means :: FUNCTOR0:def 23
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 holds F . (g * f) = (F . g) * (F . f);
compatibility
( 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 holds F . (g * f) = (F . g) * (F . f) )
proof end;
end;

:: deftheorem defines comp-preserving FUNCTOR0:def 23 :
for C1 being non empty transitive AltCatStr
for C2 being non empty reflexive AltCatStr
for F being feasible Covariant 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 holds F . (g * f) = (F . g) * (F . f) );

definition
let C1 be non empty transitive AltCatStr ;
let C2 be non empty reflexive AltCatStr ;
let F be feasible Contravariant FunctorStr over C1,C2;
redefine attr F is comp-reversing means :: FUNCTOR0:def 24
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 holds F . (g * f) = (F . f) * (F . g);
compatibility
( 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 holds F . (g * f) = (F . f) * (F . g) )
proof end;
end;

:: deftheorem defines comp-reversing FUNCTOR0:def 24 :
for C1 being non empty transitive AltCatStr
for C2 being non empty reflexive AltCatStr
for F being feasible Contravariant 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 holds F . (g * f) = (F . f) * (F . g) );

theorem Th25: :: FUNCTOR0:25
for C1 being non empty AltGraph
for C2 being non empty reflexive AltGraph
for o2 being Object of C2
for m being Morphism of o2,o2
for F being feasible Covariant FunctorStr over C1,C2 st F = C1 --> m holds
for o, o9 being Object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
F . f = m
proof end;

theorem Th26: :: FUNCTOR0:26
for C1 being non empty AltGraph
for C2 being non empty reflexive AltGraph
for o2 being Object of C2
for m being Morphism of o2,o2
for o, o9 being Object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
(C1 --> m) . f = m
proof end;

registration
let C1 be non empty transitive AltCatStr ;
let C2 be non empty with_units AltCatStr ;
let o be Object of C2;
coherence
( C1 --> (idm o) is comp-preserving & C1 --> (idm o) is comp-reversing )
proof end;
end;

definition
let C1 be non empty transitive with_units AltCatStr ;
let C2 be non empty with_units AltCatStr ;
mode Functor of C1,C2 -> FunctorStr over C1,C2 means :Def25: :: FUNCTOR0:def 25
( it is feasible & it is id-preserving & ( ( it is Covariant & it is comp-preserving ) or ( it is Contravariant & it is comp-reversing ) ) );
existence
ex b1 being FunctorStr over C1,C2 st
( b1 is feasible & b1 is id-preserving & ( ( b1 is Covariant & b1 is comp-preserving ) or ( b1 is Contravariant & b1 is comp-reversing ) ) )
proof end;
end;

:: deftheorem Def25 defines Functor FUNCTOR0:def 25 :
for C1 being non empty transitive with_units AltCatStr
for C2 being non empty with_units AltCatStr
for b3 being FunctorStr over C1,C2 holds
( b3 is Functor of C1,C2 iff ( b3 is feasible & b3 is id-preserving & ( ( b3 is Covariant & b3 is comp-preserving ) or ( b3 is Contravariant & b3 is comp-reversing ) ) ) );

definition
let C1 be non empty transitive with_units AltCatStr ;
let C2 be non empty with_units AltCatStr ;
let F be Functor of C1,C2;
attr F is covariant means :Def26: :: FUNCTOR0:def 26
( F is Covariant & F is comp-preserving );
attr F is contravariant means :Def27: :: FUNCTOR0:def 27
( F is Contravariant & F is comp-reversing );
end;

:: deftheorem Def26 defines covariant FUNCTOR0:def 26 :
for C1 being non empty transitive with_units AltCatStr
for C2 being non empty with_units AltCatStr
for F being Functor of C1,C2 holds
( F is covariant iff ( F is Covariant & F is comp-preserving ) );

:: deftheorem Def27 defines contravariant FUNCTOR0:def 27 :
for C1 being non empty transitive with_units AltCatStr
for C2 being non empty with_units AltCatStr
for F being Functor of C1,C2 holds
( F is contravariant iff ( F is Contravariant & F is comp-reversing ) );

definition
let A be AltCatStr ;
let B be SubCatStr of A;
func incl B -> strict FunctorStr over B,A means :Def28: :: FUNCTOR0:def 28
( the ObjectMap of it = id [: the carrier of B, the carrier of B:] & the MorphMap of it = id the Arrows of B );
existence
ex b1 being strict FunctorStr over B,A st
( the ObjectMap of b1 = id [: the carrier of B, the carrier of B:] & the MorphMap of b1 = id the Arrows of B )
proof end;
correctness
uniqueness
for b1, b2 being strict FunctorStr over B,A st the ObjectMap of b1 = id [: the carrier of B, the carrier of B:] & the MorphMap of b1 = id the Arrows of B & the ObjectMap of b2 = id [: the carrier of B, the carrier of B:] & the MorphMap of b2 = id the Arrows of B holds
b1 = b2
;
;
end;

:: deftheorem Def28 defines incl FUNCTOR0:def 28 :
for A being AltCatStr
for B being SubCatStr of A
for b3 being strict FunctorStr over B,A holds
( b3 = incl B iff ( the ObjectMap of b3 = id [: the carrier of B, the carrier of B:] & the MorphMap of b3 = id the Arrows of B ) );

definition
let A be AltGraph ;
func id A -> strict FunctorStr over A,A means :Def29: :: FUNCTOR0:def 29
( the ObjectMap of it = id [: the carrier of A, the carrier of A:] & the MorphMap of it = id the Arrows of A );
existence
ex b1 being strict FunctorStr over A,A st
( the ObjectMap of b1 = id [: the carrier of A, the carrier of A:] & the MorphMap of b1 = id the Arrows of A )
proof end;
correctness
uniqueness
for b1, b2 being strict FunctorStr over A,A st the ObjectMap of b1 = id [: the carrier of A, the carrier of A:] & the MorphMap of b1 = id the Arrows of A & the ObjectMap of b2 = id [: the carrier of A, the carrier of A:] & the MorphMap of b2 = id the Arrows of A holds
b1 = b2
;
;
end;

:: deftheorem Def29 defines id FUNCTOR0:def 29 :
for A being AltGraph
for b2 being strict FunctorStr over A,A holds
( b2 = id A iff ( the ObjectMap of b2 = id [: the carrier of A, the carrier of A:] & the MorphMap of b2 = id the Arrows of A ) );

registration
let A be AltCatStr ;
let B be SubCatStr of A;
coherence
proof end;
end;

theorem Th27: :: FUNCTOR0:27
for A being non empty AltCatStr
for B being non empty SubCatStr of A
for o being Object of B holds (incl B) . o = o
proof end;

theorem Th28: :: FUNCTOR0:28
for A being non empty AltCatStr
for B being non empty SubCatStr of A
for o1, o2 being Object of B holds <^o1,o2^> c= <^((incl B) . o1),((incl B) . o2)^>
proof end;

registration
let A be non empty AltCatStr ;
let B be non empty SubCatStr of A;
coherence
incl B is feasible
by ;
end;

definition
let A, B be AltGraph ;
let F be FunctorStr over A,B;
attr F is faithful means :: FUNCTOR0:def 30
the MorphMap of F is "1-1" ;
end;

:: deftheorem defines faithful FUNCTOR0:def 30 :
for A, B being AltGraph
for F being FunctorStr over A,B holds
( F is faithful iff the MorphMap of F is "1-1" );

definition
let A, B be AltGraph ;
let F be FunctorStr over A,B;
attr F is full means :: FUNCTOR0:def 31
ex B9 being ManySortedSet of [: the carrier of A, the carrier of A:] ex f being ManySortedFunction of the Arrows of A,B9 st
( B9 = the Arrows of B * the ObjectMap of F & f = the MorphMap of F & f is "onto" );
end;

:: deftheorem defines full FUNCTOR0:def 31 :
for A, B being AltGraph
for F being FunctorStr over A,B holds
( F is full iff ex B9 being ManySortedSet of [: the carrier of A, the carrier of A:] ex f being ManySortedFunction of the Arrows of A,B9 st
( B9 = the Arrows of B * the ObjectMap of F & f = the MorphMap of F & f is "onto" ) );

definition
let A be AltGraph ;
let B be non empty AltGraph ;
let F be FunctorStr over A,B;
redefine attr F is full means :: FUNCTOR0:def 32
ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & f is "onto" );
compatibility
( F is full iff ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & f is "onto" ) )
;
end;

:: deftheorem defines full FUNCTOR0:def 32 :
for A being AltGraph
for B being non empty AltGraph
for F being FunctorStr over A,B holds
( F is full iff ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & f is "onto" ) );

definition
let A, B be AltGraph ;
let F be FunctorStr over A,B;
attr F is injective means :: FUNCTOR0:def 33
( F is one-to-one & F is faithful );
attr F is surjective means :: FUNCTOR0:def 34
( F is full & F is onto );
end;

:: deftheorem defines injective FUNCTOR0:def 33 :
for A, B being AltGraph
for F being FunctorStr over A,B holds
( F is injective iff ( F is one-to-one & F is faithful ) );

:: deftheorem defines surjective FUNCTOR0:def 34 :
for A, B being AltGraph
for F being FunctorStr over A,B holds
( F is surjective iff ( F is full & F is onto ) );

definition
let A, B be AltGraph ;
let F be FunctorStr over A,B;
attr F is bijective means :: FUNCTOR0:def 35
( F is injective & F is surjective );
end;

:: deftheorem defines bijective FUNCTOR0:def 35 :
for A, B being AltGraph
for F being FunctorStr over A,B holds
( F is bijective iff ( F is injective & F is surjective ) );

registration
let A, B be non empty transitive with_units AltCatStr ;
existence
ex b1 being Functor of A,B st
( b1 is strict & b1 is covariant & b1 is contravariant & b1 is feasible )
proof end;
end;

theorem Th29: :: FUNCTOR0:29
for A being non empty AltGraph
for o being Object of A holds (id A) . o = o
proof end;

theorem Th30: :: FUNCTOR0:30
for A being non empty AltGraph
for o1, o2 being Object of A st <^o1,o2^> <> {} holds
for m being Morphism of o1,o2 holds (Morph-Map ((id A),o1,o2)) . m = m
proof end;

registration
let A be non empty AltGraph ;
coherence
( id A is feasible & id A is Covariant )
proof end;
end;

registration
let A be non empty AltGraph ;
cluster feasible Covariant for FunctorStr over A,A;
existence
ex b1 being FunctorStr over A,A st
( b1 is Covariant & b1 is feasible )
proof end;
end;

theorem Th31: :: FUNCTOR0:31
for A being non empty AltGraph
for o1, o2 being Object of A st <^o1,o2^> <> {} holds
for F being feasible Covariant FunctorStr over A,A st F = id A holds
for m being Morphism of o1,o2 holds F . m = m
proof end;

registration
let A be non empty transitive with_units AltCatStr ;
coherence
( id A is id-preserving & id A is comp-preserving )
proof end;
end;

definition
let A be non empty transitive with_units AltCatStr ;
:: original: id
redefine func id A -> strict covariant Functor of A,A;
coherence
id A is strict covariant Functor of A,A
by ;
end;

registration
let A be AltGraph ;
coherence
id A is bijective
proof end;
end;

definition
let C1 be non empty AltGraph ;
let C2, C3 be non empty reflexive AltGraph ;
let F be feasible FunctorStr over C1,C2;
let G be FunctorStr over C2,C3;
func G * F -> strict FunctorStr over C1,C3 means :Def36: :: FUNCTOR0:def 36
( the ObjectMap of it = the ObjectMap of G * the ObjectMap of F & the MorphMap of it = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F );
existence
ex b1 being strict FunctorStr over C1,C3 st
( the ObjectMap of b1 = the ObjectMap of G * the ObjectMap of F & the MorphMap of b1 = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F )
proof end;
correctness
uniqueness
for b1, b2 being strict FunctorStr over C1,C3 st the ObjectMap of b1 = the ObjectMap of G * the ObjectMap of F & the MorphMap of b1 = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F & the ObjectMap of b2 = the ObjectMap of G * the ObjectMap of F & the MorphMap of b2 = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F holds
b1 = b2
;
;
end;

:: deftheorem Def36 defines * FUNCTOR0:def 36 :
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3
for b6 being strict FunctorStr over C1,C3 holds
( b6 = G * F iff ( the ObjectMap of b6 = the ObjectMap of G * the ObjectMap of F & the MorphMap of b6 = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F ) );

registration
let C1 be non empty AltGraph ;
let C2, C3 be non empty reflexive AltGraph ;
let F be feasible Covariant FunctorStr over C1,C2;
let G be Covariant FunctorStr over C2,C3;
correctness
coherence
G * F is Covariant
;
proof end;
end;

registration
let C1 be non empty AltGraph ;
let C2, C3 be non empty reflexive AltGraph ;
let F be feasible Contravariant FunctorStr over C1,C2;
let G be Covariant FunctorStr over C2,C3;
correctness
coherence
G * F is Contravariant
;
proof end;
end;

registration
let C1 be non empty AltGraph ;
let C2, C3 be non empty reflexive AltGraph ;
let F be feasible Covariant FunctorStr over C1,C2;
let G be Contravariant FunctorStr over C2,C3;
correctness
coherence
G * F is Contravariant
;
proof end;
end;

registration
let C1 be non empty AltGraph ;
let C2, C3 be non empty reflexive AltGraph ;
let F be feasible Contravariant FunctorStr over C1,C2;
let G be Contravariant FunctorStr over C2,C3;
correctness
coherence
G * F is Covariant
;
proof end;
end;

registration
let C1 be non empty AltGraph ;
let C2, C3 be non empty reflexive AltGraph ;
let F be feasible FunctorStr over C1,C2;
let G be feasible FunctorStr over C2,C3;
coherence
G * F is feasible
proof end;
end;

theorem :: FUNCTOR0:32
for C1 being non empty AltGraph
for C2, C3, C4 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being feasible FunctorStr over C2,C3
for H being FunctorStr over C3,C4 holds (H * G) * F = H * (G * F)
proof end;

theorem Th33: :: FUNCTOR0:33
for C1 being non empty AltCatStr
for C2, C3 being non empty reflexive AltCatStr
for F being reflexive feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3
for o being Object of C1 holds (G * F) . o = G . (F . o)
proof end;

theorem Th34: :: FUNCTOR0:34
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being reflexive feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3
for o being Object of C1 holds Morph-Map ((G * F),o,o) = (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o))
proof end;

registration
let C1, C2, C3 be non empty with_units AltCatStr ;
let F be reflexive feasible id-preserving FunctorStr over C1,C2;
let G be id-preserving FunctorStr over C2,C3;
coherence
G * F is id-preserving
proof end;
end;

definition
let A, C be non empty reflexive AltCatStr ;
let B be non empty SubCatStr of A;
let F be FunctorStr over A,C;
func F | B -> FunctorStr over B,C equals :: FUNCTOR0:def 37
F * (incl B);
correctness
coherence
F * (incl B) is FunctorStr over B,C
;
;
end;

:: deftheorem defines | FUNCTOR0:def 37 :
for A, C being non empty reflexive AltCatStr
for B being non empty SubCatStr of A
for F being FunctorStr over A,C holds F | B = F * (incl B);

definition
let A, B be non empty AltGraph ;
let F be FunctorStr over A,B;
assume A1: F is bijective ;
func F " -> strict FunctorStr over B,A means :Def38: :: FUNCTOR0:def 38
( the ObjectMap of it = the ObjectMap of F " & ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & the MorphMap of it = (f "") * ( the ObjectMap of F ") ) );
existence
ex b1 being strict FunctorStr over B,A st
( the ObjectMap of b1 = the ObjectMap of F " & ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & the MorphMap of b1 = (f "") * ( the ObjectMap of F ") ) )
proof end;
uniqueness
for b1, b2 being strict FunctorStr over B,A st the ObjectMap of b1 = the ObjectMap of F " & ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & the MorphMap of b1 = (f "") * ( the ObjectMap of F ") ) & the ObjectMap of b2 = the ObjectMap of F " & ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & the MorphMap of b2 = (f "") * ( the ObjectMap of F ") ) holds
b1 = b2
;
end;

:: deftheorem Def38 defines " FUNCTOR0:def 38 :
for A, B being non empty AltGraph
for F being FunctorStr over A,B st F is bijective holds
for b4 being strict FunctorStr over B,A holds
( b4 = F " iff ( the ObjectMap of b4 = the ObjectMap of F " & ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & the MorphMap of b4 = (f "") * ( the ObjectMap of F ") ) ) );

theorem Th35: :: FUNCTOR0:35
for A, B being non empty transitive with_units AltCatStr
for F being feasible FunctorStr over A,B st F is bijective holds
( F " is bijective & F " is feasible )
proof end;

theorem Th36: :: FUNCTOR0:36
for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive holds
F " is reflexive
proof end;

theorem Th37: :: FUNCTOR0:37
for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible id-preserving FunctorStr over A,B st F is bijective & F is coreflexive holds
F " is id-preserving
proof end;

theorem Th38: :: FUNCTOR0:38
for A, B being non empty transitive with_units AltCatStr
for F being feasible FunctorStr over A,B st F is bijective & F is Covariant holds
F " is Covariant
proof end;

theorem Th39: :: FUNCTOR0:39
for A, B being non empty transitive with_units AltCatStr
for F being feasible FunctorStr over A,B st F is bijective & F is Contravariant holds
F " is Contravariant
proof end;

theorem Th40: :: FUNCTOR0:40
for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive & F is Covariant holds
for o1, o2 being Object of B
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m
proof end;

theorem Th41: :: FUNCTOR0:41
for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive & F is Contravariant holds
for o1, o2 being Object of B
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map (F,((F ") . o2),((F ") . o1))) . ((Morph-Map ((F "),o1,o2)) . m) = m
proof end;

theorem Th42: :: FUNCTOR0:42
for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr over A,B st F is bijective & F is comp-preserving & F is Covariant & F is coreflexive holds
F " is comp-preserving
proof end;

theorem Th43: :: FUNCTOR0:43
for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr over A,B st F is bijective & F is comp-reversing & F is Contravariant & F is coreflexive holds
F " is comp-reversing
proof end;

registration
let C1 be 1-sorted ;
let C2 be non empty 1-sorted ;
cluster Covariant -> reflexive for BimapStr over C1,C2;
coherence
for b1 being BimapStr over C1,C2 st b1 is Covariant holds
b1 is reflexive
proof end;
end;

registration
let C1 be 1-sorted ;
let C2 be non empty 1-sorted ;
cluster Contravariant -> reflexive for BimapStr over C1,C2;
coherence
for b1 being BimapStr over C1,C2 st b1 is Contravariant holds
b1 is reflexive
proof end;
end;

theorem Th44: :: FUNCTOR0:44
for C1, C2 being 1-sorted
for M being BimapStr over C1,C2 st M is Covariant & M is onto holds
M is coreflexive
proof end;

theorem Th45: :: FUNCTOR0:45
for C1, C2 being 1-sorted
for M being BimapStr over C1,C2 st M is Contravariant & M is onto holds
M is coreflexive
proof end;

registration
let C1 be non empty transitive with_units AltCatStr ;
let C2 be non empty with_units AltCatStr ;
cluster covariant -> reflexive for Functor of C1,C2;
coherence
for b1 being Functor of C1,C2 st b1 is covariant holds
b1 is reflexive
;
end;

registration
let C1 be non empty transitive with_units AltCatStr ;
let C2 be non empty with_units AltCatStr ;
cluster contravariant -> reflexive for Functor of C1,C2;
coherence
for b1 being Functor of C1,C2 st b1 is contravariant holds
b1 is reflexive
;
end;

theorem Th46: :: FUNCTOR0:46
for C1 being non empty transitive with_units AltCatStr
for C2 being non empty with_units AltCatStr
for F being Functor of C1,C2 st F is covariant & F is onto holds
F is coreflexive by Th44;

theorem Th47: :: FUNCTOR0:47
for C1 being non empty transitive with_units AltCatStr
for C2 being non empty with_units AltCatStr
for F being Functor of C1,C2 st F is contravariant & F is onto holds
F is coreflexive by Th45;

theorem Th48: :: FUNCTOR0:48
for A, B being non empty transitive with_units AltCatStr
for F being covariant Functor of A,B st F is bijective holds
ex G being Functor of B,A st
( G = F " & G is bijective & G is covariant )
proof end;

theorem Th49: :: FUNCTOR0:49
for A, B being non empty transitive with_units AltCatStr
for F being contravariant Functor of A,B st F is bijective holds
ex G being Functor of B,A st
( G = F " & G is bijective & G is contravariant )
proof end;

definition
let A, B be non empty transitive with_units AltCatStr ;
pred A,B are_isomorphic means :: FUNCTOR0:def 39
ex F being Functor of A,B st
( F is bijective & F is covariant );
reflexivity
for A being non empty transitive with_units AltCatStr ex F being Functor of A,A st
( F is bijective & F is covariant )
proof end;
symmetry
for A, B being non empty transitive with_units AltCatStr st ex F being Functor of A,B st
( F is bijective & F is covariant ) holds
ex F being Functor of B,A st
( F is bijective & F is covariant )
proof end;
pred A,B are_anti-isomorphic means :: FUNCTOR0:def 40
ex F being Functor of A,B st
( F is bijective & F is contravariant );
symmetry
for A, B being non empty transitive with_units AltCatStr st ex F being Functor of A,B st
( F is bijective & F is contravariant ) holds
ex F being Functor of B,A st
( F is bijective & F is contravariant )
proof end;
end;

:: deftheorem defines are_isomorphic FUNCTOR0:def 39 :
for A, B being non empty transitive with_units AltCatStr holds
( A,B are_isomorphic iff ex F being Functor of A,B st
( F is bijective & F is covariant ) );

:: deftheorem defines are_anti-isomorphic FUNCTOR0:def 40 :
for A, B being non empty transitive with_units AltCatStr holds
( A,B are_anti-isomorphic iff ex F being Functor of A,B st
( F is bijective & F is contravariant ) );