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

begin

scheme :: FUNCTOR0:sch 1
ValOnPair{ F₁() -> non empty set , F₂() -> Function, F₃() -> Element of F₁(), F₄() -> Element of F₁(), F₅( set , set ) -> set , P₁[ set , set ] } :

F₂() . (F₃(),F₄()) = F₅(F₃(),F₄())

provided

A1: F₂() = { [[o,o9],F₅(o,o9)] where o, o9 is Element of F₁() : P₁[o,o9] } and
A2: P₁[F₃(),F₄()]

proof end;

theorem Th1: :: FUNCTOR0:1

for A being set holds {} is Function of A,{}

proof end;

theorem :: FUNCTOR0:2

canceled;

theorem Th3: :: FUNCTOR0:3

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

proof end;

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 Th4: :: FUNCTOR0:4

for A being set
for f being Function holds f .: (id A) = (~ f) .: (id A)

proof end;

theorem Th5: :: FUNCTOR0:5

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;
cluster ~ f -> Function-yielding ;
coherence
~ f is Function-yielding ;

end;

theorem Th6: :: FUNCTOR0:6

for A, B, a being set holds ~ ([:A,B:] --> a) = [:B,A:] --> a

proof end;

theorem Th7: :: FUNCTOR0:7

for f, g being Function st f is one-to-one & g is one-to-one holds
[:f,g:] " = [:(f "),(g "):]

proof end;

theorem Th8: :: FUNCTOR0:8

for f being Function st [:f,f:] is one-to-one holds
f is one-to-one

proof end;

theorem Th9: :: FUNCTOR0:9

for f being Function st f is one-to-one holds
~ f is one-to-one

proof end;

theorem Th10: :: FUNCTOR0:10

for f, g being Function st ~ [:f,g:] is one-to-one holds
[:g,f:] is one-to-one

proof end;

theorem Th11: :: FUNCTOR0:11

for f, g being Function st f is one-to-one & g is one-to-one holds
(~ [:f,g:]) " = ~ ([:g,f:] ")

proof end;

theorem Th12: :: FUNCTOR0:12

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 Th13: :: FUNCTOR0:13

for F, G being Function-yielding Function
for f being Function holds (G ** F) * f = (G * f) ** (F * f)

proof end;

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

proof end;

end;

theorem Th14: :: FUNCTOR0:14

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 Th15: :: FUNCTOR0:15

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;

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;
canceled;
attr f is Covariant means :Def2: :: FUNCTOR0:def 2
ex g being Function of A,B st f = [:g,g:];
attr f is Contravariant means :Def3: :: FUNCTOR0:def 3
ex g being Function of A,B st f = ~ [:g,g:];

end;

:: deftheorem FUNCTOR0:def 1 :
canceled;

:: deftheorem Def2 defines Covariant FUNCTOR0:def 2 :
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 Def3 defines Contravariant FUNCTOR0:def 3 :
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 Th16: :: FUNCTOR0:16

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

proof end;

end;

theorem :: FUNCTOR0:17

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;

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 :Def4: :: FUNCTOR0:def 4
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 = [[0]] I1;
existence
( ( I2 <> {} implies ex b₁ 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 & b₁ is ManySortedFunction of A,B9 * f9 ) ) & ( not I2 <> {} implies ex b₁ being ManySortedSet of I1 st b₁ = [[0]] I1 ) )

proof end;

consistency
for b₁ being ManySortedSet of I1 holds verum ;

end;

:: deftheorem Def4 defines MSUnTrans FUNCTOR0:def 4 :
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 b₆ being ManySortedSet of I1 holds
( ( I2 <> {} implies ( b₆ 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 & b₆ is ManySortedFunction of A,B9 * f9 ) ) ) & ( not I2 <> {} implies ( b₆ is MSUnTrans of f,A,B iff b₆ = [[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 :Def5: :: FUNCTOR0:def 5
it is ManySortedFunction of A,B * f;
compatibility
for b₁ being ManySortedSet of I1 holds
( b₁ is MSUnTrans of f,A,B iff b₁ is ManySortedFunction of A,B * f )

proof end;

end;

:: deftheorem Def5 defines MSUnTrans FUNCTOR0:def 5 :
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 b₆ being ManySortedSet of I1 holds
( b₆ is MSUnTrans of f,A,B iff b₆ 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 MSUnTrans of f,A,B;
coherence
for b₁ being MSUnTrans of f,A,B holds b₁ is Function-yielding

proof end;

end;

theorem Th18: :: FUNCTOR0:18

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 Th19: :: FUNCTOR0:19

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 Th20: :: FUNCTOR0:20

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;

begin

definition

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

end;

definition

let C1, C2 be non empty AltGraph ;
let F be BimapStr of C1,C2;
let o be object of C1;
func F . o -> object of C2 equals :: FUNCTOR0:def 6
( 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 6 :
for C1, C2 being non empty AltGraph
for F being BimapStr of 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 of A,B;
attr F is one-to-one means :Def7: :: FUNCTOR0:def 7
the ObjectMap of F is one-to-one ;
attr F is onto means :Def8: :: FUNCTOR0:def 8
the ObjectMap of F is onto ;
attr F is reflexive means :Def9: :: FUNCTOR0:def 9
the ObjectMap of F .: (id the carrier of A) c= id the carrier of B;
attr F is coreflexive means :Def10: :: FUNCTOR0:def 10
id the carrier of B c= the ObjectMap of F .: (id the carrier of A);

end;

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

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

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

:: deftheorem Def10 defines coreflexive FUNCTOR0:def 10 :
for A, B being 1-sorted
for F being BimapStr of 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 of A,B;
redefine attr F is reflexive means :Def11: :: FUNCTOR0:def 11
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 Def11 defines reflexive FUNCTOR0:def 11 :
for A, B being non empty AltGraph
for F being BimapStr of 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 Th21: :: FUNCTOR0:21

for A, B being non empty reflexive AltGraph
for F being BimapStr of 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 of C1,C2;
attr F is feasible means :Def12: :: FUNCTOR0:def 12
for o1, o2 being object of C1 st <^o1,o2^> <> {} holds
the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {} ;

end;

:: deftheorem Def12 defines feasible FUNCTOR0:def 12 :
for C1, C2 being non empty AltGraph
for F being BimapStr of 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 c₃ is strict ;
struct FunctorStr of C1,C2 -> BimapStr of C1,C2;
aggr FunctorStr(# ObjectMap, MorphMap #) -> FunctorStr of C1,C2;
sel MorphMap c₃ -> MSUnTrans of the ObjectMap of c₃, the Arrows of C1, the Arrows of C2;

end;

definition

let C1, C2 be 1-sorted ;
let IT be BimapStr of C1,C2;
attr IT is Covariant means :Def13: :: FUNCTOR0:def 13
the ObjectMap of IT is Covariant ;
attr IT is Contravariant means :Def14: :: FUNCTOR0:def 14
the ObjectMap of IT is Contravariant ;

end;

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

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

registration

let C1, C2 be AltGraph ;
cluster Covariant FunctorStr of C1,C2;
existence
ex b₁ being FunctorStr of C1,C2 st b₁ is Covariant

proof end;

cluster Contravariant FunctorStr of C1,C2;
existence
ex b₁ being FunctorStr of C1,C2 st b₁ is Contravariant

proof end;

end;

definition

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

end;

:: deftheorem defines Morph-Map FUNCTOR0:def 15 :
for C1, C2 being AltGraph
for F being FunctorStr of 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 of 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 of 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 of 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 :Def16: :: FUNCTOR0:def 16
(Morph-Map (F,o1,o2)) . m;
coherence
(Morph-Map (F,o1,o2)) . m is Morphism of (F . o1),(F . o2)

proof end;

end;

:: deftheorem Def16 defines . FUNCTOR0:def 16 :
for C1, C2 being non empty AltGraph
for F being Covariant FunctorStr of 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 of 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 of 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 :Def17: :: FUNCTOR0:def 17
(Morph-Map (F,o1,o2)) . m;
coherence
(Morph-Map (F,o1,o2)) . m is Morphism of (F . o2),(F . o1)

proof end;

end;

:: deftheorem Def17 defines . FUNCTOR0:def 17 :
for C1, C2 being non empty AltGraph
for F being Contravariant FunctorStr of 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 of C1,C2 means :Def18: :: FUNCTOR0:def 18
( 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 b₁ being strict FunctorStr of C1,C2 st
( the ObjectMap of b₁ = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b₁ = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } )

proof end;

uniqueness
for b₁, b₂ being strict FunctorStr of C1,C2 st the ObjectMap of b₁ = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b₁ = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } & the ObjectMap of b₂ = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b₂ = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } holds
b₁ = b₂ ;

end;

:: deftheorem Def18 defines --> FUNCTOR0:def 18 :
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 b₅ being strict FunctorStr of C1,C2 holds
( b₅ = C1 --> m iff ( the ObjectMap of b₅ = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b₅ = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } ) );

theorem Th22: :: FUNCTOR0:22

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;
cluster C1 --> m -> feasible strict Covariant Contravariant ;
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 FunctorStr of C1,C2;
existence
ex b₁ being FunctorStr of C1,C2 st
( b₁ is feasible & b₁ is Covariant & b₁ is Contravariant )

proof end;

end;

theorem Th23: :: FUNCTOR0:23

for C1, C2 being non empty AltGraph
for F being Covariant FunctorStr of 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 of C1,C2;
redefine attr F is feasible means :Def19: :: FUNCTOR0:def 19
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 Def19 defines feasible FUNCTOR0:def 19 :
for C1, C2 being non empty AltGraph
for F being Covariant FunctorStr of C1,C2 holds
( F is feasible iff for o1, o2 being object of C1 st <^o1,o2^> <> {} holds
<^(F . o1),(F . o2)^> <> {} );

theorem Th24: :: FUNCTOR0:24

for C1, C2 being non empty AltGraph
for F being Contravariant FunctorStr of 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 of C1,C2;
redefine attr F is feasible means :Def20: :: FUNCTOR0:def 20
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 Def20 defines feasible FUNCTOR0:def 20 :
for C1, C2 being non empty AltGraph
for F being Contravariant FunctorStr of 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 of C1,C2;
cluster the MorphMap of F -> Function-yielding ;
coherence
the MorphMap of F is Function-yielding ;

end;

registration

cluster non empty reflexive AltCatStr ;
existence
ex b₁ being AltCatStr st
( not b₁ is empty & b₁ is reflexive )

proof end;

end;

definition

let C1, C2 be non empty with_units AltCatStr ;
let F be FunctorStr of C1,C2;
attr F is id-preserving means :Def21: :: FUNCTOR0:def 21
for o being object of C1 holds (Morph-Map (F,o,o)) . (idm o) = idm (F . o);

end;

:: deftheorem Def21 defines id-preserving FUNCTOR0:def 21 :
for C1, C2 being non empty with_units AltCatStr
for F being FunctorStr of 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 Th25: :: FUNCTOR0:25

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 AltCatStr ;
coherence
for b₁ being non empty AltCatStr st b₁ is with_units holds
b₁ 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;
cluster C1 --> m -> reflexive strict ;
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 FunctorStr of C1,C2;
existence
ex b₁ being FunctorStr of C1,C2 st
( b₁ is feasible & b₁ is reflexive )

proof end;

end;

registration

let C1, C2 be non empty with_units AltCatStr ;
cluster reflexive feasible strict id-preserving FunctorStr of C1,C2;
existence
ex b₁ being FunctorStr of C1,C2 st
( b₁ is id-preserving & b₁ is feasible & b₁ is reflexive & b₁ is strict )

proof end;

end;

definition

let C1, C2 be non empty AltCatStr ;
let F be FunctorStr of C1,C2;
attr F is comp-preserving means :Def22: :: 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 . 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 Def22 defines comp-preserving FUNCTOR0:def 22 :
for C1, C2 being non empty AltCatStr
for F being FunctorStr of 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 of C1,C2;
attr F is comp-reversing means :Def23: :: 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 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 Def23 defines comp-reversing FUNCTOR0:def 23 :
for C1, C2 being non empty AltCatStr
for F being FunctorStr of 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 of C1,C2;
redefine attr F is comp-preserving 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 . 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 24 :
for C1 being non empty transitive AltCatStr
for C2 being non empty reflexive AltCatStr
for F being feasible Covariant FunctorStr of 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 of C1,C2;
redefine attr F is comp-reversing means :: FUNCTOR0:def 25
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 25 :
for C1 being non empty transitive AltCatStr
for C2 being non empty reflexive AltCatStr
for F being feasible Contravariant FunctorStr of 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 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 F being feasible Covariant FunctorStr of 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 Th27: :: FUNCTOR0:27

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;
cluster C1 --> (idm o) -> strict comp-preserving comp-reversing ;
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 of C1,C2 means :Def26: :: FUNCTOR0:def 26
( it is feasible & it is id-preserving & ( ( it is Covariant & it is comp-preserving ) or ( it is Contravariant & it is comp-reversing ) ) );
existence
ex b₁ being FunctorStr of C1,C2 st
( b₁ is feasible & b₁ is id-preserving & ( ( b₁ is Covariant & b₁ is comp-preserving ) or ( b₁ is Contravariant & b₁ is comp-reversing ) ) )

proof end;

end;

:: deftheorem Def26 defines Functor FUNCTOR0:def 26 :
for C1 being non empty transitive with_units AltCatStr
for C2 being non empty with_units AltCatStr
for b₃ being FunctorStr of C1,C2 holds
( b₃ is Functor of C1,C2 iff ( b₃ is feasible & b₃ is id-preserving & ( ( b₃ is Covariant & b₃ is comp-preserving ) or ( b₃ is Contravariant & b₃ 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 :Def27: :: FUNCTOR0:def 27
( F is Covariant & F is comp-preserving );
attr F is contravariant means :Def28: :: FUNCTOR0:def 28
( F is Contravariant & F is comp-reversing );

end;

:: deftheorem Def27 defines covariant 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 covariant iff ( F is Covariant & F is comp-preserving ) );

:: deftheorem Def28 defines contravariant FUNCTOR0:def 28 :
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 of B,A means :Def29: :: FUNCTOR0:def 29
( the ObjectMap of it = id [: the carrier of B, the carrier of B:] & the MorphMap of it = id the Arrows of B );
existence
ex b₁ being strict FunctorStr of B,A st
( the ObjectMap of b₁ = id [: the carrier of B, the carrier of B:] & the MorphMap of b₁ = id the Arrows of B )

proof end;

correctness
uniqueness
for b₁, b₂ being strict FunctorStr of B,A st the ObjectMap of b₁ = id [: the carrier of B, the carrier of B:] & the MorphMap of b₁ = id the Arrows of B & the ObjectMap of b₂ = id [: the carrier of B, the carrier of B:] & the MorphMap of b₂ = id the Arrows of B holds
b₁ = b₂;
;

end;

:: deftheorem Def29 defines incl FUNCTOR0:def 29 :
for A being AltCatStr
for B being SubCatStr of A
for b₃ being strict FunctorStr of B,A holds
( b₃ = incl B iff ( the ObjectMap of b₃ = id [: the carrier of B, the carrier of B:] & the MorphMap of b₃ = id the Arrows of B ) );

definition

let A be AltGraph ;
func id A -> strict FunctorStr of A,A means :Def30: :: FUNCTOR0:def 30
( the ObjectMap of it = id [: the carrier of A, the carrier of A:] & the MorphMap of it = id the Arrows of A );
existence
ex b₁ being strict FunctorStr of A,A st
( the ObjectMap of b₁ = id [: the carrier of A, the carrier of A:] & the MorphMap of b₁ = id the Arrows of A )

proof end;

correctness
uniqueness
for b₁, b₂ being strict FunctorStr of A,A st the ObjectMap of b₁ = id [: the carrier of A, the carrier of A:] & the MorphMap of b₁ = id the Arrows of A & the ObjectMap of b₂ = id [: the carrier of A, the carrier of A:] & the MorphMap of b₂ = id the Arrows of A holds
b₁ = b₂;
;

end;

:: deftheorem Def30 defines id FUNCTOR0:def 30 :
for A being AltGraph
for b₂ being strict FunctorStr of A,A holds
( b₂ = id A iff ( the ObjectMap of b₂ = id [: the carrier of A, the carrier of A:] & the MorphMap of b₂ = 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

proof end;

end;

theorem Th28: :: FUNCTOR0:28

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 Th29: :: FUNCTOR0:29

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;
cluster incl B -> feasible strict ;
coherence
incl B is feasible

proof end;

end;

definition

let A, B be AltGraph ;
let F be FunctorStr of A,B;
attr F is faithful means :Def31: :: FUNCTOR0:def 31
the MorphMap of F is "1-1" ;

end;

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

definition

let A, B be AltGraph ;
let F be FunctorStr of A,B;
attr F is full means :Def32: :: FUNCTOR0:def 32
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 Def32 defines full FUNCTOR0:def 32 :
for A, B being AltGraph
for F being FunctorStr of 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 of A,B;
redefine attr F is full means :Def33: :: FUNCTOR0:def 33
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" ) )

proof end;

end;

:: deftheorem Def33 defines full FUNCTOR0:def 33 :
for A being AltGraph
for B being non empty AltGraph
for F being FunctorStr of 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 of A,B;
attr F is injective means :Def34: :: FUNCTOR0:def 34
( F is one-to-one & F is faithful );
attr F is surjective means :Def35: :: FUNCTOR0:def 35
( F is full & F is onto );

end;

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

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

definition

let A, B be AltGraph ;
let F be FunctorStr of A,B;
attr F is bijective means :Def36: :: FUNCTOR0:def 36
( F is injective & F is surjective );

end;

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

registration

let A, B be non empty transitive with_units AltCatStr ;
cluster feasible strict covariant contravariant Functor of A,B;
existence
ex b₁ being Functor of A,B st
( b₁ is strict & b₁ is covariant & b₁ is contravariant & b₁ is feasible )

proof end;

end;

theorem Th30: :: FUNCTOR0:30

for A being non empty AltGraph
for o being object of A holds (id A) . o = o

proof end;

theorem Th31: :: FUNCTOR0:31

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 ;
cluster id A -> feasible strict Covariant ;
coherence
( id A is feasible & id A is Covariant )

proof end;

end;

registration

let A be non empty AltGraph ;
cluster feasible Covariant FunctorStr of A,A;
existence
ex b₁ being FunctorStr of A,A st
( b₁ is Covariant & b₁ is feasible )

proof end;

end;

theorem Th32: :: FUNCTOR0:32

for A being non empty AltGraph
for o1, o2 being object of A st <^o1,o2^> <> {} holds
for F being feasible Covariant FunctorStr of 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 ;
cluster id A -> strict id-preserving comp-preserving ;
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 Def26, Def27;

end;

registration

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

proof end;

end;

begin

definition

let C1 be non empty AltGraph ;
let C2, C3 be non empty reflexive AltGraph ;
let F be feasible FunctorStr of C1,C2;
let G be FunctorStr of C2,C3;
func G * F -> strict FunctorStr of C1,C3 means :Def37: :: FUNCTOR0:def 37
( 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 b₁ being strict FunctorStr of C1,C3 st
( the ObjectMap of b₁ = the ObjectMap of G * the ObjectMap of F & the MorphMap of b₁ = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F )

proof end;

correctness
uniqueness
for b₁, b₂ being strict FunctorStr of C1,C3 st the ObjectMap of b₁ = the ObjectMap of G * the ObjectMap of F & the MorphMap of b₁ = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F & the ObjectMap of b₂ = the ObjectMap of G * the ObjectMap of F & the MorphMap of b₂ = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F holds
b₁ = b₂;
;

end;

:: deftheorem Def37 defines * FUNCTOR0:def 37 :
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr of C1,C2
for G being FunctorStr of C2,C3
for b₆ being strict FunctorStr of C1,C3 holds
( b₆ = G * F iff ( the ObjectMap of b₆ = the ObjectMap of G * the ObjectMap of F & the MorphMap of b₆ = ( 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 of C1,C2;
let G be Covariant FunctorStr of C2,C3;
cluster G * F -> strict Covariant ;
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 of C1,C2;
let G be Covariant FunctorStr of C2,C3;
cluster G * F -> strict Contravariant ;
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 of C1,C2;
let G be Contravariant FunctorStr of C2,C3;
cluster G * F -> strict Contravariant ;
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 of C1,C2;
let G be Contravariant FunctorStr of C2,C3;
cluster G * F -> strict Covariant ;
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 of C1,C2;
let G be feasible FunctorStr of C2,C3;
cluster G * F -> feasible strict ;
coherence
G * F is feasible

proof end;

end;

theorem :: FUNCTOR0:33

for C1 being non empty AltGraph
for C2, C3, C4 being non empty reflexive AltGraph
for F being feasible FunctorStr of C1,C2
for G being feasible FunctorStr of C2,C3
for H being FunctorStr of C3,C4 holds (H * G) * F = H * (G * F)

proof end;

theorem Th34: :: FUNCTOR0:34

for C1 being non empty AltCatStr
for C2, C3 being non empty reflexive AltCatStr
for F being reflexive feasible FunctorStr of C1,C2
for G being FunctorStr of C2,C3
for o being object of C1 holds (G * F) . o = G . (F . o)

proof end;

theorem Th35: :: FUNCTOR0:35

for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being reflexive feasible FunctorStr of C1,C2
for G being FunctorStr of 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 of C1,C2;
let G be id-preserving FunctorStr of C2,C3;
cluster G * F -> strict id-preserving ;
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 of A,C;
func F | B -> FunctorStr of B,C equals :: FUNCTOR0:def 38
F * (incl B);
correctness
coherence
F * (incl B) is FunctorStr of B,C;
;

end;

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

begin

definition

let A, B be non empty AltGraph ;
let F be FunctorStr of A,B;
assume A1: F is bijective ;
func F " -> strict FunctorStr of B,A means :Def39: :: FUNCTOR0:def 39
( 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 b₁ being strict FunctorStr of B,A st
( the ObjectMap of b₁ = 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 b₁ = (f "") * ( the ObjectMap of F ") ) )

proof end;

uniqueness
for b₁, b₂ being strict FunctorStr of B,A st the ObjectMap of b₁ = 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 b₁ = (f "") * ( the ObjectMap of F ") ) & the ObjectMap of b₂ = 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 b₂ = (f "") * ( the ObjectMap of F ") ) holds
b₁ = b₂ ;

end;

:: deftheorem Def39 defines " FUNCTOR0:def 39 :
for A, B being non empty AltGraph
for F being FunctorStr of A,B st F is bijective holds
for b₄ being strict FunctorStr of B,A holds
( b₄ = F " iff ( the ObjectMap of b₄ = 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 b₄ = (f "") * ( the ObjectMap of F ") ) ) );

theorem Th36: :: FUNCTOR0:36

for A, B being non empty transitive with_units AltCatStr
for F being feasible FunctorStr of A,B st F is bijective holds
( F " is bijective & F " is feasible )

proof end;

theorem Th37: :: FUNCTOR0:37

for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr of A,B st F is bijective & F is coreflexive holds
F " is reflexive

proof end;

theorem Th38: :: FUNCTOR0:38

for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible id-preserving FunctorStr of A,B st F is bijective & F is coreflexive holds
F " is id-preserving

proof end;

theorem Th39: :: FUNCTOR0:39

for A, B being non empty transitive with_units AltCatStr
for F being feasible FunctorStr of A,B st F is bijective & F is Covariant holds
F " is Covariant

proof end;

theorem Th40: :: FUNCTOR0:40

for A, B being non empty transitive with_units AltCatStr
for F being feasible FunctorStr of A,B st F is bijective & F is Contravariant holds
F " is Contravariant

proof end;

theorem Th41: :: FUNCTOR0:41

for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr of 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 Th42: :: FUNCTOR0:42

for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr of 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 Th43: :: FUNCTOR0:43

for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr of A,B st F is bijective & F is comp-preserving & F is Covariant & F is coreflexive holds
F " is comp-preserving

proof end;

theorem Th44: :: FUNCTOR0:44

for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr of 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 BimapStr of C1,C2;
coherence
for b₁ being BimapStr of C1,C2 st b₁ is Covariant holds
b₁ is reflexive

proof end;

end;

registration

let C1 be 1-sorted ;
let C2 be non empty 1-sorted ;
cluster Contravariant -> reflexive BimapStr of C1,C2;
coherence
for b₁ being BimapStr of C1,C2 st b₁ is Contravariant holds
b₁ is reflexive

proof end;

end;

theorem Th45: :: FUNCTOR0:45

for C1, C2 being 1-sorted
for M being BimapStr of C1,C2 st M is Covariant & M is onto holds
M is coreflexive

proof end;

theorem Th46: :: FUNCTOR0:46

for C1, C2 being 1-sorted
for M being BimapStr of 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 Functor of C1,C2;
coherence
for b₁ being Functor of C1,C2 st b₁ is covariant holds
b₁ is reflexive

proof end;

end;

registration

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

proof end;

end;

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 covariant & F is onto holds
F is coreflexive

proof end;

theorem Th48: :: FUNCTOR0:48

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

proof end;

theorem Th49: :: FUNCTOR0:49

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 Th50: :: FUNCTOR0:50

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 40
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 41
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 40 :
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 41 :
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 ) );