:: by Andrzej Trybulec

::

:: Received April 24, 1996

:: Copyright (c) 1996-2019 Association of Mizar Users

scheme :: FUNCTOR0:sch 1

ValOnPair{ F_{1}() -> non empty set , F_{2}() -> Function, F_{3}() -> Element of F_{1}(), F_{4}() -> Element of F_{1}(), F_{5}( object , object ) -> set , P_{1}[ object , object ] } :

provided

ValOnPair{ F

provided

A1:
F_{2}() = { [[o,o9],F_{5}(o,o9)] where o, o9 is Element of F_{1}() : P_{1}[o,o9] }
and

A2: P_{1}[F_{3}(),F_{4}()]

A2: P

proof end;

registration

let f be empty Function;

coherence

~ f is empty ;

let g be Function;

coherence

[:f,g:] is empty

[:g,f:] is empty

end;
coherence

~ f is empty ;

let g be Function;

coherence

[:f,g:] is empty

proof end;

coherence [:g,f:] is empty

proof end;

theorem Th12: :: FUNCTOR0:12

for F, G being Function-yielding Function

for f being Function holds (G ** F) * f = (G * f) ** (F * f)

for f being Function holds (G ** F) * f = (G * f) ** (F * f)

proof end;

theorem Th14: :: FUNCTOR0:14

for A being set

for B being non empty set

for f being Function of A,B holds [:f,f:] .: (id A) c= id B

for B being non empty set

for f being Function of A,B holds [:f,f:] .: (id A) c= id B

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

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

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 )

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 ;

ex b_{1} being bifunction of A,B st

( b_{1} is Covariant & b_{1} is Contravariant )

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

( b

proof 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]

for f being Covariant Contravariant bifunction of A,B ex b being Element of B st f = [:A,A:] --> [b,b]

proof end;

definition

let I1, I2 be set ;

let f be Function of I1,I2;

let A be ManySortedSet of I1;

let B be ManySortedSet of I2;

( ( I2 <> {} implies ex b_{1} 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_{1} is ManySortedFunction of A,B9 * f9 ) ) & ( not I2 <> {} implies ex b_{1} being ManySortedSet of I1 st b_{1} = EmptyMS I1 ) )

for b_{1} being ManySortedSet of I1 holds verum
;

end;
let f be Function of I1,I2;

let A be ManySortedSet of I1;

let B be ManySortedSet of I2;

mode MSUnTrans of f,A,B -> ManySortedSet of I1 means :Def3: :: FUNCTOR0:def 3

ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st

( f = f9 & B = B9 & it is ManySortedFunction of A,B9 * f9 ) if I2 <> {}

otherwise it = EmptyMS I1;

existence ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of I1,I29 st

( f = f9 & B = B9 & it is ManySortedFunction of A,B9 * f9 ) if I2 <> {}

otherwise it = EmptyMS I1;

( ( I2 <> {} implies ex b

( f = f9 & B = B9 & b

proof end;

consistency for b

:: 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 b_{6} being ManySortedSet of I1 holds

( ( I2 <> {} implies ( b_{6} 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_{6} is ManySortedFunction of A,B9 * f9 ) ) ) & ( not I2 <> {} implies ( b_{6} is MSUnTrans of f,A,B iff b_{6} = EmptyMS I1 ) ) );

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

( ( I2 <> {} implies ( b

( f = f9 & B = B9 & b

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;

compatibility

for b_{1} being ManySortedSet of I1 holds

( b_{1} is MSUnTrans of f,A,B iff b_{1} is ManySortedFunction of A,B * f )

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

compatibility

for b

( b

proof 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 b_{6} being ManySortedSet of I1 holds

( b_{6} is MSUnTrans of f,A,B iff b_{6} is ManySortedFunction of A,B * f );

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

( b

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;

coherence

for b_{1} being MSUnTrans of f,A,B holds b_{1} is Function-yielding

end;
let f be Function of I1,I2;

let A be ManySortedSet of I1;

let B be ManySortedSet of I2;

coherence

for b

proof 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

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

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

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

for A being ManySortedSet of I1

for B being ManySortedSet of I2

for o being Element of I2 st B . o <> {} holds

for m being Element of B . o

for f being Function of I1,I2 st f = I1 --> o holds

{ [o9,((A . o9) --> m)] where o9 is Element of I1 : verum } is MSUnTrans of f,A,B

proof end;

theorem Th19: :: FUNCTOR0:19

for I1 being set

for I2, I3 being non empty set

for f being Function of I1,I2

for g being Function of I2,I3

for A being ManySortedSet of I1

for B being ManySortedSet of I2

for C being ManySortedSet of I3

for F being MSUnTrans of f,A,B

for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds

(C * (g * f)) . ii = {} ) holds

G ** F is MSUnTrans of g * f,A,C

for I2, I3 being non empty set

for f being Function of I1,I2

for g being Function of I2,I3

for A being ManySortedSet of I1

for B being ManySortedSet of I2

for C being ManySortedSet of I3

for F being MSUnTrans of f,A,B

for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds

(C * (g * f)) . ii = {} ) holds

G ** F is MSUnTrans of g * f,A,C

proof end;

definition

let C1, C2 be 1-sorted ;

attr c_{3} is strict ;

struct BimapStr over C1,C2 -> ;

aggr BimapStr(# ObjectMap #) -> BimapStr over C1,C2;

sel ObjectMap c_{3} -> bifunction of the carrier of C1, the carrier of C2;

end;
attr c

struct BimapStr over C1,C2 -> ;

aggr BimapStr(# ObjectMap #) -> BimapStr over C1,C2;

sel ObjectMap c

definition

let C1, C2 be non empty AltGraph ;

let F be BimapStr over C1,C2;

let o be Object of C1;

coherence

( the ObjectMap of F . (o,o)) `1 is Object of C2 by MCART_1:10;

end;
let F be BimapStr over C1,C2;

let o be Object of C1;

coherence

( the ObjectMap of F . (o,o)) `1 is Object of C2 by MCART_1:10;

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

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;

end;
let F be BimapStr over A,B;

attr F is reflexive means :: FUNCTOR0:def 8

the ObjectMap of F .: (id the carrier of A) c= id the carrier of B;

the ObjectMap of F .: (id the carrier of A) c= id the carrier of B;

attr F is coreflexive means :: FUNCTOR0:def 9

id the carrier of B c= the ObjectMap of F .: (id the carrier of A);

id the carrier of B c= the ObjectMap of F .: (id the carrier of A);

:: deftheorem defines one-to-one FUNCTOR0:def 6 :

for A, B being 1-sorted

for F being BimapStr over A,B holds

( F is one-to-one iff the ObjectMap of F is one-to-one );

for A, B being 1-sorted

for F being BimapStr over A,B holds

( F is one-to-one iff the ObjectMap of F is one-to-one );

:: deftheorem defines onto FUNCTOR0:def 7 :

for A, B being 1-sorted

for F being BimapStr over A,B holds

( F is onto iff the ObjectMap of F is onto );

for A, B being 1-sorted

for F being BimapStr over A,B holds

( F is onto iff the ObjectMap of F is onto );

:: deftheorem defines reflexive FUNCTOR0:def 8 :

for A, B being 1-sorted

for F being BimapStr over A,B holds

( F is reflexive iff the ObjectMap of F .: (id the carrier of A) c= id the carrier of B );

for A, B being 1-sorted

for F being BimapStr over A,B holds

( F is reflexive iff the ObjectMap of F .: (id the carrier of A) c= id the carrier of B );

:: deftheorem defines coreflexive FUNCTOR0:def 9 :

for A, B being 1-sorted

for F being BimapStr over A,B holds

( F is coreflexive iff id the carrier of B c= the ObjectMap of F .: (id the carrier of A) );

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;

( F is reflexive iff for o being Object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)] )

end;
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 for o being Object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)];

( F is reflexive iff for o being Object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)] )

proof 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)] );

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

for F being BimapStr over A,B st F is coreflexive holds

for o being Object of B ex o9 being Object of A st F . o9 = o

proof end;

:: 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)) <> {} );

for C1, C2 being non empty AltGraph

for F being BimapStr over C1,C2 holds

( F is feasible iff for o1, o2 being Object of C1 st <^o1,o2^> <> {} holds

the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {} );

definition

let C1, C2 be AltGraph ;

attr c_{3} is strict ;

struct FunctorStr over C1,C2 -> BimapStr over C1,C2;

aggr FunctorStr(# ObjectMap, MorphMap #) -> FunctorStr over C1,C2;

sel MorphMap c_{3} -> MSUnTrans of the ObjectMap of c_{3}, the Arrows of C1, the Arrows of C2;

end;
attr c

struct FunctorStr over C1,C2 -> BimapStr over C1,C2;

aggr FunctorStr(# ObjectMap, MorphMap #) -> FunctorStr over C1,C2;

sel MorphMap c

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

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

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 ;

existence

ex b_{1} being FunctorStr over C1,C2 st b_{1} is Covariant

ex b_{1} being FunctorStr over C1,C2 st b_{1} is Contravariant

end;
existence

ex b

proof end;

existence ex b

proof end;

definition

let C1, C2 be AltGraph ;

let F be FunctorStr over C1,C2;

let o1, o2 be Object of C1;

correctness

coherence

the MorphMap of F . (o1,o2) is set ;

;

end;
let F be FunctorStr over C1,C2;

let o1, o2 be Object of C1;

correctness

coherence

the MorphMap of F . (o1,o2) is set ;

;

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

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;

coherence

( Morph-Map (F,o1,o2) is Relation-like & Morph-Map (F,o1,o2) is Function-like ) ;

end;
let F be FunctorStr over C1,C2;

let o1, o2 be Object of C1;

coherence

( Morph-Map (F,o1,o2) is Relation-like & Morph-Map (F,o1,o2) is Function-like ) ;

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

end;
let F be Covariant FunctorStr over C1,C2;

let o1, o2 be Object of C1;

:: original: Morph-Map

redefine func Morph-Map (F,o1,o2) -> Function of <^o1,o2^>,<^(F . o1),(F . o2)^>;

coherence

Morph-Map (F,o1,o2) is Function of <^o1,o2^>,<^(F . o1),(F . o2)^>

proof end;

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;

(Morph-Map (F,o1,o2)) . m is Morphism of (F . o1),(F . o2)

end;
let F be Covariant FunctorStr over C1,C2;

let o1, o2 be Object of C1;

assume that

A1: <^o1,o2^> <> {} and

A2: <^(F . o1),(F . o2)^> <> {} ;

let m be Morphism of o1,o2;

func F . m -> Morphism of (F . o1),(F . o2) equals :Def15: :: FUNCTOR0:def 15

(Morph-Map (F,o1,o2)) . m;

coherence (Morph-Map (F,o1,o2)) . m;

(Morph-Map (F,o1,o2)) . m is Morphism of (F . o1),(F . o2)

proof end;

:: deftheorem Def15 defines . FUNCTOR0:def 15 :

for C1, C2 being non empty AltGraph

for F being Covariant FunctorStr over C1,C2

for o1, o2 being Object of C1 st <^o1,o2^> <> {} & <^(F . o1),(F . o2)^> <> {} holds

for m being Morphism of o1,o2 holds F . m = (Morph-Map (F,o1,o2)) . m;

for C1, C2 being non empty AltGraph

for F being Covariant FunctorStr over C1,C2

for o1, o2 being Object of C1 st <^o1,o2^> <> {} & <^(F . o1),(F . o2)^> <> {} holds

for m being Morphism of o1,o2 holds F . m = (Morph-Map (F,o1,o2)) . m;

definition

let C1, C2 be non empty AltGraph ;

let F be Contravariant FunctorStr over C1,C2;

let o1, o2 be Object of C1;

:: original: Morph-Map

redefine func Morph-Map (F,o1,o2) -> Function of <^o1,o2^>,<^(F . o2),(F . o1)^>;

coherence

Morph-Map (F,o1,o2) is Function of <^o1,o2^>,<^(F . o2),(F . o1)^>

end;
let F be Contravariant FunctorStr over C1,C2;

let o1, o2 be Object of C1;

:: original: Morph-Map

redefine func Morph-Map (F,o1,o2) -> Function of <^o1,o2^>,<^(F . o2),(F . o1)^>;

coherence

Morph-Map (F,o1,o2) is Function of <^o1,o2^>,<^(F . o2),(F . o1)^>

proof end;

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;

(Morph-Map (F,o1,o2)) . m is Morphism of (F . o2),(F . o1)

end;
let F be Contravariant FunctorStr over C1,C2;

let o1, o2 be Object of C1;

assume that

A1: <^o1,o2^> <> {} and

A2: <^(F . o2),(F . o1)^> <> {} ;

let m be Morphism of o1,o2;

func F . m -> Morphism of (F . o2),(F . o1) equals :Def16: :: FUNCTOR0:def 16

(Morph-Map (F,o1,o2)) . m;

coherence (Morph-Map (F,o1,o2)) . m;

(Morph-Map (F,o1,o2)) . m is Morphism of (F . o2),(F . o1)

proof end;

:: deftheorem Def16 defines . FUNCTOR0:def 16 :

for C1, C2 being non empty AltGraph

for F being Contravariant FunctorStr over C1,C2

for o1, o2 being Object of C1 st <^o1,o2^> <> {} & <^(F . o2),(F . o1)^> <> {} holds

for m being Morphism of o1,o2 holds F . m = (Morph-Map (F,o1,o2)) . m;

for C1, C2 being non empty AltGraph

for F being Contravariant FunctorStr over C1,C2

for o1, o2 being Object of C1 st <^o1,o2^> <> {} & <^(F . o2),(F . o1)^> <> {} holds

for m being Morphism of o1,o2 holds F . m = (Morph-Map (F,o1,o2)) . m;

definition

let C1, C2 be non empty AltGraph ;

let o be Object of C2;

assume A1: <^o,o^> <> {} ;

let m be Morphism of o,o;

ex b_{1} being strict FunctorStr over C1,C2 st

( the ObjectMap of b_{1} = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b_{1} = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is Object of C1 : verum } )

for b_{1}, b_{2} being strict FunctorStr over C1,C2 st the ObjectMap of b_{1} = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b_{1} = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is Object of C1 : verum } & the ObjectMap of b_{2} = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b_{2} = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is Object of C1 : verum } holds

b_{1} = b_{2}
;

end;
let o be Object of C2;

assume A1: <^o,o^> <> {} ;

let m be Morphism of o,o;

func C1 --> m -> strict FunctorStr over C1,C2 means :Def17: :: FUNCTOR0:def 17

( the ObjectMap of it = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of it = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is Object of C1 : verum } );

existence ( 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 } );

ex b

( the ObjectMap of b

proof end;

uniqueness for b

b

:: 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 b_{5} being strict FunctorStr over C1,C2 holds

( b_{5} = C1 --> m iff ( the ObjectMap of b_{5} = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b_{5} = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is Object of C1 : verum } ) );

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

( b

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

for o2 being Object of C2 st <^o2,o2^> <> {} holds

for m being Morphism of o2,o2

for o1 being Object of C1 holds (C1 --> m) . o1 = o2

proof end;

registration

let C1 be non empty AltGraph ;

let C2 be non empty reflexive AltGraph ;

let o be Object of C2;

let m be Morphism of o,o;

coherence

( C1 --> m is Covariant & C1 --> m is Contravariant & C1 --> m is feasible )

end;
let C2 be non empty reflexive AltGraph ;

let o be Object of C2;

let m be Morphism of o,o;

coherence

( C1 --> m is Covariant & C1 --> m is Contravariant & C1 --> m is feasible )

proof end;

registration

let C1 be non empty AltGraph ;

let C2 be non empty reflexive AltGraph ;

existence

ex b_{1} being FunctorStr over C1,C2 st

( b_{1} is feasible & b_{1} is Covariant & b_{1} is Contravariant )

end;
let C2 be non empty reflexive AltGraph ;

existence

ex b

( b

proof 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)]

for F being Covariant FunctorStr over C1,C2

for o1, o2 being Object of C1 holds the ObjectMap of F . (o1,o2) = [(F . o1),(F . o2)]

proof end;

definition

let C1, C2 be non empty AltGraph ;

let F be Covariant FunctorStr over C1,C2;

( F is feasible iff for o1, o2 being Object of C1 st <^o1,o2^> <> {} holds

<^(F . o1),(F . o2)^> <> {} )

end;
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 for o1, o2 being Object of C1 st <^o1,o2^> <> {} holds

<^(F . o1),(F . o2)^> <> {} ;

( F is feasible iff for o1, o2 being Object of C1 st <^o1,o2^> <> {} holds

<^(F . o1),(F . o2)^> <> {} )

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

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)]

for F being Contravariant FunctorStr over C1,C2

for o1, o2 being Object of C1 holds the ObjectMap of F . (o1,o2) = [(F . o2),(F . o1)]

proof end;

definition

let C1, C2 be non empty AltGraph ;

let F be Contravariant FunctorStr over C1,C2;

( F is feasible iff for o1, o2 being Object of C1 st <^o1,o2^> <> {} holds

<^(F . o2),(F . o1)^> <> {} )

end;
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 for o1, o2 being Object of C1 st <^o1,o2^> <> {} holds

<^(F . o2),(F . o1)^> <> {} ;

( F is feasible iff for o1, o2 being Object of C1 st <^o1,o2^> <> {} holds

<^(F . o2),(F . o1)^> <> {} )

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

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;

coherence

the MorphMap of F is Function-yielding ;

end;
let F be FunctorStr over C1,C2;

coherence

the MorphMap of F is Function-yielding ;

registration
end;

:: Wlasnosci funktorow, Semadeni-Wiweger str. 32

definition

let C1, C2 be non empty with_units AltCatStr ;

let F be FunctorStr over C1,C2;

end;
let F be FunctorStr over C1,C2;

attr F is id-preserving means :Def20: :: FUNCTOR0:def 20

for o being Object of C1 holds (Morph-Map (F,o,o)) . (idm o) = idm (F . o);

for o being Object of C1 holds (Morph-Map (F,o,o)) . (idm o) = idm (F . o);

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

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

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

registration

let C1, C2 be non empty with_units AltCatStr ;

let o2 be Object of C2;

coherence

C1 --> (idm o2) is id-preserving

end;
let o2 be Object of C2;

coherence

C1 --> (idm o2) is id-preserving

proof end;

registration

let C1 be non empty AltGraph ;

let C2 be non empty reflexive AltGraph ;

let o2 be Object of C2;

let m be Morphism of o2,o2;

coherence

C1 --> m is reflexive

end;
let C2 be non empty reflexive AltGraph ;

let o2 be Object of C2;

let m be Morphism of o2,o2;

coherence

C1 --> m is reflexive

proof end;

registration

let C1 be non empty AltGraph ;

let C2 be non empty reflexive AltGraph ;

existence

ex b_{1} being FunctorStr over C1,C2 st

( b_{1} is feasible & b_{1} is reflexive )

end;
let C2 be non empty reflexive AltGraph ;

existence

ex b

( b

proof end;

registration

let C1, C2 be non empty with_units AltCatStr ;

existence

ex b_{1} being FunctorStr over C1,C2 st

( b_{1} is id-preserving & b_{1} is feasible & b_{1} is reflexive & b_{1} is strict )

end;
existence

ex b

( b

proof end;

definition

let C1, C2 be non empty AltCatStr ;

let F be FunctorStr over C1,C2;

end;
let F be FunctorStr over C1,C2;

attr F is comp-preserving means :: FUNCTOR0:def 21

for o1, o2, o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds

for f being Morphism of o1,o2

for g being Morphism of o2,o3 ex f9 being Morphism of (F . o1),(F . o2) ex g9 being Morphism of (F . o2),(F . o3) st

( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 );

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

:: deftheorem defines comp-preserving FUNCTOR0:def 21 :

for C1, C2 being non empty AltCatStr

for F being FunctorStr over C1,C2 holds

( F is comp-preserving iff for o1, o2, o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds

for f being Morphism of o1,o2

for g being Morphism of o2,o3 ex f9 being Morphism of (F . o1),(F . o2) ex g9 being Morphism of (F . o2),(F . o3) st

( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 ) );

for C1, C2 being non empty AltCatStr

for F being FunctorStr over C1,C2 holds

( F is comp-preserving iff for o1, o2, o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds

for f being Morphism of o1,o2

for g being Morphism of o2,o3 ex f9 being Morphism of (F . o1),(F . o2) ex g9 being Morphism of (F . o2),(F . o3) st

( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 ) );

definition

let C1, C2 be non empty AltCatStr ;

let F be FunctorStr over C1,C2;

end;
let F be FunctorStr over C1,C2;

attr F is comp-reversing means :: FUNCTOR0:def 22

for o1, o2, o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds

for f being Morphism of o1,o2

for g being Morphism of o2,o3 ex f9 being Morphism of (F . o2),(F . o1) ex g9 being Morphism of (F . o3),(F . o2) st

( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = f9 * g9 );

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

:: deftheorem defines comp-reversing FUNCTOR0:def 22 :

for C1, C2 being non empty AltCatStr

for F being FunctorStr over C1,C2 holds

( F is comp-reversing iff for o1, o2, o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds

for f being Morphism of o1,o2

for g being Morphism of o2,o3 ex f9 being Morphism of (F . o2),(F . o1) ex g9 being Morphism of (F . o3),(F . o2) st

( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = f9 * g9 ) );

for C1, C2 being non empty AltCatStr

for F being FunctorStr over C1,C2 holds

( F is comp-reversing iff for o1, o2, o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds

for f being Morphism of o1,o2

for g being Morphism of o2,o3 ex f9 being Morphism of (F . o2),(F . o1) ex g9 being Morphism of (F . o3),(F . o2) st

( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = f9 * g9 ) );

definition

let C1 be non empty transitive AltCatStr ;

let C2 be non empty reflexive AltCatStr ;

let F be feasible Covariant FunctorStr over C1,C2;

( 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) )

end;
let C2 be non empty reflexive AltCatStr ;

let F be feasible Covariant FunctorStr over C1,C2;

redefine attr F is comp-preserving means :: FUNCTOR0:def 23

for o1, o2, o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds

for f being Morphism of o1,o2

for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f);

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

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

:: deftheorem defines comp-preserving FUNCTOR0:def 23 :

for C1 being non empty transitive AltCatStr

for C2 being non empty reflexive AltCatStr

for F being feasible Covariant FunctorStr over C1,C2 holds

( F is comp-preserving iff for o1, o2, o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds

for f being Morphism of o1,o2

for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f) );

for C1 being non empty transitive AltCatStr

for C2 being non empty reflexive AltCatStr

for F being feasible Covariant FunctorStr over C1,C2 holds

( F is comp-preserving iff for o1, o2, o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds

for f being Morphism of o1,o2

for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f) );

definition

let C1 be non empty transitive AltCatStr ;

let C2 be non empty reflexive AltCatStr ;

let F be feasible Contravariant FunctorStr over C1,C2;

( 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) )

end;
let C2 be non empty reflexive AltCatStr ;

let F be feasible Contravariant FunctorStr over C1,C2;

redefine attr F is comp-reversing means :: FUNCTOR0:def 24

for o1, o2, o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds

for f being Morphism of o1,o2

for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g);

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

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

:: deftheorem defines comp-reversing FUNCTOR0:def 24 :

for C1 being non empty transitive AltCatStr

for C2 being non empty reflexive AltCatStr

for F being feasible Contravariant FunctorStr over C1,C2 holds

( F is comp-reversing iff for o1, o2, o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds

for f being Morphism of o1,o2

for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g) );

for C1 being non empty transitive AltCatStr

for C2 being non empty reflexive AltCatStr

for F being feasible Contravariant FunctorStr over C1,C2 holds

( F is comp-reversing iff for o1, o2, o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds

for f being Morphism of o1,o2

for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g) );

theorem Th25: :: FUNCTOR0:25

for C1 being non empty AltGraph

for C2 being non empty reflexive AltGraph

for o2 being Object of C2

for m being Morphism of o2,o2

for F being feasible Covariant FunctorStr over C1,C2 st F = C1 --> m holds

for o, o9 being Object of C1

for f being Morphism of o,o9 st <^o,o9^> <> {} holds

F . f = m

for C2 being non empty reflexive AltGraph

for o2 being Object of C2

for m being Morphism of o2,o2

for F being feasible Covariant FunctorStr over C1,C2 st F = C1 --> m holds

for o, o9 being Object of C1

for f being Morphism of o,o9 st <^o,o9^> <> {} holds

F . f = m

proof end;

theorem Th26: :: FUNCTOR0:26

for C1 being non empty AltGraph

for C2 being non empty reflexive AltGraph

for o2 being Object of C2

for m being Morphism of o2,o2

for o, o9 being Object of C1

for f being Morphism of o,o9 st <^o,o9^> <> {} holds

(C1 --> m) . f = m

for C2 being non empty reflexive AltGraph

for o2 being Object of C2

for m being Morphism of o2,o2

for o, o9 being Object of C1

for f being Morphism of o,o9 st <^o,o9^> <> {} holds

(C1 --> m) . f = m

proof end;

registration

let C1 be non empty transitive AltCatStr ;

let C2 be non empty with_units AltCatStr ;

let o be Object of C2;

coherence

( C1 --> (idm o) is comp-preserving & C1 --> (idm o) is comp-reversing )

end;
let C2 be non empty with_units AltCatStr ;

let o be Object of C2;

coherence

( C1 --> (idm o) is comp-preserving & C1 --> (idm o) is comp-reversing )

proof end;

definition

let C1 be non empty transitive with_units AltCatStr ;

let C2 be non empty with_units AltCatStr ;

ex b_{1} being FunctorStr over C1,C2 st

( b_{1} is feasible & b_{1} is id-preserving & ( ( b_{1} is Covariant & b_{1} is comp-preserving ) or ( b_{1} is Contravariant & b_{1} is comp-reversing ) ) )

end;
let C2 be non empty with_units AltCatStr ;

mode Functor of C1,C2 -> FunctorStr over C1,C2 means :Def25: :: FUNCTOR0:def 25

( it is feasible & it is id-preserving & ( ( it is Covariant & it is comp-preserving ) or ( it is Contravariant & it is comp-reversing ) ) );

existence ( it is feasible & it is id-preserving & ( ( it is Covariant & it is comp-preserving ) or ( it is Contravariant & it is comp-reversing ) ) );

ex b

( b

proof 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 b_{3} being FunctorStr over C1,C2 holds

( b_{3} is Functor of C1,C2 iff ( b_{3} is feasible & b_{3} is id-preserving & ( ( b_{3} is Covariant & b_{3} is comp-preserving ) or ( b_{3} is Contravariant & b_{3} is comp-reversing ) ) ) );

for C1 being non empty transitive with_units AltCatStr

for C2 being non empty with_units AltCatStr

for b

( b

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;

end;
let C2 be non empty with_units AltCatStr ;

let F be Functor of C1,C2;

attr F is contravariant means :Def27: :: FUNCTOR0:def 27

( F is Contravariant & F is comp-reversing );

( F is Contravariant & F is comp-reversing );

:: deftheorem Def26 defines covariant FUNCTOR0:def 26 :

for C1 being non empty transitive with_units AltCatStr

for C2 being non empty with_units AltCatStr

for F being Functor of C1,C2 holds

( F is covariant iff ( F is Covariant & F is comp-preserving ) );

for C1 being non empty transitive with_units AltCatStr

for C2 being non empty with_units AltCatStr

for F being Functor of C1,C2 holds

( F is covariant iff ( F is Covariant & F is comp-preserving ) );

:: deftheorem Def27 defines contravariant FUNCTOR0:def 27 :

for C1 being non empty transitive with_units AltCatStr

for C2 being non empty with_units AltCatStr

for F being Functor of C1,C2 holds

( F is contravariant iff ( F is Contravariant & F is comp-reversing ) );

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;

ex b_{1} being strict FunctorStr over B,A st

( the ObjectMap of b_{1} = id [: the carrier of B, the carrier of B:] & the MorphMap of b_{1} = id the Arrows of B )

uniqueness

for b_{1}, b_{2} being strict FunctorStr over B,A st the ObjectMap of b_{1} = id [: the carrier of B, the carrier of B:] & the MorphMap of b_{1} = id the Arrows of B & the ObjectMap of b_{2} = id [: the carrier of B, the carrier of B:] & the MorphMap of b_{2} = id the Arrows of B holds

b_{1} = b_{2};

;

end;
let B be SubCatStr of A;

func incl B -> strict FunctorStr over B,A means :Def28: :: FUNCTOR0:def 28

( the ObjectMap of it = id [: the carrier of B, the carrier of B:] & the MorphMap of it = id the Arrows of B );

existence ( the ObjectMap of it = id [: the carrier of B, the carrier of B:] & the MorphMap of it = id the Arrows of B );

ex b

( the ObjectMap of b

proof end;

correctness uniqueness

for b

b

;

:: deftheorem Def28 defines incl FUNCTOR0:def 28 :

for A being AltCatStr

for B being SubCatStr of A

for b_{3} being strict FunctorStr over B,A holds

( b_{3} = incl B iff ( the ObjectMap of b_{3} = id [: the carrier of B, the carrier of B:] & the MorphMap of b_{3} = id the Arrows of B ) );

for A being AltCatStr

for B being SubCatStr of A

for b

( b

definition

let A be AltGraph ;

ex b_{1} being strict FunctorStr over A,A st

( the ObjectMap of b_{1} = id [: the carrier of A, the carrier of A:] & the MorphMap of b_{1} = id the Arrows of A )

uniqueness

for b_{1}, b_{2} being strict FunctorStr over A,A st the ObjectMap of b_{1} = id [: the carrier of A, the carrier of A:] & the MorphMap of b_{1} = id the Arrows of A & the ObjectMap of b_{2} = id [: the carrier of A, the carrier of A:] & the MorphMap of b_{2} = id the Arrows of A holds

b_{1} = b_{2};

;

end;
func id A -> strict FunctorStr over A,A means :Def29: :: FUNCTOR0:def 29

( the ObjectMap of it = id [: the carrier of A, the carrier of A:] & the MorphMap of it = id the Arrows of A );

existence ( the ObjectMap of it = id [: the carrier of A, the carrier of A:] & the MorphMap of it = id the Arrows of A );

ex b

( the ObjectMap of b

proof end;

correctness uniqueness

for b

b

;

:: deftheorem Def29 defines id FUNCTOR0:def 29 :

for A being AltGraph

for b_{2} being strict FunctorStr over A,A holds

( b_{2} = id A iff ( the ObjectMap of b_{2} = id [: the carrier of A, the carrier of A:] & the MorphMap of b_{2} = id the Arrows of A ) );

for A being AltGraph

for b

( b

registration
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

for B being non empty SubCatStr of A

for o being Object of B holds (incl B) . o = o

proof end;

theorem Th28: :: FUNCTOR0:28

for A being non empty AltCatStr

for B being non empty SubCatStr of A

for o1, o2 being Object of B holds <^o1,o2^> c= <^((incl B) . o1),((incl B) . o2)^>

for B being non empty SubCatStr of A

for o1, o2 being Object of B holds <^o1,o2^> c= <^((incl B) . o1),((incl B) . o2)^>

proof end;

registration

let A be non empty AltCatStr ;

let B be non empty SubCatStr of A;

coherence

incl B is feasible by Th28, XBOOLE_1:3;

end;
let B be non empty SubCatStr of A;

coherence

incl B is feasible by Th28, XBOOLE_1:3;

:: deftheorem defines faithful FUNCTOR0:def 30 :

for A, B being AltGraph

for F being FunctorStr over A,B holds

( F is faithful iff the MorphMap of F is "1-1" );

for A, B being AltGraph

for F being FunctorStr over A,B holds

( F is faithful iff the MorphMap of F is "1-1" );

:: deftheorem defines full FUNCTOR0:def 31 :

for A, B being AltGraph

for F being FunctorStr over A,B holds

( F is full iff ex B9 being ManySortedSet of [: the carrier of A, the carrier of A:] ex f being ManySortedFunction of the Arrows of A,B9 st

( B9 = the Arrows of B * the ObjectMap of F & f = the MorphMap of F & f is "onto" ) );

for A, B being AltGraph

for F being FunctorStr over A,B holds

( F is full iff ex B9 being ManySortedSet of [: the carrier of A, the carrier of A:] ex f being ManySortedFunction of the Arrows of A,B9 st

( B9 = the Arrows of B * the ObjectMap of F & f = the MorphMap of F & f is "onto" ) );

definition

let A be AltGraph ;

let B be non empty AltGraph ;

let F be FunctorStr over A,B;

( F is full iff ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st

( f = the MorphMap of F & f is "onto" ) ) ;

end;
let B be non empty AltGraph ;

let F be FunctorStr over A,B;

redefine attr F is full means :: FUNCTOR0:def 32

ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st

( f = the MorphMap of F & f is "onto" );

compatibility 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" );

( 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" ) ) ;

:: deftheorem defines full FUNCTOR0:def 32 :

for A being AltGraph

for B being non empty AltGraph

for F being FunctorStr over A,B holds

( F is full iff ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st

( f = the MorphMap of F & f is "onto" ) );

for A being AltGraph

for B being non empty AltGraph

for F being FunctorStr over A,B holds

( F is full iff ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st

( f = the MorphMap of F & f is "onto" ) );

:: deftheorem defines injective FUNCTOR0:def 33 :

for A, B being AltGraph

for F being FunctorStr over A,B holds

( F is injective iff ( F is one-to-one & F is faithful ) );

for A, B being AltGraph

for F being FunctorStr over A,B holds

( F is injective iff ( F is one-to-one & F is faithful ) );

:: deftheorem defines surjective FUNCTOR0:def 34 :

for A, B being AltGraph

for F being FunctorStr over A,B holds

( F is surjective iff ( F is full & F is onto ) );

for A, B being AltGraph

for F being FunctorStr over A,B holds

( F is surjective iff ( F is full & F is onto ) );

:: deftheorem defines bijective FUNCTOR0:def 35 :

for A, B being AltGraph

for F being FunctorStr over A,B holds

( F is bijective iff ( F is injective & F is surjective ) );

for A, B being AltGraph

for F being FunctorStr over A,B holds

( F is bijective iff ( F is injective & F is surjective ) );

registration

let A, B be non empty transitive with_units AltCatStr ;

existence

ex b_{1} being Functor of A,B st

( b_{1} is strict & b_{1} is covariant & b_{1} is contravariant & b_{1} is feasible )

end;
existence

ex b

( b

proof end;

theorem Th30: :: FUNCTOR0:30

for A being non empty AltGraph

for o1, o2 being Object of A st <^o1,o2^> <> {} holds

for m being Morphism of o1,o2 holds (Morph-Map ((id A),o1,o2)) . m = m

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

registration

let A be non empty AltGraph ;

existence

ex b_{1} being FunctorStr over A,A st

( b_{1} is Covariant & b_{1} is feasible )

end;
existence

ex b

( b

proof 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

for o1, o2 being Object of A st <^o1,o2^> <> {} holds

for F being feasible Covariant FunctorStr over A,A st F = id A holds

for m being Morphism of o1,o2 holds F . m = m

proof end;

registration

let A be non empty transitive with_units AltCatStr ;

coherence

( id A is id-preserving & id A is comp-preserving )

end;
coherence

( id A is id-preserving & id A is comp-preserving )

proof 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;
:: 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;

registration
end;

definition

let C1 be non empty AltGraph ;

let C2, C3 be non empty reflexive AltGraph ;

let F be feasible FunctorStr over C1,C2;

let G be FunctorStr over C2,C3;

ex b_{1} being strict FunctorStr over C1,C3 st

( the ObjectMap of b_{1} = the ObjectMap of G * the ObjectMap of F & the MorphMap of b_{1} = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F )

uniqueness

for b_{1}, b_{2} being strict FunctorStr over C1,C3 st the ObjectMap of b_{1} = the ObjectMap of G * the ObjectMap of F & the MorphMap of b_{1} = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F & the ObjectMap of b_{2} = the ObjectMap of G * the ObjectMap of F & the MorphMap of b_{2} = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F holds

b_{1} = b_{2};

;

end;
let C2, C3 be non empty reflexive AltGraph ;

let F be feasible FunctorStr over C1,C2;

let G be FunctorStr over C2,C3;

func G * F -> strict FunctorStr over C1,C3 means :Def36: :: FUNCTOR0:def 36

( the ObjectMap of it = the ObjectMap of G * the ObjectMap of F & the MorphMap of it = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F );

existence ( 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 );

ex b

( the ObjectMap of b

proof end;

correctness uniqueness

for b

b

;

:: 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 b_{6} being strict FunctorStr over C1,C3 holds

( b_{6} = G * F iff ( the ObjectMap of b_{6} = the ObjectMap of G * the ObjectMap of F & the MorphMap of b_{6} = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F ) );

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 b

( b

registration

let C1 be non empty AltGraph ;

let C2, C3 be non empty reflexive AltGraph ;

let F be feasible Covariant FunctorStr over C1,C2;

let G be Covariant FunctorStr over C2,C3;

correctness

coherence

G * F is Covariant ;

end;
let C2, C3 be non empty reflexive AltGraph ;

let F be feasible Covariant FunctorStr over C1,C2;

let G be Covariant FunctorStr over C2,C3;

correctness

coherence

G * F is Covariant ;

proof end;

registration

let C1 be non empty AltGraph ;

let C2, C3 be non empty reflexive AltGraph ;

let F be feasible Contravariant FunctorStr over C1,C2;

let G be Covariant FunctorStr over C2,C3;

correctness

coherence

G * F is Contravariant ;

end;
let C2, C3 be non empty reflexive AltGraph ;

let F be feasible Contravariant FunctorStr over C1,C2;

let G be Covariant FunctorStr over C2,C3;

correctness

coherence

G * F is Contravariant ;

proof end;

registration

let C1 be non empty AltGraph ;

let C2, C3 be non empty reflexive AltGraph ;

let F be feasible Covariant FunctorStr over C1,C2;

let G be Contravariant FunctorStr over C2,C3;

correctness

coherence

G * F is Contravariant ;

end;
let C2, C3 be non empty reflexive AltGraph ;

let F be feasible Covariant FunctorStr over C1,C2;

let G be Contravariant FunctorStr over C2,C3;

correctness

coherence

G * F is Contravariant ;

proof end;

registration

let C1 be non empty AltGraph ;

let C2, C3 be non empty reflexive AltGraph ;

let F be feasible Contravariant FunctorStr over C1,C2;

let G be Contravariant FunctorStr over C2,C3;

correctness

coherence

G * F is Covariant ;

end;
let C2, C3 be non empty reflexive AltGraph ;

let F be feasible Contravariant FunctorStr over C1,C2;

let G be Contravariant FunctorStr over C2,C3;

correctness

coherence

G * F is Covariant ;

proof end;

registration

let C1 be non empty AltGraph ;

let C2, C3 be non empty reflexive AltGraph ;

let F be feasible FunctorStr over C1,C2;

let G be feasible FunctorStr over C2,C3;

coherence

G * F is feasible

end;
let C2, C3 be non empty reflexive AltGraph ;

let F be feasible FunctorStr over C1,C2;

let G be feasible FunctorStr over C2,C3;

coherence

G * F is feasible

proof end;

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)

for C2, C3, C4 being non empty reflexive AltGraph

for F being feasible FunctorStr over C1,C2

for G being feasible FunctorStr over C2,C3

for H being FunctorStr over C3,C4 holds (H * G) * F = H * (G * F)

proof end;

theorem Th33: :: FUNCTOR0:33

for C1 being non empty AltCatStr

for C2, C3 being non empty reflexive AltCatStr

for F being reflexive feasible FunctorStr over C1,C2

for G being FunctorStr over C2,C3

for o being Object of C1 holds (G * F) . o = G . (F . o)

for C2, C3 being non empty reflexive AltCatStr

for F being reflexive feasible FunctorStr over C1,C2

for G being FunctorStr over C2,C3

for o being Object of C1 holds (G * F) . o = G . (F . o)

proof end;

theorem Th34: :: FUNCTOR0:34

for C1 being non empty AltGraph

for C2, C3 being non empty reflexive AltGraph

for F being reflexive feasible FunctorStr over C1,C2

for G being FunctorStr over C2,C3

for o being Object of C1 holds Morph-Map ((G * F),o,o) = (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o))

for C2, C3 being non empty reflexive AltGraph

for F being reflexive feasible FunctorStr over C1,C2

for G being FunctorStr over C2,C3

for o being Object of C1 holds Morph-Map ((G * F),o,o) = (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o))

proof end;

registration

let C1, C2, C3 be non empty with_units AltCatStr ;

let F be reflexive feasible id-preserving FunctorStr over C1,C2;

let G be id-preserving FunctorStr over C2,C3;

coherence

G * F is id-preserving

end;
let F be reflexive feasible id-preserving FunctorStr over C1,C2;

let G be id-preserving FunctorStr over C2,C3;

coherence

G * F is id-preserving

proof end;

definition

let A, C be non empty reflexive AltCatStr ;

let B be non empty SubCatStr of A;

let F be FunctorStr over A,C;

correctness

coherence

F * (incl B) is FunctorStr over B,C;

;

end;
let B be non empty SubCatStr of A;

let F be FunctorStr over A,C;

correctness

coherence

F * (incl B) is FunctorStr over B,C;

;

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

for A, C being non empty reflexive AltCatStr

for B being non empty SubCatStr of A

for F being FunctorStr over A,C holds F | B = F * (incl B);

definition

let A, B be non empty AltGraph ;

let F be FunctorStr over A,B;

assume A1: F is bijective ;

ex b_{1} being strict FunctorStr over B,A st

( the ObjectMap of b_{1} = 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_{1} = (f "") * ( the ObjectMap of F ") ) )

for b_{1}, b_{2} being strict FunctorStr over B,A st the ObjectMap of b_{1} = 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_{1} = (f "") * ( the ObjectMap of F ") ) & the ObjectMap of b_{2} = 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_{2} = (f "") * ( the ObjectMap of F ") ) holds

b_{1} = b_{2}
;

end;
let F be FunctorStr over A,B;

assume A1: F is bijective ;

func F " -> strict FunctorStr over B,A means :Def38: :: FUNCTOR0:def 38

( the ObjectMap of it = the ObjectMap of F " & ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st

( f = the MorphMap of F & the MorphMap of it = (f "") * ( the ObjectMap of F ") ) );

existence ( 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 ") ) );

ex b

( the ObjectMap of b

( f = the MorphMap of F & the MorphMap of b

proof end;

uniqueness for b

( f = the MorphMap of F & the MorphMap of b

( f = the MorphMap of F & the MorphMap of b

b

:: 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 b_{4} being strict FunctorStr over B,A holds

( b_{4} = F " iff ( the ObjectMap of b_{4} = 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_{4} = (f "") * ( the ObjectMap of F ") ) ) );

for A, B being non empty AltGraph

for F being FunctorStr over A,B st F is bijective holds

for b

( b

( f = the MorphMap of F & the MorphMap of b

theorem Th35: :: FUNCTOR0:35

for A, B being non empty transitive with_units AltCatStr

for F being feasible FunctorStr over A,B st F is bijective holds

( F " is bijective & F " is feasible )

for F being feasible FunctorStr over A,B st F is bijective holds

( F " is bijective & F " is feasible )

proof end;

theorem Th36: :: FUNCTOR0:36

for A, B being non empty transitive with_units AltCatStr

for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive holds

F " is reflexive

for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive holds

F " is reflexive

proof end;

theorem Th37: :: FUNCTOR0:37

for A, B being non empty transitive with_units AltCatStr

for F being reflexive feasible id-preserving FunctorStr over A,B st F is bijective & F is coreflexive holds

F " is id-preserving

for F being reflexive feasible id-preserving FunctorStr over A,B st F is bijective & F is coreflexive holds

F " is id-preserving

proof end;

theorem Th38: :: FUNCTOR0:38

for A, B being non empty transitive with_units AltCatStr

for F being feasible FunctorStr over A,B st F is bijective & F is Covariant holds

F " is Covariant

for F being feasible FunctorStr over A,B st F is bijective & F is Covariant holds

F " is Covariant

proof end;

theorem Th39: :: FUNCTOR0:39

for A, B being non empty transitive with_units AltCatStr

for F being feasible FunctorStr over A,B st F is bijective & F is Contravariant holds

F " is Contravariant

for F being feasible FunctorStr over A,B st F is bijective & F is Contravariant holds

F " is Contravariant

proof end;

theorem Th40: :: FUNCTOR0:40

for A, B being non empty transitive with_units AltCatStr

for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive & F is Covariant holds

for o1, o2 being Object of B

for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

(Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m

for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive & F is Covariant holds

for o1, o2 being Object of B

for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

(Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m

proof end;

theorem Th41: :: FUNCTOR0:41

for A, B being non empty transitive with_units AltCatStr

for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive & F is Contravariant holds

for o1, o2 being Object of B

for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

(Morph-Map (F,((F ") . o2),((F ") . o1))) . ((Morph-Map ((F "),o1,o2)) . m) = m

for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive & F is Contravariant holds

for o1, o2 being Object of B

for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

(Morph-Map (F,((F ") . o2),((F ") . o1))) . ((Morph-Map ((F "),o1,o2)) . m) = m

proof end;

theorem Th42: :: FUNCTOR0:42

for A, B being non empty transitive with_units AltCatStr

for F being reflexive feasible FunctorStr over A,B st F is bijective & F is comp-preserving & F is Covariant & F is coreflexive holds

F " is comp-preserving

for F being reflexive feasible FunctorStr over A,B st F is bijective & F is comp-preserving & F is Covariant & F is coreflexive holds

F " is comp-preserving

proof end;

theorem Th43: :: FUNCTOR0:43

for A, B being non empty transitive with_units AltCatStr

for F being reflexive feasible FunctorStr over A,B st F is bijective & F is comp-reversing & F is Contravariant & F is coreflexive holds

F " is comp-reversing

for F being reflexive feasible FunctorStr over A,B st F is bijective & F is comp-reversing & F is Contravariant & F is coreflexive holds

F " is comp-reversing

proof end;

registration

let C1 be 1-sorted ;

let C2 be non empty 1-sorted ;

coherence

for b_{1} being BimapStr over C1,C2 st b_{1} is Covariant holds

b_{1} is reflexive

end;
let C2 be non empty 1-sorted ;

coherence

for b

b

proof end;

registration

let C1 be 1-sorted ;

let C2 be non empty 1-sorted ;

coherence

for b_{1} being BimapStr over C1,C2 st b_{1} is Contravariant holds

b_{1} is reflexive

end;
let C2 be non empty 1-sorted ;

coherence

for b

b

proof end;

theorem Th44: :: FUNCTOR0:44

for C1, C2 being 1-sorted

for M being BimapStr over C1,C2 st M is Covariant & M is onto holds

M is coreflexive

for M being BimapStr over C1,C2 st M is Covariant & M is onto holds

M is coreflexive

proof end;

theorem Th45: :: FUNCTOR0:45

for C1, C2 being 1-sorted

for M being BimapStr over C1,C2 st M is Contravariant & M is onto holds

M is coreflexive

for M being BimapStr over C1,C2 st M is Contravariant & M is onto holds

M is coreflexive

proof end;

registration

let C1 be non empty transitive with_units AltCatStr ;

let C2 be non empty with_units AltCatStr ;

coherence

for b_{1} being Functor of C1,C2 st b_{1} is covariant holds

b_{1} is reflexive
;

end;
let C2 be non empty with_units AltCatStr ;

coherence

for b

b

registration

let C1 be non empty transitive with_units AltCatStr ;

let C2 be non empty with_units AltCatStr ;

coherence

for b_{1} being Functor of C1,C2 st b_{1} is contravariant holds

b_{1} is reflexive
;

end;
let C2 be non empty with_units AltCatStr ;

coherence

for b

b

theorem Th46: :: FUNCTOR0:46

for C1 being non empty transitive with_units AltCatStr

for C2 being non empty with_units AltCatStr

for F being Functor of C1,C2 st F is covariant & F is onto holds

F is coreflexive by Th44;

for C2 being non empty with_units AltCatStr

for F being Functor of C1,C2 st F is covariant & F is onto holds

F is coreflexive by Th44;

theorem Th47: :: FUNCTOR0:47

for C1 being non empty transitive with_units AltCatStr

for C2 being non empty with_units AltCatStr

for F being Functor of C1,C2 st F is contravariant & F is onto holds

F is coreflexive by Th45;

for C2 being non empty with_units AltCatStr

for F being Functor of C1,C2 st F is contravariant & F is onto holds

F is coreflexive by Th45;

theorem Th48: :: FUNCTOR0:48

for A, B being non empty transitive with_units AltCatStr

for F being covariant Functor of A,B st F is bijective holds

ex G being Functor of B,A st

( G = F " & G is bijective & G is covariant )

for F being covariant Functor of A,B st F is bijective holds

ex G being Functor of B,A st

( G = F " & G is bijective & G is covariant )

proof end;

theorem Th49: :: FUNCTOR0:49

for A, B being non empty transitive with_units AltCatStr

for F being contravariant Functor of A,B st F is bijective holds

ex G being Functor of B,A st

( G = F " & G is bijective & G is contravariant )

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 ;

for A being non empty transitive with_units AltCatStr ex F being Functor of A,A st

( F is bijective & F is covariant )

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 )

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 )

end;
pred A,B are_isomorphic means :: FUNCTOR0:def 39

ex F being Functor of A,B st

( F is bijective & F is covariant );

reflexivity ex F being Functor of A,B st

( F is bijective & F is covariant );

for A being non empty transitive with_units AltCatStr ex F being Functor of A,A st

( F is bijective & F is covariant )

proof end;

symmetry for A, B being non empty transitive with_units AltCatStr st ex F being Functor of A,B st

( F is bijective & F is covariant ) holds

ex F being Functor of B,A st

( F is bijective & F is covariant )

proof end;

pred A,B are_anti-isomorphic means :: FUNCTOR0:def 40

ex F being Functor of A,B st

( F is bijective & F is contravariant );

symmetry ex F being Functor of A,B st

( F is bijective & F is contravariant );

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;

:: deftheorem defines are_isomorphic FUNCTOR0:def 39 :

for A, B being non empty transitive with_units AltCatStr holds

( A,B are_isomorphic iff ex F being Functor of A,B st

( F is bijective & F is covariant ) );

for A, B being non empty transitive with_units AltCatStr holds

( A,B are_isomorphic iff ex F being Functor of A,B st

( F is bijective & F is covariant ) );

:: deftheorem defines are_anti-isomorphic FUNCTOR0:def 40 :

for A, B being non empty transitive with_units AltCatStr holds

( A,B are_anti-isomorphic iff ex F being Functor of A,B st

( F is bijective & F is contravariant ) );

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