:: Miscellaneous Facts about Functors
:: by Grzegorz Bancerek
::
:: Received July 31, 2001
:: Copyright (c) 2001-2012 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 over 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 )
proofend;

theorem Th2: :: YELLOW20:2
for A, B being non empty transitive with_units AltCatStr
for F being feasible Covariant FunctorStr over A,B
for G being feasible Covariant FunctorStr over 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 )
proofend;

theorem Th3: :: YELLOW20:3
for A, B being non empty transitive with_units AltCatStr
for F being feasible Contravariant FunctorStr over A,B
for G being feasible Contravariant FunctorStr over B,A st F is bijective &amp; 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 )
proofend;

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

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

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

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

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

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

begin

definition
let A, B be AltCatStr ;
predA,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]) &amp; 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 )
proofend;

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^> <> {} &amp; <^a2,a3^> <> {} holds
for b1, b2, b3 being object of B st <^b1,b2^> <> {} &amp; <^b2,b3^> <> {} &amp; b1 = a1 &amp; b2 = a2 &amp; 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 )
proofend;

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

definition
let f, g be Function;
func Intersect (f,g) ->  Function means :Def2: :: YELLOW20:def 2
( dom it = (dom f) /\ (dom g) &amp; ( 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) &amp; ( for x being set st x in (dom f) /\ (dom g) holds
b1 . x = (f . x) /\ (g . x) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = (dom f) /\ (dom g) &amp; ( for x being set st x in (dom f) /\ (dom g) holds
b1 . x = (f . x) /\ (g . x) ) &amp; dom b2 = (dom f) /\ (dom g) &amp; ( for x being set st x in (dom f) /\ (dom g) holds
b2 . x = (f . x) /\ (g . x) ) holds
b1 = b2
proofend;
commutativity
 for b1, f, g being Function st dom b1 = (dom f) /\ (dom g) &amp; ( 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) &amp; ( 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) &amp; ( 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
proofend;

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

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

theorem Th16: :: YELLOW20:16
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) &amp; 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 &amp; x in dom G holds
F . x tolerates G . x ) holds
Intersect (F,G) is ManySortedFunction of A,B
proofend;

theorem Th17: :: YELLOW20:17
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) &amp; Intersect ({|F|},{|G|}) = {|H|} )
proofend;

theorem Th18: :: YELLOW20:18
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) &amp; H2 = Intersect (F2,G2) &amp; Intersect ({|F1,F2|},{|G1,G2|}) = {|H1,H2|} )
proofend;

definition
let A, B be AltCatStr ;
assume B1: 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 &amp; the Arrows of it = Intersect ( the Arrows of A, the Arrows of B) &amp; 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 &amp; the Arrows of b1 = Intersect ( the Arrows of A, the Arrows of B) &amp; the Comp of b1 = Intersect ( the Comp of A, the Comp of B) )
proofend;
uniqueness
 for b1, b2 being strict AltCatStr st the carrier of b1 = the carrier of A /\ the carrier of B &amp; the Arrows of b1 = Intersect ( the Arrows of A, the Arrows of B) &amp; the Comp of b1 = Intersect ( the Comp of A, the Comp of B) &amp; the carrier of b2 = the carrier of A /\ the carrier of B &amp; the Arrows of b2 = Intersect ( the Arrows of A, the Arrows of B) &amp; 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 &amp; the Arrows of b3 = Intersect ( the Arrows of A, the Arrows of B) &amp; the Comp of b3 = Intersect ( the Comp of A, the Comp of B) ) );

theorem :: YELLOW20:19
for A, B being AltCatStr st A,B have_the_same_composition holds
Intersect (A,B) = Intersect (B,A)
proofend;

theorem Th20: :: YELLOW20:20
for A, B being AltCatStr st A,B have_the_same_composition holds
Intersect (A,B) is SubCatStr of A
proofend;

theorem Th21: :: YELLOW20:21
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 &amp; o1 = b1 &amp; o2 = a2 &amp; o2 = b2 holds
<^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>
proofend;

theorem Th22: :: YELLOW20:22
for A, B being transitive AltCatStr st A,B have_the_same_composition holds
Intersect (A,B) is transitive
proofend;

theorem Th23: :: YELLOW20:23
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 &amp; o1 = b1 &amp; o2 = a2 &amp; o2 = b2 &amp; <^a1,a2^> <> {} &amp; <^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^>
proofend;

theorem :: YELLOW20:24
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 &amp; o = b &amp; idm a = idm b holds
idm a in <^o,o^> by Th23;

theorem :: YELLOW20:25
for A, B being category st A,B have_the_same_composition &amp; not Intersect (A,B) is empty &amp; ( 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
proofend;

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 &amp; b9 = b &amp; <^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 &amp; b9 = b &amp; <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff P2[a,b,f] )
proofend;

theorem Th26: :: YELLOW20:26
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 &amp; b2 = a2 holds
<^b1,b2^> = <^a1,a2^> )
proofend;

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

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

begin

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

theorem Th27: :: YELLOW20:27
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
proofend;

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 &amp; incl C is comp-preserving )
proofend;
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_25;
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 funcF | C ->  strict covariant Functor of C,B;
coherence
 F | C is strict covariant Functor of C,B
proofend;
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 funcF | C ->  strict contravariant Functor of C,B;
coherence
 F | C is strict contravariant Functor of C,B
proofend;
end;

theorem Th28: :: YELLOW20:28
for A, B being category
for C being non empty subcategory of A
for F being FunctorStr over A,B
for a being object of A
for c being object of C st c = a holds
(F | C) . c = F . a
proofend;

theorem Th29: :: YELLOW20:29
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 &amp; d = b &amp; <^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
proofend;

theorem Th30: :: YELLOW20:30
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 &amp; d = b &amp; <^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
proofend;

theorem Th31: :: YELLOW20:31
for A, B being non empty AltGraph
for F being BimapStr over A,B st F is Covariant &amp; F is one-to-one holds
for a, b being object of A st F . a = F . b holds
a = b
proofend;

theorem Th32: :: YELLOW20:32
for A, B being non empty reflexive AltGraph
for F being feasible Covariant FunctorStr over 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
proofend;

theorem Th33: :: YELLOW20:33
for A, B being non empty AltGraph
for F being Covariant FunctorStr over 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 &amp; b = F . d &amp; <^c,d^> <> {} &amp; f = F . g )
proofend;

theorem Th34: :: YELLOW20:34
for A, B being non empty AltGraph
for F being BimapStr over A,B st F is Contravariant &amp; F is one-to-one holds
for a, b being object of A st F . a = F . b holds
a = b
proofend;

theorem Th35: :: YELLOW20:35
for A, B being non empty reflexive AltGraph
for F being feasible Contravariant FunctorStr over 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
proofend;

theorem Th36: :: YELLOW20:36
for A, B being non empty AltGraph
for F being Contravariant FunctorStr over 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 &amp; a = F . d &amp; <^c,d^> <> {} &amp; f = F . g )
proofend;

begin

definition
let A, B be category;
let F be FunctorStr over A,B;
let A9, B9 be category;
predA9,B9 are_isomorphic_under F means :: YELLOW20:def 4
( A9 is subcategory of A &amp; B9 is subcategory of B &amp; ex G being covariant Functor of A9,B9 st
( G is bijective &amp; ( for a9 being object of A9
for a being object of A st a9 = a holds
G . a9 = F . a ) &amp; ( for b9, c9 being object of A9
for b, c being object of A st <^b9,c9^> <> {} &amp; b9 = b &amp; 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 ) ) );
predA9,B9 are_anti-isomorphic_under F means :: YELLOW20:def 5
( A9 is subcategory of A &amp; B9 is subcategory of B &amp; ex G being contravariant Functor of A9,B9 st
( G is bijective &amp; ( for a9 being object of A9
for a being object of A st a9 = a holds
G . a9 = F . a ) &amp; ( for b9, c9 being object of A9
for b, c being object of A st <^b9,c9^> <> {} &amp; b9 = b &amp; 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 over A,B
for A9, B9 being category holds
( A9,B9 are_isomorphic_under F iff ( A9 is subcategory of A &amp; B9 is subcategory of B &amp; ex G being covariant Functor of A9,B9 st
( G is bijective &amp; ( for a9 being object of A9
for a being object of A st a9 = a holds
G . a9 = F . a ) &amp; ( for b9, c9 being object of A9
for b, c being object of A st <^b9,c9^> <> {} &amp; b9 = b &amp; 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 over A,B
for A9, B9 being category holds
( A9,B9 are_anti-isomorphic_under F iff ( A9 is subcategory of A &amp; B9 is subcategory of B &amp; ex G being contravariant Functor of A9,B9 st
( G is bijective &amp; ( for a9 being object of A9
for a being object of A st a9 = a holds
G . a9 = F . a ) &amp; ( for b9, c9 being object of A9
for b, c being object of A st <^b9,c9^> <> {} &amp; b9 = b &amp; 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:37
for A, B, A1, B1 being category
for F being FunctorStr over A,B st A1,B1 are_isomorphic_under F holds
A1,B1 are_isomorphic
proofend;

theorem :: YELLOW20:38
for A, B, A1, B1 being category
for F being FunctorStr over A,B st A1,B1 are_anti-isomorphic_under F holds
A1,B1 are_anti-isomorphic
proofend;

theorem :: YELLOW20:39
for A, B being category
for F being covariant Functor of A,B st A,B are_isomorphic_under F holds
F is bijective
proofend;

theorem :: YELLOW20:40
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
proofend;

theorem :: YELLOW20:41
for A, B being category
for F being covariant Functor of A,B st F is bijective holds
A,B are_isomorphic_under F
proofend;

theorem :: YELLOW20:42
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
proofend;

theorem :: YELLOW20:43
for A being category
for B being non empty subcategory of A holds B,B are_isomorphic_under id A
proofend;

theorem Th44: :: YELLOW20:44
for f, g being Function st f c= g holds
~ f c= ~ g
proofend;

theorem :: YELLOW20:45
for f, g being Function st dom f is Relation &amp; ~ f c= ~ g holds
f c= g
proofend;

theorem Th46: :: YELLOW20:46
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
proofend;

theorem Th47: :: YELLOW20:47
for A being non empty transitive AltCatStr
for B being non empty transitive SubCatStr of A holds B opp is SubCatStr of A opp
proofend;

theorem Th48: :: YELLOW20:48
for A being category
for B being non empty subcategory of A holds B opp is subcategory of A opp
proofend;

theorem :: YELLOW20:49
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))
proofend;

theorem :: YELLOW20:50
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 "
proofend;

theorem :: YELLOW20:51
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 "
proofend;

theorem :: YELLOW20:52
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 &amp; B2,B3 are_isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
proofend;

theorem :: YELLOW20:53
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 &amp; B2,B3 are_isomorphic_under G holds
B1,B3 are_anti-isomorphic_under G * F
proofend;

theorem :: YELLOW20:54
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 &amp; B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_anti-isomorphic_under G * F
proofend;

theorem :: YELLOW20:55
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 &amp; B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
proofend;

theorem :: YELLOW20:56
for A1, A2 being 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 &amp; ( for a being object of A1 holds
( a is object of B1 iff F . a is object of B2 ) ) &amp; ( for a, b being object of A1 st <^a,b^> <> {} holds
for a1, b1 being object of B1 st a1 = a &amp; b1 = b holds
for a2, b2 being object of B2 st a2 = F . a &amp; 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
proofend;

theorem :: YELLOW20:57
for A1, A2 being 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 &amp; ( for a being object of A1 holds
( a is object of B1 iff F . a is object of B2 ) ) &amp; ( for a, b being object of A1 st <^a,b^> <> {} holds
for a1, b1 being object of B1 st a1 = a &amp; b1 = b holds
for a2, b2 being object of B2 st a2 = F . a &amp; 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
proofend;