:: Miscellaneous Facts about Functors
:: by Grzegorz Bancerek
::
:: Received July 31, 2001
:: Copyright (c) 2001-2011 Association of Mizar Users


begin

theorem Th1: :: YELLOW20:1
for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr of A,B st F is coreflexive & F is bijective holds
for a being object of A
for b being object of B holds
( F . a = b iff (F ") . b = a )
proof end;

theorem Th2: :: YELLOW20:2
for A, B being non empty transitive with_units AltCatStr
for F being feasible Covariant FunctorStr of A,B
for G being feasible Covariant FunctorStr of B,A st F is bijective & G = F " holds
for a1, a2 being object of A st <^a1,a2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of (F . a1),(F . a2) holds
( F . f = g iff G . g = f )
proof end;

theorem Th3: :: YELLOW20:3
for A, B being non empty transitive with_units AltCatStr
for F being feasible Contravariant FunctorStr of A,B
for G being feasible Contravariant FunctorStr of B,A st F is bijective & G = F " holds
for a1, a2 being object of A st <^a1,a2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of (F . a2),(F . a1) holds
( F . f = g iff G . g = f )
proof end;

theorem Th4: :: YELLOW20:4
for A, B being category
for F being Functor of A,B st F is bijective holds
for G being Functor of B,A st F * G = id B holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
proof end;

theorem Th5: :: YELLOW20:5
for A, B being category
for F being Functor of A,B st F is bijective holds
for G being Functor of B,A st G * F = id A holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
proof end;

theorem :: YELLOW20:6
for A, B being category
for F being covariant Functor of A,B st F is bijective holds
for G being covariant Functor of B,A st ( for b being object of B holds F . (G . b) = b ) & ( for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . (G . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
proof end;

theorem :: YELLOW20:7
for A, B being category
for F being contravariant Functor of A,B st F is bijective holds
for G being contravariant Functor of B,A st ( for b being object of B holds F . (G . b) = b ) & ( for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . (G . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
proof end;

theorem :: YELLOW20:8
for A, B being category
for F being covariant Functor of A,B st F is bijective holds
for G being covariant Functor of B,A st ( for a being object of A holds G . (F . a) = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . (F . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
proof end;

theorem :: YELLOW20:9
for A, B being category
for F being contravariant Functor of A,B st F is bijective holds
for G being contravariant Functor of B,A st ( for a being object of A holds G . (F . a) = a ) & ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . (F . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
proof end;

begin

definition
let A, B be AltCatStr ;
pred A,B have_the_same_composition means :Def1: :: YELLOW20:def 1
for a1, a2, a3 being set holds the Comp of A . [a1,a2,a3] tolerates the Comp of B . [a1,a2,a3];
symmetry
for A, B being AltCatStr st ( for a1, a2, a3 being set holds the Comp of A . [a1,a2,a3] tolerates the Comp of B . [a1,a2,a3] ) holds
for a1, a2, a3 being set holds the Comp of B . [a1,a2,a3] tolerates the Comp of A . [a1,a2,a3]
;
end;

:: deftheorem Def1 defines have_the_same_composition YELLOW20:def 1 :
for A, B being AltCatStr holds
( A,B have_the_same_composition iff for a1, a2, a3 being set holds the Comp of A . [a1,a2,a3] tolerates the Comp of B . [a1,a2,a3] );

theorem Th10: :: YELLOW20:10
for A, B being AltCatStr holds
( A,B have_the_same_composition iff for a1, a2, a3, x being set st x in dom ( the Comp of A . [a1,a2,a3]) & x in dom ( the Comp of B . [a1,a2,a3]) holds
( the Comp of A . [a1,a2,a3]) . x = ( the Comp of B . [a1,a2,a3]) . x )
proof end;

theorem Th11: :: YELLOW20:11
for A, B being non empty transitive AltCatStr holds
( A,B have_the_same_composition iff for a1, a2, a3 being object of A st <^a1,a2^> <> {} & <^a2,a3^> <> {} holds
for b1, b2, b3 being object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds
for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1 )
proof end;

theorem :: YELLOW20:12
for A, B being semi-functional para-functional category holds A,B have_the_same_composition
proof end;

definition
let f, g be Function;
func Intersect (f,g) -> Function means :Def2: :: YELLOW20:def 2
( dom it = (dom f) /\ (dom g) & ( for x being set st x in (dom f) /\ (dom g) holds
it . x = (f . x) /\ (g . x) ) );
existence
ex b1 being Function st
( dom b1 = (dom f) /\ (dom g) & ( for x being set st x in (dom f) /\ (dom g) holds
b1 . x = (f . x) /\ (g . x) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = (dom f) /\ (dom g) & ( for x being set st x in (dom f) /\ (dom g) holds
b1 . x = (f . x) /\ (g . x) ) & dom b2 = (dom f) /\ (dom g) & ( for x being set st x in (dom f) /\ (dom g) holds
b2 . x = (f . x) /\ (g . x) ) holds
b1 = b2
proof end;
commutativity
for b1, f, g being Function st dom b1 = (dom f) /\ (dom g) & ( for x being set st x in (dom f) /\ (dom g) holds
b1 . x = (f . x) /\ (g . x) ) holds
( dom b1 = (dom g) /\ (dom f) & ( for x being set st x in (dom g) /\ (dom f) holds
b1 . x = (g . x) /\ (f . x) ) )
;
end;

:: deftheorem Def2 defines Intersect YELLOW20:def 2 :
for f, g, b3 being Function holds
( b3 = Intersect (f,g) iff ( dom b3 = (dom f) /\ (dom g) & ( for x being set st x in (dom f) /\ (dom g) holds
b3 . x = (f . x) /\ (g . x) ) ) );

theorem :: YELLOW20:13
for I being set
for A, B being ManySortedSet of I holds Intersect (A,B) = A /\ B
proof end;

theorem Th14: :: YELLOW20:14
for I, J being set
for A being ManySortedSet of I
for B being ManySortedSet of J holds Intersect (A,B) is ManySortedSet of I /\ J
proof end;

theorem Th15: :: YELLOW20:15
for I, J being set
for A being ManySortedSet of I
for B being Function
for C being ManySortedSet of J st C = Intersect (A,B) holds
C cc= A
proof end;

theorem :: YELLOW20:16
canceled;

theorem Th17: :: YELLOW20:17
for I1, I2 being set
for A1, B1 being ManySortedSet of I1
for A2, B2 being ManySortedSet of I2
for A, B being ManySortedSet of I1 /\ I2 st A = Intersect (A1,A2) & B = Intersect (B1,B2) holds
for F being ManySortedFunction of A1,B1
for G being ManySortedFunction of A2,B2 st ( for x being set st x in dom F & x in dom G holds
F . x tolerates G . x ) holds
Intersect (F,G) is ManySortedFunction of A,B
proof end;

theorem Th18: :: YELLOW20:18
for I, J being set
for F being ManySortedSet of [:I,I:]
for G being ManySortedSet of [:J,J:] ex H being ManySortedSet of [:(I /\ J),(I /\ J):] st
( H = Intersect (F,G) & Intersect ({|F|},{|G|}) = {|H|} )
proof end;

theorem Th19: :: YELLOW20:19
for I, J being set
for F1, F2 being ManySortedSet of [:I,I:]
for G1, G2 being ManySortedSet of [:J,J:] ex H1, H2 being ManySortedSet of [:(I /\ J),(I /\ J):] st
( H1 = Intersect (F1,G1) & H2 = Intersect (F2,G2) & Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} )
proof end;

definition
let A, B be AltCatStr ;
assume A1: A,B have_the_same_composition ;
func Intersect (A,B) -> strict AltCatStr means :Def3: :: YELLOW20:def 3
( the carrier of it = the carrier of A /\ the carrier of B & the Arrows of it = Intersect ( the Arrows of A, the Arrows of B) & the Comp of it = Intersect ( the Comp of A, the Comp of B) );
existence
ex b1 being strict AltCatStr st
( the carrier of b1 = the carrier of A /\ the carrier of B & the Arrows of b1 = Intersect ( the Arrows of A, the Arrows of B) & the Comp of b1 = Intersect ( the Comp of A, the Comp of B) )
proof end;
uniqueness
for b1, b2 being strict AltCatStr st the carrier of b1 = the carrier of A /\ the carrier of B & the Arrows of b1 = Intersect ( the Arrows of A, the Arrows of B) & the Comp of b1 = Intersect ( the Comp of A, the Comp of B) & the carrier of b2 = the carrier of A /\ the carrier of B & the Arrows of b2 = Intersect ( the Arrows of A, the Arrows of B) & the Comp of b2 = Intersect ( the Comp of A, the Comp of B) holds
b1 = b2
;
end;

:: deftheorem Def3 defines Intersect YELLOW20:def 3 :
for A, B being AltCatStr st A,B have_the_same_composition holds
for b3 being strict AltCatStr holds
( b3 = Intersect (A,B) iff ( the carrier of b3 = the carrier of A /\ the carrier of B & the Arrows of b3 = Intersect ( the Arrows of A, the Arrows of B) & the Comp of b3 = Intersect ( the Comp of A, the Comp of B) ) );

theorem :: YELLOW20:20
for A, B being AltCatStr st A,B have_the_same_composition holds
Intersect (A,B) = Intersect (B,A)
proof end;

theorem Th21: :: YELLOW20:21
for A, B being AltCatStr st A,B have_the_same_composition holds
Intersect (A,B) is SubCatStr of A
proof end;

theorem Th22: :: YELLOW20:22
for A, B being AltCatStr st A,B have_the_same_composition holds
for a1, a2 being object of A
for b1, b2 being object of B
for o1, o2 being object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 holds
<^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>
proof end;

theorem Th23: :: YELLOW20:23
for A, B being transitive AltCatStr st A,B have_the_same_composition holds
Intersect (A,B) is transitive
proof end;

theorem Th24: :: YELLOW20:24
for A, B being AltCatStr st A,B have_the_same_composition holds
for a1, a2 being object of A
for b1, b2 being object of B
for o1, o2 being object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^b1,b2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of b1,b2 st f = g holds
f in <^o1,o2^>
proof end;

theorem :: YELLOW20:25
for A, B being non empty with_units AltCatStr st A,B have_the_same_composition holds
for a being object of A
for b being object of B
for o being object of (Intersect (A,B)) st o = a & o = b & idm a = idm b holds
idm a in <^o,o^> by Th24;

theorem :: YELLOW20:26
for A, B being category st A,B have_the_same_composition & not Intersect (A,B) is empty & ( for a being object of A
for b being object of B st a = b holds
idm a = idm b ) holds
Intersect (A,B) is subcategory of A
proof end;

begin

scheme :: YELLOW20:sch 1
SubcategoryUniq{ F1() -> category, F2() -> non empty subcategory of F1(), F3() -> non empty subcategory of F1(), P1[ set ], P2[ set , set , set ] } :
AltCatStr(# the carrier of F2(), the Arrows of F2(), the Comp of F2() #) = AltCatStr(# the carrier of F3(), the Arrows of F3(), the Comp of F3() #)
provided
A1: for a being object of F1() holds
( a is object of F2() iff P1[a] ) and
A2: for a, b being object of F1()
for a9, b9 being object of F2() st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff P2[a,b,f] ) and
A3: for a being object of F1() holds
( a is object of F3() iff P1[a] ) and
A4: for a, b being object of F1()
for a9, b9 being object of F3() st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff P2[a,b,f] )
proof end;

theorem Th27: :: YELLOW20:27
for A being non empty AltCatStr
for B being non empty SubCatStr of A holds
( B is full iff for a1, a2 being object of A
for b1, b2 being object of B st b1 = a1 & b2 = a2 holds
<^b1,b2^> = <^a1,a2^> )
proof end;

scheme :: YELLOW20:sch 2
FullSubcategoryEx{ F1() -> category, P1[ set ] } :
ex B being non empty strict full subcategory of F1() st
for a being object of F1() holds
( a is object of B iff P1[a] )
provided
A1: ex a being object of F1() st P1[a]
proof end;

scheme :: YELLOW20:sch 3
FullSubcategoryUniq{ F1() -> category, F2() -> non empty full subcategory of F1(), F3() -> non empty full subcategory of F1(), P1[ set ] } :
AltCatStr(# the carrier of F2(), the Arrows of F2(), the Comp of F2() #) = AltCatStr(# the carrier of F3(), the Arrows of F3(), the Comp of F3() #)
provided
A1: for a being object of F1() holds
( a is object of F2() iff P1[a] ) and
A2: for a being object of F1() holds
( a is object of F3() iff P1[a] )
proof end;

begin

registration
let f be Function-yielding Function;
let x, y be set ;
cluster f . (x,y) -> Relation-like Function-like ;
coherence
( f . (x,y) is Relation-like & f . (x,y) is Function-like )
;
end;

theorem Th28: :: YELLOW20:28
for A being category
for C being non empty subcategory of A
for a, b being object of C st <^a,b^> <> {} holds
for f being Morphism of a,b holds (incl C) . f = f
proof end;

registration
let A be category;
let C be non empty subcategory of A;
cluster incl C -> id-preserving comp-preserving ;
coherence
( incl C is id-preserving & incl C is comp-preserving )
proof end;
end;

registration
let A be category;
let C be non empty subcategory of A;
cluster incl C -> Covariant ;
coherence
incl C is Covariant
;
end;

definition
let A be category;
let C be non empty subcategory of A;
:: original: incl
redefine func incl C -> strict covariant Functor of C,A;
coherence
incl C is strict covariant Functor of C,A
by FUNCTOR0:def 26;
end;

definition
let A, B be category;
let C be non empty subcategory of A;
let F be covariant Functor of A,B;
:: original: |
redefine func F | C -> strict covariant Functor of C,B;
coherence
F | C is strict covariant Functor of C,B
proof end;
end;

definition
let A, B be category;
let C be non empty subcategory of A;
let F be contravariant Functor of A,B;
:: original: |
redefine func F | C -> strict contravariant Functor of C,B;
coherence
F | C is strict contravariant Functor of C,B
proof end;
end;

theorem Th29: :: YELLOW20:29
for A, B being category
for C being non empty subcategory of A
for F being FunctorStr of A,B
for a being object of A
for c being object of C st c = a holds
(F | C) . c = F . a
proof end;

theorem Th30: :: YELLOW20:30
for A, B being category
for C being non empty subcategory of A
for F being covariant Functor of A,B
for a, b being object of A
for c, d being object of C st c = a & d = b & <^c,d^> <> {} holds
for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
proof end;

theorem Th31: :: YELLOW20:31
for A, B being category
for C being non empty subcategory of A
for F being contravariant Functor of A,B
for a, b being object of A
for c, d being object of C st c = a & d = b & <^c,d^> <> {} holds
for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
proof end;

theorem Th32: :: YELLOW20:32
for A, B being non empty AltGraph
for F being BimapStr of A,B st F is Covariant & F is one-to-one holds
for a, b being object of A st F . a = F . b holds
a = b
proof end;

theorem Th33: :: YELLOW20:33
for A, B being non empty reflexive AltGraph
for F being feasible Covariant FunctorStr of A,B st F is faithful holds
for a, b being object of A st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F . f = F . g holds
f = g
proof end;

theorem Th34: :: YELLOW20:34
for A, B being non empty AltGraph
for F being Covariant FunctorStr of A,B st F is surjective holds
for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g )
proof end;

theorem Th35: :: YELLOW20:35
for A, B being non empty AltGraph
for F being BimapStr of A,B st F is Contravariant & F is one-to-one holds
for a, b being object of A st F . a = F . b holds
a = b
proof end;

theorem Th36: :: YELLOW20:36
for A, B being non empty reflexive AltGraph
for F being feasible Contravariant FunctorStr of A,B st F is faithful holds
for a, b being object of A st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F . f = F . g holds
f = g
proof end;

theorem Th37: :: YELLOW20:37
for A, B being non empty AltGraph
for F being Contravariant FunctorStr of A,B st F is surjective holds
for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( b = F . c & a = F . d & <^c,d^> <> {} & f = F . g )
proof end;

begin

definition
let A, B be category;
let F be FunctorStr of A,B;
let A9, B9 be category;
pred A9,B9 are_isomorphic_under F means :: YELLOW20:def 4
( A9 is subcategory of A & B9 is subcategory of B & ex G being covariant Functor of A9,B9 st
( G is bijective & ( for a9 being object of A9
for a being object of A st a9 = a holds
G . a9 = F . a ) & ( for b9, c9 being object of A9
for b, c being object of A st <^b9,c9^> <> {} & b9 = b & c9 = c holds
for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
G . f9 = (Morph-Map (F,b,c)) . f ) ) );
pred A9,B9 are_anti-isomorphic_under F means :: YELLOW20:def 5
( A9 is subcategory of A & B9 is subcategory of B & ex G being contravariant Functor of A9,B9 st
( G is bijective & ( for a9 being object of A9
for a being object of A st a9 = a holds
G . a9 = F . a ) & ( for b9, c9 being object of A9
for b, c being object of A st <^b9,c9^> <> {} & b9 = b & c9 = c holds
for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
G . f9 = (Morph-Map (F,b,c)) . f ) ) );
end;

:: deftheorem defines are_isomorphic_under YELLOW20:def 4 :
for A, B being category
for F being FunctorStr of A,B
for A9, B9 being category holds
( A9,B9 are_isomorphic_under F iff ( A9 is subcategory of A & B9 is subcategory of B & ex G being covariant Functor of A9,B9 st
( G is bijective & ( for a9 being object of A9
for a being object of A st a9 = a holds
G . a9 = F . a ) & ( for b9, c9 being object of A9
for b, c being object of A st <^b9,c9^> <> {} & b9 = b & c9 = c holds
for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
G . f9 = (Morph-Map (F,b,c)) . f ) ) ) );

:: deftheorem defines are_anti-isomorphic_under YELLOW20:def 5 :
for A, B being category
for F being FunctorStr of A,B
for A9, B9 being category holds
( A9,B9 are_anti-isomorphic_under F iff ( A9 is subcategory of A & B9 is subcategory of B & ex G being contravariant Functor of A9,B9 st
( G is bijective & ( for a9 being object of A9
for a being object of A st a9 = a holds
G . a9 = F . a ) & ( for b9, c9 being object of A9
for b, c being object of A st <^b9,c9^> <> {} & b9 = b & c9 = c holds
for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
G . f9 = (Morph-Map (F,b,c)) . f ) ) ) );

theorem :: YELLOW20:38
for A, B, A1, B1 being category
for F being FunctorStr of A,B st A1,B1 are_isomorphic_under F holds
A1,B1 are_isomorphic
proof end;

theorem :: YELLOW20:39
for A, B, A1, B1 being category
for F being FunctorStr of A,B st A1,B1 are_anti-isomorphic_under F holds
A1,B1 are_anti-isomorphic
proof end;

theorem :: YELLOW20:40
for A, B being category
for F being covariant Functor of A,B st A,B are_isomorphic_under F holds
F is bijective
proof end;

theorem :: YELLOW20:41
for A, B being category
for F being contravariant Functor of A,B st A,B are_anti-isomorphic_under F holds
F is bijective
proof end;

theorem :: YELLOW20:42
for A, B being category
for F being covariant Functor of A,B st F is bijective holds
A,B are_isomorphic_under F
proof end;

theorem :: YELLOW20:43
for A, B being category
for F being contravariant Functor of A,B st F is bijective holds
A,B are_anti-isomorphic_under F
proof end;

theorem :: YELLOW20:44
for A being category
for B being non empty subcategory of A holds B,B are_isomorphic_under id A
proof end;

theorem Th45: :: YELLOW20:45
for f, g being Function st f c= g holds
~ f c= ~ g
proof end;

theorem :: YELLOW20:46
for f, g being Function st dom f is Relation & ~ f c= ~ g holds
f c= g
proof end;

theorem Th47: :: YELLOW20:47
for I, J being set
for A being ManySortedSet of [:I,I:]
for B being ManySortedSet of [:J,J:] st A cc= B holds
~ A cc= ~ B
proof end;

theorem Th48: :: YELLOW20:48
for A being non empty transitive AltCatStr
for B being non empty transitive SubCatStr of A holds B opp is SubCatStr of A opp
proof end;

theorem Th49: :: YELLOW20:49
for A being category
for B being non empty subcategory of A holds B opp is subcategory of A opp
proof end;

theorem :: YELLOW20:50
for A being category
for B being non empty subcategory of A holds B,B opp are_anti-isomorphic_under dualizing-func (A,(A opp))
proof end;

theorem :: YELLOW20:51
for A1, A2 being category
for F being covariant Functor of A1,A2 st F is bijective holds
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 st B1,B2 are_isomorphic_under F holds
B2,B1 are_isomorphic_under F "
proof end;

theorem :: YELLOW20:52
for A1, A2 being category
for F being contravariant Functor of A1,A2 st F is bijective holds
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 st B1,B2 are_anti-isomorphic_under F holds
B2,B1 are_anti-isomorphic_under F "
proof end;

theorem :: YELLOW20:53
for A1, A2, A3 being category
for F being covariant Functor of A1,A2
for G being covariant Functor of A2,A3
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_isomorphic_under F & B2,B3 are_isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
proof end;

theorem :: YELLOW20:54
for A1, A2, A3 being category
for F being contravariant Functor of A1,A2
for G being covariant Functor of A2,A3
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_anti-isomorphic_under F & B2,B3 are_isomorphic_under G holds
B1,B3 are_anti-isomorphic_under G * F
proof end;

theorem :: YELLOW20:55
for A1, A2, A3 being category
for F being covariant Functor of A1,A2
for G being contravariant Functor of A2,A3
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_anti-isomorphic_under G * F
proof end;

theorem :: YELLOW20:56
for A1, A2, A3 being category
for F being contravariant Functor of A1,A2
for G being contravariant Functor of A2,A3
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 st B1,B2 are_anti-isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
proof end;

theorem :: YELLOW20:57
for A1, A2 being non empty category
for F being covariant Functor of A1,A2
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 st F is bijective & ( for a being object of A1 holds
( a is object of B1 iff F . a is object of B2 ) ) & ( for a, b being object of A1 st <^a,b^> <> {} holds
for a1, b1 being object of B1 st a1 = a & b1 = b holds
for a2, b2 being object of B2 st a2 = F . a & b2 = F . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff F . f in <^a2,b2^> ) ) holds
B1,B2 are_isomorphic_under F
proof end;

theorem :: YELLOW20:58
for A1, A2 being non empty category
for F being contravariant Functor of A1,A2
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 st F is bijective & ( for a being object of A1 holds
( a is object of B1 iff F . a is object of B2 ) ) & ( for a, b being object of A1 st <^a,b^> <> {} holds
for a1, b1 being object of B1 st a1 = a & b1 = b holds
for a2, b2 being object of B2 st a2 = F . a & b2 = F . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff F . f in <^b2,a2^> ) ) holds
B1,B2 are_anti-isomorphic_under F
proof end;