:: Functors for Alternative Categories
:: by Andrzej Trybulec
::
:: Received April 24, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

scheme :: FUNCTOR0:sch 1
ValOnPair{ F1() ->  non empty set , F2() ->  Function, F3() ->  Element of F1(), F4() ->  Element of F1(), F5( set , set ) ->  set , P1[ set , set ] } :
 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()]
proofend;

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

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

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

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

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 )
proofend;

registration
let f be Function-yielding Function;
cluster ~ f ->  Function-yielding ;
coherence
 ~ f is Function-yielding ;
end;

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

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 "):]
proofend;

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

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

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

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:] ")
proofend;

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)
proofend;

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

definition
let A, B, C be set ;
let f be Function of [:A,B:],C;
:: original:~
redefine func ~ f ->  Function of [:B,A:],C;
coherence
 ~ f is Function of [:B,A:],C
proofend;
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
proofend;

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
proofend;

begin

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;
attrf is Covariant  means :Def1: :: FUNCTOR0:def 1
 ex g being Function of A,B st f = [:g,g:];
attrf 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 )
proofend;

registration
let A, B be set ;
cluster Relation-like [:A,A:] -defined [:B,B:] -valued Function-like quasi_total Covariant Contravariant for Element of bool [:[:A,A:],[:B,B:]:];
existence
 ex b1 being bifunction of A,B st
( b1 is Covariant & b1 is Contravariant )
proofend;
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]
proofend;

begin

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 &amp; B = B9 &amp; it is ManySortedFunction of A,B9 * f9 ) if I2 <> {}
otherwise it = [[0]] 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 &amp; B = B9 &amp; b1 is ManySortedFunction of A,B9 * f9 ) ) &amp; ( not I2 <> {} implies ex b1 being ManySortedSet of I1 st b1 = [[0]] I1 ) )
proofend;
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 &amp; B = B9 &amp; b6 is ManySortedFunction of A,B9 * f9 ) ) ) &amp; ( not I2 <> {} implies ( b6 is MSUnTrans of f,A,B iff b6 = [[0]] 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 )
proofend;
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
proofend;
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
proofend;

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
proofend;
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
proofend;

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 &amp; (B * f) . ii = {} &amp; not A . ii = {} holds
(C * (g * f)) . ii = {} ) holds
G ** F is MSUnTrans of g * f,A,C
proofend;

begin

definition
let C1, C2 be 1-sorted ;
attrc3 is strict ;
struct BimapStr over C1,C2 -> ;
aggrBimapStr(# 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;
funcF . 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;
attrF is one-to-one  means :Def6: :: FUNCTOR0:def 6
 the ObjectMap of F is one-to-one ;
attrF is onto  means :Def7: :: FUNCTOR0:def 7
 the ObjectMap of F is onto ;
attrF is reflexive  means :Def8: :: FUNCTOR0:def 8
 the ObjectMap of F .: (id the carrier of A) c= id the carrier of B;
attrF is coreflexive  means :Def9: :: FUNCTOR0:def 9
 id the carrier of B c= the ObjectMap of F .: (id the carrier of A);
end;

:: deftheorem Def6 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 Def7 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 Def8 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 Def9 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)] )
proofend;
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
proofend;

definition
let C1, C2 be non empty AltGraph ;
let F be BimapStr over C1,C2;
attrF 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 ;
attrc3 is strict ;
struct FunctorStr over C1,C2 ->  BimapStr over C1,C2;
aggrFunctorStr(# 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;
attrIT is Covariant  means :Def12: :: FUNCTOR0:def 12
 the ObjectMap of IT is Covariant ;
attrIT 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
proofend;
cluster Contravariant for FunctorStr over C1,C2;
existence
 ex b1 being FunctorStr over C1,C2 st b1 is Contravariant
proofend;
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 &amp; 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)^>
proofend;
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;
funcF . 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)
proofend;
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^> <> {} &amp; <^(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)^>
proofend;
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;
funcF . 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)
proofend;
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^> <> {} &amp; <^(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 B1: <^o,o^> <> {} ;
let m be Morphism of o,o;
funcC1 --> 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] &amp; 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] &amp; the MorphMap of b1 =  {  [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum  }  )
proofend;
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] &amp; the MorphMap of b1 =  {  [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum  }  &amp; the ObjectMap of b2 = [: the carrier of C1, the carrier of C1:] --> [o,o] &amp; 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] &amp; 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
proofend;

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;
clusterC1 --> m ->  feasible strict Covariant Contravariant ;
coherence
 ( C1 --> m is Covariant &amp; C1 --> m is Contravariant &amp; C1 --> m is feasible )
proofend;
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 &amp; b1 is Covariant &amp; b1 is Contravariant )
proofend;
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)]
proofend;

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)^> <> {} )
proofend;
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)]
proofend;

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)^> <> {} )
proofend;
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
cluster non empty reflexive for AltCatStr ;
existence
 ex b1 being AltCatStr st
( not b1 is empty &amp; b1 is reflexive )
proofend;
end;

:: Wlasnosci funktorow, Semadeni-Wiweger str. 32
definition
let C1, C2 be non empty with_units AltCatStr ;
let F be FunctorStr over C1,C2;
attrF 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
proofend;

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;
clusterC1 --> (idm o2) ->  strict id-preserving ;
coherence
 C1 --> (idm o2) is id-preserving
proofend;
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;
clusterC1 --> m ->  reflexive strict ;
coherence
 C1 --> m is reflexive
proofend;
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 &amp; b1 is reflexive )
proofend;
end;

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

definition
let C1, C2 be non empty AltCatStr ;
let F be FunctorStr over C1,C2;
attrF is comp-preserving  means :Def21: :: FUNCTOR0:def 21
 for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} &amp; <^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 &amp; g9 = (Morph-Map (F,o2,o3)) . g &amp; (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 );
end;

:: deftheorem Def21 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^> <> {} &amp; <^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 &amp; g9 = (Morph-Map (F,o2,o3)) . g &amp; (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 ) );

definition
let C1, C2 be non empty AltCatStr ;
let F be FunctorStr over C1,C2;
attrF is comp-reversing  means :Def22: :: FUNCTOR0:def 22
 for o1, o2, o3 being object of C1 st <^o1,o2^> <> {} &amp; <^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 &amp; g9 = (Morph-Map (F,o2,o3)) . g &amp; (Morph-Map (F,o1,o3)) . (g * f) = f9 * g9 );
end;

:: deftheorem Def22 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^> <> {} &amp; <^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 &amp; g9 = (Morph-Map (F,o2,o3)) . g &amp; (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^> <> {} &amp; <^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^> <> {} &amp; <^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) )
proofend;
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^> <> {} &amp; <^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^> <> {} &amp; <^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^> <> {} &amp; <^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) )
proofend;
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^> <> {} &amp; <^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
proofend;

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
proofend;

registration
let C1 be non empty transitive AltCatStr ;
let C2 be non empty with_units AltCatStr ;
let o be object of C2;
clusterC1 --> (idm o) ->  strict comp-preserving comp-reversing ;
coherence
 ( C1 --> (idm o) is comp-preserving &amp; C1 --> (idm o) is comp-reversing )
proofend;
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 &amp; it is id-preserving &amp; ( ( it is Covariant &amp; it is comp-preserving ) or ( it is Contravariant &amp; it is comp-reversing ) ) );
existence
 ex b1 being FunctorStr over C1,C2 st
( b1 is feasible &amp; b1 is id-preserving &amp; ( ( b1 is Covariant &amp; b1 is comp-preserving ) or ( b1 is Contravariant &amp; b1 is comp-reversing ) ) )
proofend;
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 &amp; b3 is id-preserving &amp; ( ( b3 is Covariant &amp; b3 is comp-preserving ) or ( b3 is Contravariant &amp; 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;
attrF is covariant  means :Def26: :: FUNCTOR0:def 26
( F is Covariant &amp; F is comp-preserving );
attrF is contravariant  means :Def27: :: FUNCTOR0:def 27
( F is Contravariant &amp; 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 &amp; 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 &amp; 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:] &amp; 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:] &amp; the MorphMap of b1 = id the Arrows of B )
proofend;
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:] &amp; the MorphMap of b1 = id the Arrows of B &amp; the ObjectMap of b2 = id [: the carrier of B, the carrier of B:] &amp; 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:] &amp; 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:] &amp; 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:] &amp; the MorphMap of b1 = id the Arrows of A )
proofend;
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:] &amp; the MorphMap of b1 = id the Arrows of A &amp; the ObjectMap of b2 = id [: the carrier of A, the carrier of A:] &amp; 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:] &amp; the MorphMap of b2 = id the Arrows of A ) );

registration
let A be AltCatStr ;
let B be SubCatStr of A;
cluster incl B ->  strict Covariant ;
coherence
 incl B is Covariant
proofend;
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
proofend;

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)^>
proofend;

registration
let A be non empty AltCatStr ;
let B be non empty SubCatStr of A;
cluster incl B ->  feasible strict ;
coherence
 incl B is feasible
proofend;
end;

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

:: deftheorem Def30 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;
attrF is full  means :Def31: :: 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 &amp; f = the MorphMap of F &amp; f is "onto" );
end;

:: deftheorem Def31 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 &amp; f = the MorphMap of F &amp; 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 :Def32: :: 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 &amp; 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 &amp; f is "onto" ) )
proofend;
end;

:: deftheorem Def32 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 &amp; f is "onto" ) );

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

:: deftheorem Def33 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 &amp; F is faithful ) );

:: deftheorem Def34 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 &amp; F is onto ) );

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

:: deftheorem Def35 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 &amp; F is surjective ) );

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

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

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
proofend;

registration
let A be non empty AltGraph ;
cluster id A ->  feasible strict Covariant ;
coherence
 ( id A is feasible &amp; id A is Covariant )
proofend;
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 &amp; b1 is feasible )
proofend;
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
proofend;

registration
let A be non empty transitive with_units AltCatStr ;
cluster id A ->  strict id-preserving comp-preserving ;
coherence
 ( id A is id-preserving &amp; id A is comp-preserving )
proofend;
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 Def25, Def26;
end;

registration
let A be AltGraph ;
cluster id A ->  strict bijective ;
coherence
 id A is bijective
proofend;
end;

begin

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;
funcG * F ->  strict FunctorStr over C1,C3 means :Def36: :: FUNCTOR0:def 36
( the ObjectMap of it = the ObjectMap of G * the ObjectMap of F &amp; 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 &amp; the MorphMap of b1 = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F )
proofend;
correctness
uniqueness
for b1, b2 being strict FunctorStr over C1,C3 st the ObjectMap of b1 = the ObjectMap of G * the ObjectMap of F &amp; the MorphMap of b1 = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F &amp; the ObjectMap of b2 = the ObjectMap of G * the ObjectMap of F &amp; 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 &amp; 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;
clusterG * F ->  strict Covariant ;
correctness
coherence
G * F is Covariant ;
proofend;
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;
clusterG * F ->  strict Contravariant ;
correctness
coherence
G * F is Contravariant ;
proofend;
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;
clusterG * F ->  strict Contravariant ;
correctness
coherence
G * F is Contravariant ;
proofend;
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;
clusterG * F ->  strict Covariant ;
correctness
coherence
G * F is Covariant ;
proofend;
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;
clusterG * F ->  feasible strict ;
coherence
 G * F is feasible
proofend;
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)
proofend;

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)
proofend;

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))
proofend;

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;
clusterG * F ->  strict id-preserving ;
coherence
 G * F is id-preserving
proofend;
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;
funcF | 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);

begin

definition
let A, B be non empty AltGraph ;
let F be FunctorStr over A,B;
assume A1: F is bijective ;
funcF "  ->  strict FunctorStr over B,A means :Def38: :: FUNCTOR0:def 38
( the ObjectMap of it = the ObjectMap of F " &amp; ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F &amp; 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 " &amp; ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F &amp; the MorphMap of b1 = (f "") * ( the ObjectMap of F ") ) )
proofend;
uniqueness
 for b1, b2 being strict FunctorStr over B,A st the ObjectMap of b1 = the ObjectMap of F " &amp; ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F &amp; the MorphMap of b1 = (f "") * ( the ObjectMap of F ") ) &amp; the ObjectMap of b2 = the ObjectMap of F " &amp; ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F &amp; 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 " &amp; ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F &amp; 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 &amp; F " is feasible )
proofend;

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 &amp; F is coreflexive holds
F " is reflexive
proofend;

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 &amp; F is coreflexive holds
F " is id-preserving
proofend;

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 &amp; F is Covariant holds
F " is Covariant
proofend;

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 &amp; F is Contravariant holds
F " is Contravariant
proofend;

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 &amp; F is coreflexive &amp; 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
proofend;

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 &amp; F is coreflexive &amp; 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
proofend;

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 &amp; F is comp-preserving &amp; F is Covariant &amp; F is coreflexive holds
F " is comp-preserving
proofend;

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 &amp; F is comp-reversing &amp; F is Contravariant &amp; F is coreflexive holds
F " is comp-reversing
proofend;

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
proofend;
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
proofend;
end;

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

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

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
proofend;
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
proofend;
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 &amp; F is onto holds
F is coreflexive
proofend;

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 &amp; F is onto holds
F is coreflexive
proofend;

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 " &amp; G is bijective &amp; G is covariant )
proofend;

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 " &amp; G is bijective &amp; G is contravariant )
proofend;

definition
let A, B be non empty transitive with_units AltCatStr ;
predA,B are_isomorphic  means :: FUNCTOR0:def 39
 ex F being Functor of A,B st
( F is bijective &amp; F is covariant );
reflexivity
 for A being non empty transitive with_units AltCatStr ex F being Functor of A,A st
( F is bijective &amp; F is covariant )
proofend;
symmetry
 for A, B being non empty transitive with_units AltCatStr st ex F being Functor of A,B st
( F is bijective &amp; F is covariant ) holds
ex F being Functor of B,A st
( F is bijective &amp; F is covariant )
proofend;
predA,B are_anti-isomorphic  means :: FUNCTOR0:def 40
 ex F being Functor of A,B st
( F is bijective &amp; 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 &amp; F is contravariant ) holds
ex F being Functor of B,A st
( F is bijective &amp; F is contravariant )
proofend;
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 &amp; 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 &amp; F is contravariant ) );