Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users

### Functors for Alternative Categories

by
Andrzej Trybulec

MML identifier: FUNCTOR0
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, MCART_1, BOOLE, RELAT_1, PBOOLE, SGRAPH1, PRALG_1,
FUNCOP_1, MSUALG_3, CAT_4, ALTCAT_1, RELAT_2, MSUALG_6, CAT_1, ALTCAT_2,
FUNCT_3, ENS_1, WELLORD1, FUNCTOR0;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, MCART_1,
FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, FUNCT_3, FUNCT_4, PBOOLE,
STRUCT_0, PRALG_1, MSUALG_1, MSUALG_3, ALTCAT_1, ALTCAT_2;
constructors ALTCAT_2, MCART_1;
clusters RELAT_1, FUNCT_1, ALTCAT_1, ALTCAT_2, MSUALG_1, STRUCT_0, PRALG_1,
RELSET_1, SUBSET_1, FUNCT_2;
requirements SUBSET, BOOLE;

begin :: Preliminaries

scheme ValOnPair
{X()-> non empty set,f()-> Function,
x1,x2()-> Element of X(), F(set,set)-> set, P[set,set]}:
f().(x1(),x2()) = F(x1(),x2())
provided
f() = { [[o,o'],F(o,o')]
where o is Element of X(), o' is Element of X(): P[o,o'] } and
P[x1(),x2()];

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

canceled;

theorem :: FUNCTOR0:3
for I being set for M being ManySortedSet of I holds M*id I = M;

definition let f be empty Function;
cluster ~f -> empty;
let g be Function;
cluster [:f,g:] -> empty;
cluster [:g,f:] -> empty;
end;

theorem :: FUNCTOR0:4
for A being set, f being Function holds f.:id A = (~f).:id A;

theorem :: FUNCTOR0:5
for X,Y being set, f being Function of X,Y holds
f is onto iff [:f,f:] is onto;

definition let f be Function-yielding Function;
cluster ~f -> Function-yielding;
end;

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

theorem :: FUNCTOR0:7
for f,g being Function st f is one-to-one & g is one-to-one holds
[:f,g:]" = [:f",g":];

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

theorem :: FUNCTOR0:9
for f being Function st f is one-to-one
holds ~f is one-to-one;

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

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

theorem :: FUNCTOR0:12
for A,B be set, f being Function of A,B st f is onto
holds id B c= [:f,f:].:id A;

theorem :: FUNCTOR0:13
for F,G being Function-yielding Function, f be Function
holds (G**F)*f = (G*f)**(F*f);

definition let A,B,C be set, f be Function of [:A,B:],C;
redefine func ~f -> Function of [:B,A:],C;
end;

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

theorem :: FUNCTOR0:15
for A be set, B being non empty set, f being Function of A,B
holds [:f,f:].:id A c= id B;

begin :: Functions bewteen Cartesian products

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

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

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

definition let A,B be set;
cluster Covariant Contravariant bifunction of A,B;
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];

begin :: Unary transformatiom

definition let I1,I2 be set, f be Function of I1,I2;
let A be ManySortedSet of I1, B be ManySortedSet of I2;
mode MSUnTrans of f,A,B -> ManySortedSet of I1 means
:: FUNCTOR0:def 4
ex I2' being non empty set, B' being ManySortedSet of I2',
f' being Function of I1,I2' st f = f' & B = B' &
it is ManySortedFunction of A,B'*f' if I2 <> {}
otherwise it = I1;
end;

definition let I1 be set, I2 be non empty set, f be Function of I1,I2;
let A be ManySortedSet of I1, B be ManySortedSet of I2;
redefine mode MSUnTrans of f,A,B means
:: FUNCTOR0:def 5
it is ManySortedFunction of A,B*f;
end;

definition let I1,I2 be set; let f be Function of I1,I2;
let A be ManySortedSet of I1, B be ManySortedSet of I2;
cluster -> Function-yielding MSUnTrans of f,A,B;
end;

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

definition let I1 be set, I2 be non empty set,
f be Function of I1,I2,
A be ManySortedSet of [:I1,I1:], B be ManySortedSet of [:I2,I2:],
F be MSUnTrans of [:f,f:],A,B;
redefine func ~F -> MSUnTrans of [:f,f:],~A,~B;
end;

theorem :: FUNCTOR0:19
for I1,I2 being non empty set,
A being ManySortedSet of I1, B being ManySortedSet of I2,
o being Element of I2 st B.o <> {}
for m being Element of B.o, f being Function of I1,I2 st f = I1 --> o
holds
{ [o',A.o' --> m] where o' is Element of I1: not contradiction }
is MSUnTrans of f,A,B;

theorem :: FUNCTOR0:20
for I1 being set, I2,I3 being non empty set,
f being Function of I1,I2, g being Function of I2,I3,
A being ManySortedSet of I1, B being ManySortedSet of I2,
C being ManySortedSet of I3, F being MSUnTrans of f,A,B,
G being MSUnTrans of g*f,B*f,C
st for ii being set st ii in I1 & (B*f).ii = {}
holds A.ii = {} or (C*(g*f)).ii = {}
holds G**(F qua Function-yielding Function) is MSUnTrans of g*f,A,C;

begin :: Functors

definition let C1,C2 be 1-sorted;
struct BimapStr over C1,C2
(#ObjectMap -> bifunction of the carrier of C1, the carrier of C2 #);
end;

definition let C1,C2 be non empty AltGraph;
let F be BimapStr over C1,C2; let o be object of C1;
func F.o -> object of C2 equals
:: FUNCTOR0:def 6
((the ObjectMap of F).(o,o))`1;
end;

definition let A,B be 1-sorted, F be BimapStr over A,B;
attr F is one-to-one means
:: FUNCTOR0:def 7
the ObjectMap of F is one-to-one;
attr F is onto means
:: FUNCTOR0:def 8
the ObjectMap of F is onto;
attr F is reflexive means
:: FUNCTOR0:def 9

(the ObjectMap of F).:id the carrier of A c= id the carrier of B;
attr F is coreflexive means
:: FUNCTOR0:def 10

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

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

theorem :: FUNCTOR0:21
for A,B being reflexive non empty AltGraph,
F being BimapStr over A,B st F is coreflexive
for o being object of B
ex o' being object of A st F.o' = o;

definition let C1, C2 be non empty AltGraph;
let F be BimapStr over C1,C2;
attr F is feasible means
:: 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;

definition let C1,C2 be AltGraph;
struct(BimapStr over C1,C2) FunctorStr over C1,C2
(#ObjectMap -> bifunction of the carrier of C1,the carrier of C2,
MorphMap ->
MSUnTrans of the ObjectMap, the Arrows of C1, the Arrows of C2 #);
end;

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

definition let C1,C2 be AltGraph;
cluster Covariant FunctorStr over C1,C2;
cluster Contravariant FunctorStr over C1,C2;
end;

definition let C1,C2 be AltGraph;
let F be FunctorStr over C1,C2; let o1,o2 be object of C1;
func Morph-Map(F,o1,o2) equals
:: FUNCTOR0:def 15

(the MorphMap of F).(o1,o2);
end;

definition let C1,C2 be AltGraph;
let F be FunctorStr over C1,C2; let o1,o2 be object of C1;
cluster Morph-Map(F,o1,o2) -> Relation-like Function-like;
end;

definition let C1,C2 be non empty AltGraph;
let F be Covariant FunctorStr over C1,C2; let o1,o2 be object of C1;
redefine func Morph-Map(F,o1,o2) -> Function of <^o1,o2^>, <^F.o1,F.o2^>;
end;

definition let C1,C2 be non empty AltGraph;
let F be Covariant FunctorStr over C1,C2; let o1,o2 be object of C1 such that
<^o1,o2^> <> {} & <^F.o1,F.o2^> <> {};
let m be Morphism of o1,o2;
func F.m -> Morphism of F.o1, F.o2 equals
:: FUNCTOR0:def 16
Morph-Map(F,o1,o2).m;
end;

definition let C1,C2 be non empty AltGraph;
let F be Contravariant FunctorStr over C1,C2; let o1,o2 be object of C1;
redefine func Morph-Map(F,o1,o2) -> Function of <^o1,o2^>, <^F.o2,F.o1^>;
end;

definition let C1,C2 be non empty AltGraph;
let F be Contravariant FunctorStr over C1,C2;
let o1,o2 be object of C1 such that
<^o1,o2^> <> {} & <^F.o2,F.o1^> <> {};
let m be Morphism of o1,o2;
func F.m -> Morphism of F.o2, F.o1 equals
:: FUNCTOR0:def 17
Morph-Map(F,o1,o2).m;
end;

definition
let C1,C2 be non empty AltGraph;
let o be object of C2 such that
<^o,o^> <> {};
let m be Morphism of o,o;
func C1 --> m -> strict FunctorStr over C1,C2 means
:: 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 is object of C1, o2 is object of C1:
end;

theorem :: FUNCTOR0:22
for C1,C2 being non empty AltGraph, o2 being object of C2 st <^o2,o2^> <> {}
for m be Morphism of o2,o2, o1 being object of C1
holds (C1 --> m).o1 = o2;

definition
let C1 be non empty AltGraph, C2 be non empty reflexive AltGraph;
let o be object of C2, m be Morphism of o,o;
cluster C1 --> m -> Covariant Contravariant feasible;
end;

definition
let C1 be non empty AltGraph, C2 be non empty reflexive AltGraph;
cluster feasible Covariant Contravariant FunctorStr over C1,C2;
end;

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

definition let C1, C2 be non empty AltGraph;
let F be Covariant FunctorStr over C1,C2;
redefine attr F is feasible means
:: FUNCTOR0:def 19

for o1,o2 being object of C1 st <^o1,o2^> <> {} holds <^F.o1,F.o2^> <> {};
end;

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

definition let C1, C2 be non empty AltGraph;
let F be Contravariant FunctorStr over C1,C2;
redefine attr F is feasible means
:: FUNCTOR0:def 20

for o1,o2 being object of C1 st <^o1,o2^> <> {} holds <^F.o2,F.o1^> <> {};
end;

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

definition
cluster non empty reflexive AltCatStr;
end;

:: Wlasnosci funktorow, Semadeni-Wiweger str. 32

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

theorem :: FUNCTOR0:25
for C1,C2 being non empty AltGraph, o2 being object of C2 st <^o2,o2^> <> {}
for m be Morphism of o2,o2, o,o' being object of C1, f being Morphism of o,o'
st <^o,o'^> <> {}
holds Morph-Map(C1 --> m,o,o').f = m;

definition
cluster with_units -> reflexive (non empty AltCatStr);
end;

definition let C1,C2 be with_units (non empty AltCatStr);
let o2 be object of C2;
cluster C1 --> idm o2 -> id-preserving;
end;

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

definition let C1 be non empty AltGraph;
let C2 be non empty reflexive AltGraph;
cluster feasible reflexive FunctorStr over C1,C2;
end;

definition let C1,C2 be with_units (non empty AltCatStr);
cluster id-preserving feasible reflexive strict FunctorStr over C1,C2;
end;

definition let C1,C2 be non empty AltCatStr;
let F be FunctorStr over C1,C2;
attr F is comp-preserving means
:: FUNCTOR0:def 22
for o1,o2,o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {}
for f being Morphism of o1,o2, g being Morphism of o2,o3
ex f' being Morphism of F.o1,F.o2, g' being Morphism of F.o2,F.o3 st
f' = Morph-Map(F,o1,o2).f & g' = Morph-Map(F,o2,o3).g &
Morph-Map(F,o1,o3).(g*f) = g'*f';
end;

definition let C1,C2 be non empty AltCatStr;
let F be FunctorStr over C1,C2;
attr F is comp-reversing means
:: FUNCTOR0:def 23
for o1,o2,o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {}
for f being Morphism of o1,o2, g being Morphism of o2,o3
ex f' being Morphism of F.o2,F.o1, g' being Morphism of F.o3,F.o2 st
f' = Morph-Map(F,o1,o2).f & g' = Morph-Map(F,o2,o3).g &
Morph-Map(F,o1,o3).(g*f) = f'*g';
end;

definition let C1 be non empty transitive AltCatStr;
let C2 be non empty reflexive AltCatStr;
let F be Covariant feasible FunctorStr over 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^> <> {}
for f being Morphism of o1,o2, g being Morphism of o2,o3
holds F.(g*f) = (F.g)*(F.f);
end;

definition let C1 be non empty transitive AltCatStr;
let C2 be non empty reflexive AltCatStr;
let F be Contravariant feasible FunctorStr over 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^> <> {}
for f being Morphism of o1,o2, g being Morphism of o2,o3
holds F.(g*f) = (F.f)*(F.g);
end;

theorem :: FUNCTOR0:26
for C1 being non empty AltGraph, C2 being non empty reflexive AltGraph,
o2 being object of C2, m be Morphism of o2,o2,
F being Covariant feasible FunctorStr over C1,C2 st F = C1 --> m
for o,o' being object of C1, f being Morphism of o,o'
st <^o,o'^> <> {}
holds F.f = m;

theorem :: FUNCTOR0:27
for C1 being non empty AltGraph, C2 being non empty reflexive AltGraph,
o2 being object of C2, m be Morphism of o2,o2,
o,o' being object of C1, f being Morphism of o,o'
st <^o,o'^> <> {}
holds (C1 --> m).f = m;

definition
let C1 be non empty transitive AltCatStr,
C2 be with_units (non empty AltCatStr);
let o be object of C2;
cluster C1 --> idm o -> comp-preserving comp-reversing;
end;

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

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

definition let A be AltCatStr, B be SubCatStr of A;
func incl B -> strict FunctorStr over B,A means
:: 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;
end;

definition let A be AltGraph;
func id A -> strict FunctorStr over A,A means
:: 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;
end;

definition let A be AltCatStr, B be SubCatStr of A;
cluster incl B -> Covariant;
end;

theorem :: FUNCTOR0:28
for A being non empty AltCatStr, B being non empty SubCatStr of A,
o being object of B
holds (incl B).o = o;

theorem :: FUNCTOR0:29
for A being non empty AltCatStr, B being non empty SubCatStr of A,
o1,o2 being object of B
holds <^o1,o2^> c= <^(incl B).o1,(incl B).o2^>;

definition let A be non empty AltCatStr, B be non empty SubCatStr of A;
cluster incl B -> feasible;
end;

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

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

definition
let A be AltGraph, B be non empty AltGraph, F be FunctorStr over A,B;
redefine attr F is full means
:: 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";
end;

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

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

definition let A,B be transitive with_units (non empty AltCatStr);
cluster strict covariant contravariant feasible Functor of A,B;
end;

theorem :: FUNCTOR0:30
for A being non empty AltGraph, o being object of A
holds (id A).o = o;

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

definition let A be non empty AltGraph;
cluster id A -> feasible Covariant;
end;

definition let A be non empty AltGraph;
cluster Covariant feasible FunctorStr over A,A;
end;

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

definition let A be transitive with_units (non empty AltCatStr);
cluster id A -> id-preserving comp-preserving;
end;

definition let A be transitive with_units (non empty AltCatStr);
redefine func id A -> strict covariant Functor of A,A;
end;

definition let A be AltGraph;
cluster id A -> bijective;
end;

begin :: The composition of functors

definition
let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
let F be feasible FunctorStr over C1,C2, G be FunctorStr over C2,C3;
func G*F -> strict FunctorStr over C1,C3 means
:: 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;
end;

definition let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
let F be Covariant feasible FunctorStr over C1,C2,
G be Covariant FunctorStr over C2,C3;
cluster G*F -> Covariant;
end;

definition let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
let F be Contravariant feasible FunctorStr over C1,C2,
G be Covariant FunctorStr over C2,C3;
cluster G*F -> Contravariant;
end;

definition let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
let F be Covariant feasible FunctorStr over C1,C2,
G be Contravariant FunctorStr over C2,C3;
cluster G*F -> Contravariant;
end;

definition let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
let F be Contravariant feasible FunctorStr over C1,C2,
G be Contravariant FunctorStr over C2,C3;
cluster G*F -> Covariant;
end;

definition let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
let F be feasible FunctorStr over C1,C2,
G be feasible FunctorStr over C2,C3;
cluster G*F -> feasible;
end;

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

theorem :: FUNCTOR0:34
for C1 being non empty AltCatStr, C2,C3 being non empty reflexive AltCatStr,
F be feasible reflexive FunctorStr over C1,C2, G be FunctorStr over C2,C3,
o be object of C1
holds (G*F).o = G.(F.o);

theorem :: FUNCTOR0:35
for C1 being non empty AltGraph,
C2,C3 being non empty reflexive AltGraph,
F be feasible reflexive FunctorStr over C1,C2,
G be FunctorStr over C2,C3,
o be object of C1
holds Morph-Map(G*F,o,o) = Morph-Map(G,F.o,F.o)*Morph-Map(F,o,o);

definition let C1,C2,C3 be with_units (non empty AltCatStr);
let F be id-preserving feasible reflexive FunctorStr over C1,C2;
let G be id-preserving FunctorStr over C2,C3;
cluster G*F -> id-preserving;
end;

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

begin :: The inverse functor

definition let A,B be non empty AltGraph, F be FunctorStr over A,B;
assume
F is bijective;
func F" -> strict FunctorStr over B,A means
:: 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)";
end;

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

theorem :: FUNCTOR0:37
for A,B being transitive with_units (non empty AltCatStr),
F being feasible reflexive FunctorStr over A,B st
F is bijective coreflexive
holds F" is reflexive;

theorem :: FUNCTOR0:38
for A,B being transitive with_units (non empty AltCatStr),
F being feasible reflexive id-preserving FunctorStr over A,B
st F is bijective coreflexive
holds F" is id-preserving;

theorem :: FUNCTOR0:39
for A,B being transitive with_units (non empty AltCatStr),
F being feasible FunctorStr over A,B st F is bijective Covariant
holds F" is Covariant;

theorem :: FUNCTOR0:40
for A,B being transitive with_units (non empty AltCatStr),
F being feasible FunctorStr over A,B st F is bijective Contravariant
holds F" is Contravariant;

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

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

theorem :: FUNCTOR0:43
for A,B being transitive with_units (non empty AltCatStr),
F being feasible reflexive FunctorStr over A,B st
F is bijective comp-preserving Covariant coreflexive
holds F" is comp-preserving;

theorem :: FUNCTOR0:44
for A,B being transitive with_units (non empty AltCatStr),
F being feasible reflexive FunctorStr over A,B st
F is bijective comp-reversing Contravariant coreflexive
holds F" is comp-reversing;

definition let C1 be 1-sorted, C2 be non empty 1-sorted;
cluster Covariant -> reflexive BimapStr over C1,C2;
end;

definition let C1 be 1-sorted, C2 be non empty 1-sorted;
cluster Contravariant -> reflexive BimapStr over C1,C2;
end;

theorem :: FUNCTOR0:45
for C1,C2 being 1-sorted, M being BimapStr over C1,C2
st M is Covariant onto holds M is coreflexive;

theorem :: FUNCTOR0:46
for C1,C2 being 1-sorted, M being BimapStr over C1,C2
st M is Contravariant onto holds M is coreflexive;

definition
let C1 be transitive with_units (non empty AltCatStr),
C2 be with_units (non empty AltCatStr);
cluster covariant -> reflexive Functor of C1,C2;
end;

definition
let C1 be transitive with_units (non empty AltCatStr),
C2 be with_units (non empty AltCatStr);
cluster contravariant -> reflexive Functor of C1,C2;
end;

theorem :: FUNCTOR0:47
for C1 being transitive with_units (non empty AltCatStr),
C2 being with_units (non empty AltCatStr),
F being Functor of C1,C2 st F is covariant onto
holds F is coreflexive;

theorem :: FUNCTOR0:48
for C1 being transitive with_units (non empty AltCatStr),
C2 being with_units (non empty AltCatStr),
F being Functor of C1,C2 st F is contravariant onto
holds F is coreflexive;

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

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

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

```